theorem proved tactic proof

`self_composition_cosh`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 170theorem self_composition_cosh (η : ℝ) :
 171    Real.cosh (2 * (2 * η)) - 1 =
 172    2 * (Real.cosh (2 * η) - 1) ^ 2 + 4 * (Real.cosh (2 * η) - 1) := by

proof body

Tactic-mode proof.

 173  have hd := Real.cosh_two_mul (2 * η)
 174  have hs := Real.cosh_sq (2 * η)
 175  set c := Real.cosh (2 * η) with hc_def
 176  set s := Real.sinh (2 * η) with hs_def
 177  have lhs : Real.cosh (2 * (2 * η)) - 1 = 2 * c ^ 2 - 2 := by linarith
 178  have rhs : 2 * (c - 1) ^ 2 + 4 * (c - 1) = 2 * c ^ 2 - 2 := by ring
 179  linarith
 180
 181end
 182
 183end NumberTheory
 184end IndisputableMonolith