-- 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 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
⊢ False

Tactic:
have hdiff' : DifferentiableOn ℝ f (Ioc a b) := fun z hz => by
  refine DifferentiableWithinAt.mono (t := Ioi a) ?_ Ioc_subset_Ioi_self
  have : derivWithin f (Ioi a) z ≠ 0 := ne_of_gt <| by
    simp_all only [mem_Ioo, and_imp, mem_Ioc, max_lt_iff]
  exact differentiableWithinAt_of_derivWithin_ne_zero this

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)
⊢ False

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
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1

Tactic:
rw [(nhds_basis_Ioo _).tendsto_right_iff] at hdiff

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff :
  ∀ (i : ℝ × ℝ),
    i.1 < derivWithin f (Ioi a) a ∧ derivWithin f (Ioi a) a < i.2 → ∀ᶠ (x : ℝ) in 𝓝[>] a, slope f a x ∈ Ioo i.1 i.2
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, (derivWithin f (Ioi a) a + 1) ⊔ 0 < derivWithin f (Ioi a) x
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
⊢ Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop

Tactic:
refine hf.congr' ?_

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
⊢ deriv f =ᶠ[𝓝[>] a] derivWithin f (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
z : ℝ
hz : z ∈ Ioc a b
⊢ 0 < derivWithin f (Ioi a) z

Tactic:
simp_all only [mem_Ioo, and_imp, mem_Ioc, max_lt_iff]

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
z : ℝ
hz : z ∈ Ioc a b
this : derivWithin f (Ioi a) z ≠ 0
⊢ DifferentiableWithinAt ℝ f (Ioi a) z

Tactic:
exact differentiableWithinAt_of_derivWithin_ne_zero this

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a

Tactic:
intro hcontra

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
hcontra : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ False

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 ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z

Tactic:
intro z hz''

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
⊢ ContinuousWithinAt f (Icc a b) z

Proof state:
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)
⊢ False

Tactic:
have hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z := by
  intro z hz''
  refine (hdiff'.continuousOn z hz'').mono_of_mem_nhdsWithin ?_
  have hfinal : 𝓝[Ioc a b] z = 𝓝[Icc a b] z := by
    refine nhdsWithin_eq_nhdsWithin' (s := Ioi a) (Ioi_mem_nhds hz''.1) ?_
    simp only [Ioc_inter_Ioi, le_refl, sup_of_le_left]
    ext y
    exact ⟨fun h => ⟨mem_Icc_of_Ioc h, mem_of_mem_inter_left h⟩, fun ⟨H1, H2⟩ => ⟨H2, H1.2⟩⟩
  rw [← hfinal]
  exact self_mem_nhdsWithin

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)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
⊢ False

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ False

Tactic:
replace hdiff := hdiff.hasDerivWithinAt

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : HasDerivWithinAt f (derivWithin f (Ioi a) a) (Ioi a) a
⊢ False