lemma
proved
tactic proof
dAlembert_product
show as:
view Lean formalization →
formal statement (Lean)
121lemma dAlembert_product
122 (H : ℝ → ℝ)
123 (h_one : H 0 = 1)
124 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
125 ∀ t u, H (t+u) * H (t-u) = (H t)^2 + (H u)^2 - 1 := by
proof body
Tactic-mode proof.
126 intro t u
127 have h := h_dAlembert (t + u) (t - u)
128 have h' : H (2 * t) + H (2 * u) = 2 * H (t + u) * H (t - u) := by
129 -- (t+u)+(t-u)=2t and (t+u)-(t-u)=2u
130 simpa [two_mul, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h
131 have h2t : H (2 * t) = 2 * (H t)^2 - 1 := dAlembert_double H h_one h_dAlembert t
132 have h2u : H (2 * u) = 2 * (H u)^2 - 1 := dAlembert_double H h_one h_dAlembert u
133 have h'' : 2 * H (t + u) * H (t - u) = (2 * (H t)^2 - 1) + (2 * (H u)^2 - 1) := by
134 calc
135 2 * H (t + u) * H (t - u) = H (2 * t) + H (2 * u) := by linarith [h']
136 _ = (2 * (H t)^2 - 1) + (2 * (H u)^2 - 1) := by simp [h2t, h2u]
137 linarith
138