-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi (f : ℝ → ℝ) {a : ℝ}
    (hf : Tendsto (deriv f) (𝓝[>] a) atTop) : ¬ DifferentiableWithinAt ℝ f (Ioi a) a

Proof state:
case intro.intro
f : ℝ → ℝ
a : ℝ
hf : ∀ t ∈ atTop, ∃ i, a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
z : ℝ
hz : z ∈ Ioc a x
hb : ∀ ⦃x : ℝ⦄, a < x → x < b → (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
⊢ (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) z

Tactic:
exact hb hz.1 <| hz.2.trans_lt hx.2

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
⊢ 𝓝[Ioc a b] z = 𝓝[Icc a b] z

Tactic:
refine nhdsWithin_eq_nhdsWithin' (s := Ioi a) (Ioi_mem_nhds hz''.1) ?_

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
⊢ Ioc a b ∩ Ioi a = Icc a b ∩ Ioi a

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
⊢ Ioc a b = Icc a b ∩ Ioi a

Tactic:
ext y

Result:
case h
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
y : ℝ
⊢ y ∈ Ioc a b ↔ y ∈ Icc a b ∩ Ioi a

Proof state:
case intro.intro
f : ℝ → ℝ
a : ℝ
hf : ∀ t ∈ atTop, ∃ i, a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
hb : MapsTo (derivWithin f (Ioi a)) (Ioo a b) (Ioi ((derivWithin f (Ioi a) a + 1) ⊔ 0))
x : ℝ
hx : x ∈ Ioo a b
z : ℝ
hz : z ∈ Ioc a x
⊢ (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) z

Tactic:
simp only [MapsTo, mem_Ioo, mem_Ioi, and_imp] at hb

Result:
case intro.intro
f : ℝ → ℝ
a : ℝ
hf : ∀ t ∈ atTop, ∃ i, a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
z : ℝ
hz : z ∈ Ioc a x
hb : ∀ ⦃x : ℝ⦄, a < x → x < b → (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
⊢ (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) z

Proof state:
case h.intro.intro
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
hcont : ContinuousOn f (Icc a b)
x : ℝ
hx₁ : x ∈ Ioo a b
hb : (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
hx₂ : derivWithin f (Ioi a) x = slope f a b
⊢ False

Tactic:
rw [hx₂, max_lt_iff] at hb

Result:
case h.intro.intro
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
hcont : ContinuousOn f (Icc a b)
x : ℝ
hx₁ : x ∈ Ioo a b
hb : derivWithin f (Ioi a) a + 1 < slope f a b ∧ 0 < slope f a b
hx₂ : derivWithin f (Ioi a) x = slope f a b
⊢ False

Proof state:
case neg
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
z : ℝ
hz : z ∈ Icc a b
hz' : ¬z = a
⊢ ContinuousWithinAt f (Icc a b) z

Tactic:
exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩

Result:
no goals

Proof state:
case h.intro.intro
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
hcont : ContinuousOn f (Icc a b)
x : ℝ
hx₁ : x ∈ Ioo a b
hb : derivWithin f (Ioi a) a + 1 < slope f a b ∧ 0 < slope f a b
hx₂ : derivWithin f (Ioi a) x = slope f a b
⊢ False

Tactic:
linarith

Result:
no goals