lemma
proved
tactic proof
dAlembert_double
show as:
view Lean formalization →
formal statement (Lean)
106lemma dAlembert_double
107 (H : ℝ → ℝ)
108 (h_one : H 0 = 1)
109 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) (t : ℝ) :
110 H (2 * t) = 2 * (H t)^2 - 1 := by
proof body
Tactic-mode proof.
111 have h := h_dAlembert t t
112 have h' : H (t + t) = 2 * (H t)^2 - 1 := by
113 -- H(2t) + H(0) = 2 H(t)^2
114 have h0 : H (t + t) + 1 = 2 * H t * H t := by
115 simpa [h_one] using h
116 have h1 : H (t + t) = 2 * H t * H t - 1 := by
117 linarith
118 simpa [pow_two, mul_assoc] using h1
119 simpa [two_mul] using h'
120