theorem
proved
tactic proof
cos_second_deriv_eq
show as:
view Lean formalization →
formal statement (Lean)
118theorem cos_second_deriv_eq : ∀ t, deriv (deriv (fun x => Real.cos x)) t = -Real.cos t := by
proof body
Tactic-mode proof.
119 intro t
120 have h1 : deriv (fun x => Real.cos x) = (fun x => -Real.sin x) := by
121 funext x
122 simpa using (Real.deriv_cos x)
123 rw [h1]
124 have hneg : deriv (fun x => -Real.sin x) t = -(deriv Real.sin t) := by
125 simpa using (deriv_neg (f := Real.sin) (x := t))
126 rw [hneg]
127 simp [Real.deriv_sin]
128
129/-- cos has the correct initial conditions: cos(0) = 1, cos'(0) = 0. -/