theorem
proved
tactic proof
even_deriv_at_zero
show as:
view Lean formalization →
formal statement (Lean)
76theorem even_deriv_at_zero (H : ℝ → ℝ)
77 (h_even : Function.Even H) (h_diff : DifferentiableAt ℝ H 0) : deriv H 0 = 0 := by
proof body
Tactic-mode proof.
78 -- For even functions, the derivative at 0 is 0
79 let negFun : ℝ → ℝ := fun x => -x
80 have h1 : deriv H 0 = deriv (H ∘ negFun) 0 := by
81 congr 1
82 ext x
83 simp only [Function.comp_apply, negFun]
84 exact (h_even x).symm
85 have h2 : deriv (H ∘ negFun) 0 = -deriv H 0 := by
86 have hd : DifferentiableAt ℝ negFun 0 := differentiable_neg.differentiableAt
87 have h_diff_neg : DifferentiableAt ℝ H (negFun 0) := by simp [negFun]; exact h_diff
88 have hchain := deriv_comp (x := (0 : ℝ)) h_diff_neg hd
89 rw [hchain]
90 simp only [negFun, neg_zero]
91 have hdn : deriv negFun 0 = -1 := congrFun deriv_neg' 0
92 rw [hdn]
93 ring
94 rw [h1] at h2
95 linarith
96