awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
rw :
  ∀ (hf : ∀ (i : ℝ), True → ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv f x ∈ Iic i),
    let f' := f ∘ Neg.neg;
    deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

Tactic:
rw [atBot_basis.tendsto_right_iff] at hf

Premises used: Filter.atBot_basis, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : ∀ (i : ℝ), True → ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv f x ∈ Iic i
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)

Tactic:
specialize hf (-1) trivial

Premises used: trivial, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∀ᶠ (x : ℝ) in 𝓝[<] a, Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
⊢ ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)

Tactic:
rw [(nhdsLT_basis a).eventually_iff] at hf

Premises used: nhdsLT_basis, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
rw : ∃ (i : ℝ), -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

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

Premises used: nhdsGT_basis, Filter.EventuallyEq, Filter.HasBasis.eventually_iff, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
obtain :
  ∀ (b : ℝ) (hb₁ : b < a) (hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)),
    ∃ (i : ℝ), -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x
⊢ ∃ (i : ℝ), -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x

Tactic:
obtain ⟨b, hb₁, hb₂⟩ := hf
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
linarith : -b ≤ -a → b - a + (-b - -a) = 0
⊢ -a < -b

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
refine : ∀ (x : ℝ) (hx : x ∈ Ioo (-a) (-b)), deriv f' x = (-deriv f ∘ Neg.neg) x
⊢ ∃ (i : ℝ), -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x

Tactic:
refine ⟨-b, by linarith, fun x hx => ?_⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
this : deriv f' x = deriv f (-x) * deriv Neg.neg x
⊢ deriv f' x = -deriv f (-x)

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
suffices : deriv f' x = deriv f (-x) * deriv Neg.neg x
⊢ deriv f' x = -deriv f (-x)

Tactic:
suffices deriv f' x = deriv f (-x) * deriv (Neg.neg : ℝ → ℝ) x by simpa using this
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ DifferentiableAt ℝ Neg.neg x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
refine : deriv f (-x) ≠ 0
⊢ deriv f' x = deriv f (-x) * deriv Neg.neg x

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

Premises used: deriv_comp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ -a < x ∧ x < -b

Tactic:
rw [mem_Ioo] at hx

Premises used: Set.mem_Ioo
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : -a < x ∧ x < -b
linarith : -x ≤ b → x - -b + (-x - b) = 0
⊢ b < -x

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : -a < x ∧ x < -b
linarith : a ≤ -x → -a - x + (a - -x) = 0
⊢ -x < a

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : -a < x ∧ x < -b
⊢ -x ∈ Ioo b a

Tactic:
have h₁ : -x ∈ Ioo b a := ⟨by linarith, by linarith⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : -a < x ∧ x < -b
h₁ : -x ∈ Ioo b a
⊢ deriv f (-x) ≤ -1

Tactic:
have h₂ : deriv f (-x) ≤ -1 := hb₂ h₁
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
x : ℝ
hx : -a < x ∧ x < -b
h₁ : -x ∈ Ioo b a
h₂ : deriv f (-x) ≤ -1
linarith : 0 ≤ deriv f (-x) → -1 + (deriv f (-x) - -1) + (0 - deriv f (-x)) = 0
⊢ deriv f (-x) < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
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)

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

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)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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:
not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi f' <| Tendsto.congr' hderiv.symm ?_

Premises used: not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
refine : Tendsto (-deriv f ∘ Neg.neg) (𝓝[>] (-a)) atTop
⊢ ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)

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

Premises used: not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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

Tactic:
Tendsto.comp (g := -deriv f) ?_ tendsto_neg_nhdsGT_neg

Premises used: deriv, tendsto_neg_nhdsGT_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
refine : Tendsto (-deriv f) (𝓝[<] a) atTop
⊢ Tendsto (-deriv f ∘ Neg.neg) (𝓝[>] (-a)) atTop

Tactic:
refine Tendsto.comp (g := -deriv f) ?_ tendsto_neg_nhdsGT_neg

Premises used: tendsto_neg_nhdsGT_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ Tendsto (-deriv f) (𝓝[<] a) atTop

Tactic:
Tendsto.comp (g := Neg.neg) tendsto_neg_atBot_atTop hf

Premises used: Filter.tendsto_neg_atBot_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ Tendsto (-deriv f) (𝓝[<] a) atTop

Tactic:
exact Tendsto.comp (g := Neg.neg) tendsto_neg_atBot_atTop hf

Premises used: Filter.tendsto_neg_atBot_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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:
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
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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:
DifferentiableWithinAt.comp (g := f) (f := Neg.neg) (t := Iio a) (-a) ?_ ?_ ?_

Premises used: DifferentiableWithinAt.comp, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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
refine_1 : DifferentiableWithinAt ℝ f (Iio a) (- -a)
refine_2 : DifferentiableWithinAt ℝ Neg.neg (Ioi (-a)) (-a)
refine_3 : MapsTo Neg.neg (Ioi (-a)) (Iio a)
⊢ DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)

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

Premises used: DifferentiableWithinAt.comp, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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
x : ℝ
⊢ x ∈ Ioi (-a) → -x ∈ Iio a

Tactic:
simp [neg_lt]

Premises used: neg_lt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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:
have : DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a) := by
    refine DifferentiableWithinAt.comp (g := f) (f := Neg.neg) (t := Iio a) (-a) ?_ ?_ ?_
    · simp [h]
    · fun_prop
    · intro x
      simp [neg_lt]
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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:
hmain this
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -deriv f x) (𝓝[<] a) atBot
⊢ Tendsto (deriv (-f)) (𝓝[<] a) atBot

Tactic:
rw [deriv.neg']

Premises used: deriv.neg'
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -deriv f x) (𝓝[<] a) atBot

Tactic:
tendsto_neg_atTop_atBot.comp hf

Premises used: Filter.tendsto_neg_atTop_atBot, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -deriv f x) (𝓝[<] a) atBot

Tactic:
exact tendsto_neg_atTop_atBot.comp hf

Premises used: Filter.tendsto_neg_atTop_atBot, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ Tendsto (deriv (-f)) (𝓝[<] a) atBot

Tactic:
have hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot := by
    rw [deriv.neg']
    exact tendsto_neg_atTop_atBot.comp hf
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot
⊢ False

Tactic:
not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio (-f) hf' h.neg

Premises used: DifferentiableWithinAt.neg, not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot
⊢ False

Tactic:
exact not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio (-f) hf' h.neg

Premises used: DifferentiableWithinAt.neg, not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
⊢ Icc x y ⊆ D

Tactic:
have hxyD : Icc x y ⊆ D := hD.ordConnected.out hx hy
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hxyD : Icc x y ⊆ D
⊢ Ioo x y ⊆ interior D

Tactic:
have hxyD' : Ioo x y ⊆ interior D :=
    subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x)

Tactic:
exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD')

Premises used: ContinuousOn.mono, DifferentiableOn.mono, exists_deriv_eq_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
obtain : ∀ (a : ℝ) (a_mem : a ∈ Ioo x y) (ha : deriv f a = (f y - f x) / (y - x)), C * (y - x) < f y - f x
⊢ C * (y - x) < f y - f x

Tactic:
obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
    exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD')

Premises used: HSub.hSub, ContinuousOn.mono, DifferentiableOn.mono, exists_deriv_eq_slope, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
⊢ C < (f y - f x) / (y - x)

Tactic:
have : C < (f y - f x) / (y - x) := ha ▸ hf'_gt _ (hxyD' a_mem)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
this : C < (f y - f x) / (y - x)
⊢ C * (y - x) < f y - f x

Tactic:
(lt_div_iff₀ (sub_pos.2 hxy)).1 this

Premises used: Iff.mpr, sub_pos, lt_div_iff₀, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
this : C < (f y - f x) / (y - x)
⊢ C * (y - x) < f y - f x

Tactic:
exact (lt_div_iff₀ (sub_pos.2 hxy)).1 this

Premises used: Iff.mpr, sub_pos, lt_div_iff₀, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
hf : Differentiable ℝ f
C : ℝ
hf'_gt : ∀ (x : ℝ), C < deriv f x
x y : ℝ
hxy : x < y
⊢ C * (y - x) < f y - f x

Tactic:
convex_univ.mul_sub_lt_image_sub_of_lt_deriv hf.continuous.continuousOn hf.differentiableOn
    (fun x _ => hf'_gt x) x trivial y trivial hxy

Premises used: Continuous.continuousOn, trivial, convex_univ, Convex.mul_sub_lt_image_sub_of_lt_deriv, Differentiable.differentiableOn, Differentiable.continuous
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
inl : ∀ (hxy' : x = y), C * (y - x) ≤ f y - f x
inr : ∀ (hxy' : x < y), C * (y - x) ≤ f y - f x
⊢ C * (y - x) ≤ f y - f x

Tactic:
rcases eq_or_lt_of_le hxy with hxy' | hxy'

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x = y
inl : C * (y - y) ≤ f y - f y
inl₁ : C * 0 ≤ f y - f y
inl₂ : C * 0 ≤ 0
inl₃ inl₄ : LE.le (α := ℝ) 0 0
⊢ C * (y - x) ≤ f y - f x

Tactic:
rw [hxy', sub_self, sub_self, mul_zero]

Premises used: sub_self, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ D

Tactic:
have hxyD : Icc x y ⊆ D := hD.ordConnected.out hx hy
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
⊢ Ioo x y ⊆ interior D

Tactic:
have hxyD' : Ioo x y ⊆ interior D :=
    subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x)

Tactic:
exists_deriv_eq_slope f hxy' (hf.mono hxyD) (hf'.mono hxyD')

Premises used: ContinuousOn.mono, DifferentiableOn.mono, exists_deriv_eq_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
inr : ∀ (a : ℝ) (a_mem : a ∈ Ioo x y) (ha : deriv f a = (f y - f x) / (y - x)), C * (y - x) ≤ f y - f x
⊢ C * (y - x) ≤ f y - f x

Tactic:
obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
    exists_deriv_eq_slope f hxy' (hf.mono hxyD) (hf'.mono hxyD')

Premises used: HSub.hSub, ContinuousOn.mono, DifferentiableOn.mono, exists_deriv_eq_slope, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
⊢ C ≤ (f y - f x) / (y - x)

Tactic:
have : C ≤ (f y - f x) / (y - x) := ha ▸ hf'_ge _ (hxyD' a_mem)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
this : C ≤ (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x

Tactic:
(le_div_iff₀ (sub_pos.2 hxy')).1 this

Premises used: Iff.mpr, sub_pos, Iff.mp, le_div_iff₀
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
this : C ≤ (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x

Tactic:
exact (le_div_iff₀ (sub_pos.2 hxy')).1 this

Premises used: Iff.mpr, sub_pos, Iff.mp, le_div_iff₀