awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
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, max (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 : max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hx₂ : derivWithin f (Ioi a) x = slope f a b
⊢ False
have hb₁ : derivWithin f (Ioi a) a + 1 < slope f a b ∧ 0 < slope f a b
Tactic: rw [hx₂, max_lt_iff] at hb
Cleared hypotheses: hb, hx₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
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, max (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
have linarith : slope f a b - (derivWithin f (Ioi a) a + 1) + (derivWithin f (Ioi a) a + 1 - slope f a b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
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, max (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
⊢ False
have hcontra : ∀ᶠ (x : ℝ) in 𝓝[>] a, False
Tactic: have hcontra : ∀ᶠ _ in 𝓝[>] a, False := by
      filter_upwards [h₀, h₁, eventually_mem_nhdsWithin] with b hb hslope (hab : a < b)
      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 [and_imp, mem_Ioc, max_lt_iff]
        exact differentiableWithinAt_of_derivWithin_ne_zero this
      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
      have hcont : ContinuousOn f (Icc a b) := by
        intro z hz
        by_cases hz' : z = a
        · rw [hz']
          exact hcont_at_a.mono Icc_subset_Ici_self
        · exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩
      obtain ⟨x, hx₁, hx₂⟩ :=
        exists_deriv_eq_slope' f hab hcont (hdiff'.mono (Ioo_subset_Ioc_self))
      specialize hb x ⟨hx₁.1, le_of_lt hx₁.2⟩
      replace hx₂ : derivWithin f (Ioi a) x = slope f a b := by
        have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx₁.1]
        rwa [derivWithin_of_mem_nhds this]
      rw [hx₂, max_lt_iff] at hb
      linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
case : ∀ (hdiff : DifferentiableWithinAt ℝ f (Ioi a) a), False
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a
have case₁ : ∀ (hdiff : HasDerivWithinAt f (derivWithin f (Ioi a) a) (Ioi a) a), False
Tactic: case pos =>
    intro hdiff
    replace hdiff := hdiff.hasDerivWithinAt
    rw [hasDerivWithinAt_iff_tendsto_slope, Set.diff_singleton_eq_self self_notMem_Ioi] at hdiff
    have h₀ : ∀ᶠ b in 𝓝[>] a,
        ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x := by
      rw [(nhdsGT_basis a).eventually_iff]
      rw [(nhdsGT_basis a).tendsto_left_iff] at hf
      obtain ⟨b, hab, hb⟩ := hf (Ioi (max (derivWithin f (Ioi a) a + 1) 0)) (Ioi_mem_atTop _)
      refine ⟨b, hab, fun x hx z hz => ?_⟩
      simp only [MapsTo, mem_Ioo, mem_Ioi, and_imp] at hb
      exact hb hz.1 <| hz.2.trans_lt hx.2
    have h₁ : ∀ᶠ b in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1 := by
      rw [(nhds_basis_Ioo _).tendsto_right_iff] at hdiff
      specialize hdiff ⟨derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1⟩ <| by simp
      filter_upwards [hdiff] with z hz using hz.2
    have hcontra : ∀ᶠ _ in 𝓝[>] a, False := by
      filter_upwards [h₀, h₁, eventually_mem_nhdsWithin] with b hb hslope (hab : a < b)
      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 [and_imp, mem_Ioc, max_lt_iff]
        exact differentiableWithinAt_of_derivWithin_ne_zero this
      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
      have hcont : ContinuousOn f (Icc a b) := by
        intro z hz
        by_cases hz' : z = a
        · rw [hz']
          exact hcont_at_a.mono Icc_subset_Ici_self
        · exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩
      obtain ⟨x, hx₁, hx₂⟩ :=
        exists_deriv_eq_slope' f hab hcont (hdiff'.mono (Ioo_subset_Ioc_self))
      specialize hb x ⟨hx₁.1, le_of_lt hx₁.2⟩
      replace hx₂ : derivWithin f (Ioi a) x = slope f a b := by
        have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx₁.1]
        rwa [derivWithin_of_mem_nhds this]
      rw [hx₂, max_lt_iff] at hb
      linarith
    simp [Filter.eventually_false_iff_eq_bot, ← notMem_closure_iff_nhdsWithin_eq_bot] at hcontra
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
case : ∀ (hdiff : DifferentiableWithinAt ℝ f (Ioi a) a), False
case₁ : ∀ (hdiff : HasDerivWithinAt f (derivWithin f (Ioi a) a) (Ioi a) a), False
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a
have case₂ : ∀ (hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))), False
Tactic: case pos =>
    intro hdiff
    replace hdiff := hdiff.hasDerivWithinAt
    rw [hasDerivWithinAt_iff_tendsto_slope, Set.diff_singleton_eq_self self_notMem_Ioi] at hdiff
    have h₀ : ∀ᶠ b in 𝓝[>] a,
        ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x := by
      rw [(nhdsGT_basis a).eventually_iff]
      rw [(nhdsGT_basis a).tendsto_left_iff] at hf
      obtain ⟨b, hab, hb⟩ := hf (Ioi (max (derivWithin f (Ioi a) a + 1) 0)) (Ioi_mem_atTop _)
      refine ⟨b, hab, fun x hx z hz => ?_⟩
      simp only [MapsTo, mem_Ioo, mem_Ioi, and_imp] at hb
      exact hb hz.1 <| hz.2.trans_lt hx.2
    have h₁ : ∀ᶠ b in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1 := by
      rw [(nhds_basis_Ioo _).tendsto_right_iff] at hdiff
      specialize hdiff ⟨derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1⟩ <| by simp
      filter_upwards [hdiff] with z hz using hz.2
    have hcontra : ∀ᶠ _ in 𝓝[>] a, False := by
      filter_upwards [h₀, h₁, eventually_mem_nhdsWithin] with b hb hslope (hab : a < b)
      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 [and_imp, mem_Ioc, max_lt_iff]
        exact differentiableWithinAt_of_derivWithin_ne_zero this
      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
      have hcont : ContinuousOn f (Icc a b) := by
        intro z hz
        by_cases hz' : z = a
        · rw [hz']
          exact hcont_at_a.mono Icc_subset_Ici_self
        · exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩
      obtain ⟨x, hx₁, hx₂⟩ :=
        exists_deriv_eq_slope' f hab hcont (hdiff'.mono (Ioo_subset_Ioc_self))
      specialize hb x ⟨hx₁.1, le_of_lt hx₁.2⟩
      replace hx₂ : derivWithin f (Ioi a) x = slope f a b := by
        have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx₁.1]
        rwa [derivWithin_of_mem_nhds this]
      rw [hx₂, max_lt_iff] at hb
      linarith
    simp [Filter.eventually_false_iff_eq_bot, ← notMem_closure_iff_nhdsWithin_eq_bot] at hcontra
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ Tendsto (deriv (-f)) (𝓝[>] a) atTop
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -deriv f x) (𝓝[>] a) atTop
Tactic: rw [deriv.neg']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ False
have hf' : Tendsto (deriv (-f)) (𝓝[>] a) atTop
Tactic: have hf' : Tendsto (deriv (-f)) (𝓝[>] a) atTop := by
    rw [deriv.neg']
    exact tendsto_neg_atBot_atTop.comp hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
have rw : ∀ (hf : ∀ (i : ℝ), True → ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv f x ∈ Iic i),
  let f' := f ∘ Neg.neg;
  deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
Tactic: rw [atBot_basis.tendsto_right_iff] at hf
Cleared hypotheses: hf, f'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : ∀ (i : ℝ), True → ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv f x ∈ Iic i
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
have hf₁ : ∀ᶠ (x : ℝ) in 𝓝[<] a, Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
Tactic: specialize hf (-1) trivial
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∀ᶠ (x : ℝ) in 𝓝[<] a, Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
have hf₁ : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
Tactic: rw [(nhdsLT_basis a).eventually_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → Membership.mem (γ := Set ℝ) (Iic (-1)) (deriv f x)
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
have rw : ∃ (i : ℝ), -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x
Tactic: rw [EventuallyEq, (nhdsGT_basis (-a)).eventually_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
hf : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i 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
have 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
Tactic: obtain ⟨b, hb₁, hb₂⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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)
⊢ -a < -b
have linarith : -b ≤ -a → b - a + (-b - -a) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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)
⊢ ∃ (i : ℝ), -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x
have refine : ∀ (x : ℝ) (hx : x ∈ Ioo (-a) (-b)), deriv f' x = (-deriv f ∘ Neg.neg) x
Tactic: refine ⟨-b, by linarith, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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)
⊢ deriv f' x = -deriv f (-x)
have suffices : deriv f' x = deriv f (-x) * deriv Neg.neg x
Tactic: suffices deriv f' x = deriv f (-x) * deriv (Neg.neg : ℝ → ℝ) x by simpa using this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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)
⊢ deriv f' x = deriv f (-x) * deriv Neg.neg x
have refine : deriv f (-x) ≠ 0
Tactic: refine deriv_comp x (differentiableAt_of_deriv_ne_zero ?_) (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
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)
⊢ deriv f (-x) ≠ 0
have hx₁ : -a < x ∧ x < -b
Tactic: rw [mem_Ioo] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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
⊢ b < -x
have linarith : -x ≤ b → x - -b + (-x - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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 < a
have linarith : a ≤ -x → -a - x + (a - -x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
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
⊢ deriv f (-x) ≠ 0
have h₁ : -x ∈ Ioo b a
Tactic: have h₁ : -x ∈ Ioo b a := ⟨by linarith, by linarith⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
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) ≠ 0
have h₂ : deriv f (-x) ≤ -1
Tactic: have h₂ : deriv f (-x) ≤ -1 := hb₂ h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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
have linarith : 0 ≤ deriv f (-x) → -1 + (deriv f (-x) - -1) + (0 - deriv f (-x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ ¬DifferentiableWithinAt ℝ f (Iio a) a
have hderiv : 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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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)
have refine : Tendsto (-deriv f ∘ Neg.neg) (𝓝[>] (-a)) atTop
Tactic: refine not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi f' <| Tendsto.congr' hderiv.symm ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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
have refine : Tendsto (-deriv f) (𝓝[<] a) atTop
Tactic: refine Tendsto.comp (g := -deriv f) ?_ tendsto_neg_nhdsGT_neg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
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
have hmain : ¬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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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)
have refine_1 : DifferentiableWithinAt ℝ f (Iio a) (- -a)
Tactic: refine DifferentiableWithinAt.comp (g := f) (f := Neg.neg) (t := Iio a) (-a) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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)
⊢ DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
have refine_2 : DifferentiableWithinAt ℝ Neg.neg (Ioi (-a)) (-a)
Tactic: refine DifferentiableWithinAt.comp (g := f) (f := Neg.neg) (t := Iio a) (-a) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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)
⊢ DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
have refine_3 : MapsTo Neg.neg (Ioi (-a)) (Iio a)
Tactic: refine DifferentiableWithinAt.comp (g := f) (f := Neg.neg) (t := Iio a) (-a) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
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
⊢ False
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ Tendsto (deriv (-f)) (𝓝[<] a) atBot
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -deriv f x) (𝓝[<] a) atBot
Tactic: rw [deriv.neg']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ False
have hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot
Tactic: have hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot := by
    rw [deriv.neg']
    exact tendsto_neg_atTop_atBot.comp hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
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
⊢ C * (y - x) < f y - f x
have hxyD : Icc x y ⊆ D
Tactic: have hxyD : Icc x y ⊆ D := hD.ordConnected.out hx hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
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
⊢ C * (y - x) < f y - f x
have hxyD' : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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
⊢ C * (y - x) < f y - f x
have 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
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')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (hypothesis)
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 * (y - x) < f y - f x
have this : C < (f y - f x) / (y - x)
Tactic: have : C < (f y - f x) / (y - x) := ha ▸ hf'_gt _ (hxyD' a_mem)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.MeanValue (goal)
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
⊢ C * (y - x) ≤ f y - f x
have inl : ∀ (hxy' : x = y), C * (y - x) ≤ f y - f x
Tactic: rcases eq_or_lt_of_le hxy with hxy' | hxy'