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

State before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ f' = 0
Tactic:
apply IsLocalExtr.elim h
State after:
case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ IsLocalMin f a → f' = 0

case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ IsLocalMax f a → f' = 0

State before:
case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ IsLocalMin f a → f' = 0
Tactic:
intro h
State after:
case a
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalExtr f a
hf : HasDerivAt f f' a
h : IsLocalMin f a
⊢ f' = 0

State before:
case a
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalExtr f a
hf : HasDerivAt f f' a
h : IsLocalMin f a
⊢ f' = 0
Tactic:
apply IsLocalMin.hasDerivAt_eq_zero h hf
State after:
no goals

State before:
case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ IsLocalMax f a → f' = 0
Tactic:
intro h
State after:
case a
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalExtr f a
hf : HasDerivAt f f' a
h : IsLocalMax f a
⊢ f' = 0

State before:
case a
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalExtr f a
hf : HasDerivAt f f' a
h : IsLocalMax f a
⊢ f' = 0
Tactic:
apply IsLocalMax.hasDerivAt_eq_zero h hf
State after:
no goals