lemma
proved
tactic proof
dAlembert_diff_square
show as:
view Lean formalization →
formal statement (Lean)
139lemma dAlembert_diff_square
140 (H : ℝ → ℝ)
141 (h_one : H 0 = 1)
142 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
143 ∀ t u,
144 (H (t+u) - H (t-u))^2 = 4 * ((H t)^2 - 1) * ((H u)^2 - 1) := by
proof body
Tactic-mode proof.
145 intro t u
146 have h_sum : H (t+u) + H (t-u) = 2 * H t * H u := h_dAlembert t u
147 have h_prod : H (t+u) * H (t-u) = (H t)^2 + (H u)^2 - 1 :=
148 dAlembert_product H h_one h_dAlembert t u
149 calc
150 (H (t+u) - H (t-u))^2
151 = (H (t+u) + H (t-u))^2 - 4 * (H (t+u) * H (t-u)) := by ring
152 _ = (2 * H t * H u)^2 - 4 * ((H t)^2 + (H u)^2 - 1) := by
153 simp [h_sum, h_prod]
154 _ = 4 * ((H t)^2 - 1) * ((H u)^2 - 1) := by ring
155