[GOAL]
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
⊢ ∃ c, c ∈ Ioo a b ∧ deriv f c = 0
[PROOFSTEP]
by_cases h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
[GOAL]
case pos
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
⊢ ∃ c, c ∈ Ioo a b ∧ deriv f c = 0
[PROOFSTEP]
exact exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt
[GOAL]
case neg
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ¬∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
⊢ ∃ c, c ∈ Ioo a b ∧ deriv f c = 0
[PROOFSTEP]
obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
[GOAL]
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ¬∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
⊢ ∃ x, x ∈ Ioo a b ∧ ¬DifferentiableAt ℝ f x
[PROOFSTEP]
push_neg at h 
[GOAL]
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ∃ x, x ∈ Ioo a b ∧ ¬DifferentiableAt ℝ f x
⊢ ∃ x, x ∈ Ioo a b ∧ ¬DifferentiableAt ℝ f x
[PROOFSTEP]
exact h
[GOAL]
case neg.intro.intro
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ¬∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
c : ℝ
hc : c ∈ Ioo a b
hcdiff : ¬DifferentiableAt ℝ f c
⊢ ∃ c, c ∈ Ioo a b ∧ deriv f c = 0
[PROOFSTEP]
exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩
