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

State before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, f' c = 0
Tactic:
have ⟨c, cmem, hc⟩ := exists_local_extr_Ioo hab hfc hfI
State after:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : IsLocalExtr f c
⊢ ∃ c ∈ Ioo a b, f' c = 0

State before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : IsLocalExtr f c
⊢ ∃ c ∈ Ioo a b, f' c = 0
Tactic:
exact ⟨c, cmem, IsLocalExtr.hasDerivAt_eq_zero hc <| hff' c cmem⟩
State after:
no goals