Theorem: Tutorial.IsLocalMin.hasDerivAt_eq_zero (Solution/Advanced/Analysis/Lecture2.lean)

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ f' = 0
Tactic:
suffices -f' = 0 from neg_eq_zero.mp this
State after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ -f' = 0

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ -f' = 0
Tactic:
apply IsLocalMax.hasDerivAt_eq_zero
State after:
case h
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ IsLocalMax ?f ?a

case hf
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ HasDerivAt ?f (-f') ?a

case f
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ ℝ → ℝ

case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ ℝ

State before:
case h
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ IsLocalMax ?f ?a

case hf
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ HasDerivAt ?f (-f') ?a

case f
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ ℝ → ℝ

case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ ℝ
Tactic:
apply IsLocalMin.neg h
State after:
case hf
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ HasDerivAt (fun x => -f x) (-f') a

State before:
case hf
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ HasDerivAt (fun x => -f x) (-f') a
Tactic:
apply hf.neg
State after:
no goals