-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio (f : ℝ → ℝ) {a : ℝ}
    (hf : Tendsto (deriv f) (𝓝[<] a) atBot) : ¬ DifferentiableWithinAt ℝ f (Iio a) a

Proof state:
case intro.intro
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : -a < x ∧ x < -b
h₁ : -x ∈ Ioo b a
h₂ : deriv f (-x) ≤ -1
⊢ deriv f (-x) ≠ 0

Tactic:
exact ne_of_lt (by linarith)

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
hf : ∀ (i : ℝ), True → ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv f x ∈ Iic i
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

Tactic:
specialize hf (-1) trivial

Result:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv f x ∈ Iic (-1)
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

Proof state:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : -a < x ∧ x < -b
⊢ -x < a

Tactic:
linarith

Result:
no goals

Proof state:
case refine_2
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ DifferentiableWithinAt ℝ Neg.neg (Ioi (-a)) (-a)

Tactic:
fun_prop

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
⊢ -a < -b

Tactic:
linarith

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
h : DifferentiableWithinAt ℝ f (Iio a) a
this : DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
⊢ False

Tactic:
exact hmain this

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → deriv f x ∈ Iic (-1)
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

Tactic:
rw [EventuallyEq, (nhdsGT_basis (-a)).eventually_iff]

Result:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → deriv f x ∈ Iic (-1)
⊢ ∃ i, -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

Tactic:
rw [atBot_basis.tendsto_right_iff] at hf

Result:
f : ℝ → ℝ
a : ℝ
hf : ∀ (i : ℝ), True → ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv f x ∈ Iic i
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

Proof state:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ DifferentiableAt ℝ Neg.neg x

Tactic:
fun_prop

Result:
no goals

Proof state:
case intro.intro
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ deriv f' x = (-deriv f ∘ Neg.neg) x

Tactic:
simp only [Pi.neg_apply, Function.comp_apply]

Result:
case intro.intro
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ deriv f' x = -deriv f (-x)

Proof state:
case intro.intro
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
⊢ ∃ i, -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x

Tactic:
refine ⟨-b, by linarith, fun x hx => ?_⟩

Result:
case intro.intro
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ deriv f' x = (-deriv f ∘ Neg.neg) x

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)

Tactic:
refine DifferentiableWithinAt.comp (g := f) (f := Neg.neg) (t := Iio a) (-a) ?_ ?_ ?_

Result:
case refine_1
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ DifferentiableWithinAt ℝ f (Iio a) (- -a)

case refine_2
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ DifferentiableWithinAt ℝ Neg.neg (Ioi (-a)) (-a)

case refine_3
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ MapsTo Neg.neg (Ioi (-a)) (Iio a)

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)

Tactic:
refine not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi f' <| Tendsto.congr' hderiv.symm ?_

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ Tendsto (-deriv f ∘ Neg.neg) (𝓝[>] (-a)) atTop

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ ¬DifferentiableWithinAt ℝ f (Iio a) a

Tactic:
have hmain : ¬ DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a) := by
  refine not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi f' <| Tendsto.congr' hderiv.symm ?_
  refine Tendsto.comp (g := -deriv f) ?_ tendsto_neg_nhdsGT_neg
  exact Tendsto.comp (g := Neg.neg) tendsto_neg_atBot_atTop hf

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
⊢ ¬DifferentiableWithinAt ℝ f (Iio a) a

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ ¬DifferentiableWithinAt ℝ f (Iio a) a

Tactic:
have hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -(deriv f ∘ Neg.neg) := by
  rw [atBot_basis.tendsto_right_iff] at hf
  specialize hf (-1) trivial
  rw [(nhdsLT_basis a).eventually_iff] at hf
  rw [EventuallyEq, (nhdsGT_basis (-a)).eventually_iff]
  obtain ⟨b, hb₁, hb₂⟩ := hf
  refine ⟨-b, by linarith, fun x hx => ?_⟩
  simp only [Pi.neg_apply, Function.comp_apply]
  suffices deriv f' x = deriv f (-x) * deriv (Neg.neg : ℝ → ℝ) x by simpa using this
  refine deriv_comp x (differentiableAt_of_deriv_ne_zero ?_) (by fun_prop)
  rw [mem_Ioo] at hx
  have h₁ : -x ∈ Ioo b a := ⟨by linarith, by linarith⟩
  have h₂ : deriv f (-x) ≤ -1 := hb₂ h₁
  exact ne_of_lt (by linarith)

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ ¬DifferentiableWithinAt ℝ f (Iio a) a

Proof state:
case intro.intro
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ deriv f' x = deriv f (-x) * deriv Neg.neg x

Tactic:
refine deriv_comp x (differentiableAt_of_deriv_ne_zero ?_) (by fun_prop)

Result:
case intro.intro
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ deriv f (-x) ≠ 0

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
⊢ ¬DifferentiableWithinAt ℝ f (Iio a) a

Tactic:
let f' := f ∘ Neg.neg

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ ¬DifferentiableWithinAt ℝ f (Iio a) a