awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
hhc : ContinuousOn h (Icc a b)
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

Tactic:
exact ⟨c, cmem, sub_eq_zero.1 hc⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
⊢ Tendsto h (𝓝[>] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))

Tactic:
have : Tendsto h (𝓝[>] a) (𝓝 <| (lgb - lga) * lfa - (lfb - lfa) * lga) :=
      (tendsto_const_nhds.mul hfa).sub (tendsto_const_nhds.mul hga)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
this : Tendsto h (𝓝[>] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
⊢ Tendsto h (𝓝[>] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))

Tactic:
this
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
this : Tendsto h (𝓝[>] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
h₁ : lgb * lfa - lfb * lga = (lgb - lga) * lfa - (lfb - lfa) * lga
⊢ Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))

Tactic:
convert! this using 2
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
this : Tendsto h (𝓝[>] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
⊢ lgb * lfa - lfb * lga = (lgb - lga) * lfa - (lfb - lfa) * lga

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
⊢ Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))

Tactic:
have hha : Tendsto h (𝓝[>] a) (𝓝 <| lgb * lfa - lfb * lga) := by
    have : Tendsto h (𝓝[>] a) (𝓝 <| (lgb - lga) * lfa - (lfb - lfa) * lga) :=
      (tendsto_const_nhds.mul hfa).sub (tendsto_const_nhds.mul hga)
    convert! this using 2
    ring
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
⊢ Tendsto h (𝓝[<] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))

Tactic:
have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
      (tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[<] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
⊢ Tendsto h (𝓝[<] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))

Tactic:
this
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[<] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
h₁ : lgb * lfa - lfb * lga = (lgb - lga) * lfb - (lfb - lfa) * lgb
⊢ Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))

Tactic:
convert! this using 2
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[<] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
⊢ lgb * lfa - lfb * lga = (lgb - lga) * lfb - (lfb - lfa) * lgb

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
⊢ Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))

Tactic:
have hhb : Tendsto h (𝓝[<] b) (𝓝 <| lgb * lfa - lfb * lga) := by
    have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
      (tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)
    convert! this using 2
    ring
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x

Tactic:
((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)

Premises used: HasDerivAt.sub, HasDerivAt.const_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x

Tactic:
exact ((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)

Premises used: HasDerivAt.sub, HasDerivAt.const_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
⊢ ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x

Tactic:
have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := by
    intro x hx
    exact ((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
rcases : ∀ (c : ℝ) (cmem : c ∈ Ioo a b) (hc : h' c = 0), ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c

Tactic:
rcases exists_hasDerivAt_eq_zero' hab hha hhb hhh' with ⟨c, cmem, hc⟩

Premises used: exists_hasDerivAt_eq_zero'
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c

Tactic:
⟨c, cmem, sub_eq_zero.1 hc⟩

Premises used: sub_eq_zero, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c

Tactic:
exact ⟨c, cmem, sub_eq_zero.1 hc⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, (b - a) * f' c = (f b - f a) * 1

Tactic:
exists_ratio_hasDerivAt_eq_ratio_slope f f' hab hfc hff' id 1 continuousOn_id
      fun x _ => hasDerivAt_id x

Premises used: id, hasDerivAt_id, exists_ratio_hasDerivAt_eq_ratio_slope, continuousOn_id, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
obtain :
  ∀ (c : ℝ) (cmem : c ∈ Ioo a b) (hc : (b - a) * f' c = (f b - f a) * 1), ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)

Tactic:
obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Ioo a b, (b - a) * f' c = (f b - f a) * 1 :=
    exists_ratio_hasDerivAt_eq_ratio_slope f f' hab hfc hff' id 1 continuousOn_id
      fun x _ => hasDerivAt_id x

Premises used: HSub.hSub, id, hasDerivAt_id, exists_ratio_hasDerivAt_eq_ratio_slope, continuousOn_id, OfNat.ofNat, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
right : f' c = (f b - f a) / (b - a)
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)

Tactic:
use c, cmem
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
right : ∀ (hc : (b - a) * f' c = f b - f a), f' c = (f b - f a) / (b - a)
right₁ : ∀ (hc : f' c * (b - a) = f b - f a), f' c = (f b - f a) / (b - a)
right₂ right₃ right₄ right₅ : ∀ (hc : f' c = (f b - f a) / (b - a)), f' c = (f b - f a) / (b - a)
⊢ f' c = (f b - f a) / (b - a)

Tactic:
rwa [mul_one, mul_comm, ← eq_div_iff (sub_ne_zero.2 hab.ne')] at hc

Premises used: Iff.mpr, sub_ne_zero, LT.lt.ne', mul_comm, mul_one, eq_div_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
g : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
⊢ ∃ c ∈ Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c

Tactic:
exists_ratio_hasDerivAt_eq_ratio_slope f (deriv f) hab hfc
    (fun x hx => ((hfd x hx).differentiableAt <| IsOpen.mem_nhds isOpen_Ioo hx).hasDerivAt) g
    (deriv g) hgc fun x hx =>
    ((hgd x hx).differentiableAt <| IsOpen.mem_nhds isOpen_Ioo hx).hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, DifferentiableWithinAt.differentiableAt, isOpen_Ioo, deriv, exists_ratio_hasDerivAt_eq_ratio_slope, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
g : ℝ → ℝ
lfa lga lfb lgb : ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hdg : DifferentiableOn ℝ g (Ioo a b)
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c

Tactic:
exists_ratio_hasDerivAt_eq_ratio_slope' _ _ hab _ _
    (fun x hx => ((hdf x hx).differentiableAt <| Ioo_mem_nhds hx.1 hx.2).hasDerivAt)
    (fun x hx => ((hdg x hx).differentiableAt <| Ioo_mem_nhds hx.1 hx.2).hasDerivAt) hfa hga hfb hgb

Premises used: DifferentiableAt.hasDerivAt, DifferentiableWithinAt.differentiableAt, Ioo_mem_nhds, And.right, And.left, exists_ratio_hasDerivAt_eq_ratio_slope'
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a)

Tactic:
exists_hasDerivAt_eq_slope f (deriv f) hab hfc fun x hx =>
    ((hfd x hx).differentiableAt <| IsOpen.mem_nhds isOpen_Ioo hx).hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, DifferentiableWithinAt.differentiableAt, isOpen_Ioo, deriv, IsOpen.mem_nhds, exists_hasDerivAt_eq_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
rw : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a)
⊢ ∃ c ∈ Ioo a b, deriv f c = slope f a b

Tactic:
rw [slope_def_field]

Premises used: slope_def_field
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a)

Tactic:
exists_deriv_eq_slope f hab hfc hfd

Premises used: exists_deriv_eq_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a)

Tactic:
exact exists_deriv_eq_slope f hab hfc hfd

Premises used: exists_deriv_eq_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
⊢ Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop

Tactic:
hf.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
refine : deriv f =ᶠ[𝓝[>] a] derivWithin f (Ioi a)
⊢ Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop

Tactic:
refine hf.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
h : ∀ (x : ℝ) (hx : x ∈ Ioi a), deriv f x = derivWithin f (Ioi a) x
⊢ deriv f =ᶠ[𝓝[>] a] derivWithin f (Ioi a)

Tactic:
filter_upwards [eventually_mem_nhdsWithin] with x hx

Premises used: eventually_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
x : ℝ
hx : x ∈ Ioi a
⊢ Ioi a ∈ 𝓝 x

Tactic:
simp [← mem_interior_iff_mem_nhds, hx]

Premises used: mem_interior_iff_mem_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
x : ℝ
hx : x ∈ Ioi a
⊢ Ioi a ∈ 𝓝 x

Tactic:
have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx]
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
x : ℝ
hx : x ∈ Ioi a
this : Ioi a ∈ 𝓝 x
⊢ deriv f x = derivWithin f (Ioi a) x

Tactic:
(derivWithin_of_mem_nhds this).symm

Premises used: Eq.symm, derivWithin_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
x : ℝ
hx : x ∈ Ioi a
this : Ioi a ∈ 𝓝 x
⊢ deriv f x = derivWithin f (Ioi a) x

Tactic:
exact (derivWithin_of_mem_nhds this).symm

Premises used: Eq.symm, derivWithin_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atTop
⊢ Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop

Tactic:
replace hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop := by
    refine hf.congr' ?_
    filter_upwards [eventually_mem_nhdsWithin] with x hx
    have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx]
    exact (derivWithin_of_mem_nhds this).symm
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
by_cases : ∀ (hcont_at_a : ContinuousWithinAt f (Ici a) a), ¬DifferentiableWithinAt ℝ f (Ioi a) a
by_cases₁ : ∀ (hcont_at_a : ¬ContinuousWithinAt f (Ici a) a), ¬DifferentiableWithinAt ℝ f (Ioi a) a
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a

Tactic:
by_cases hcont_at_a : ContinuousWithinAt f (Ici a) a

Premises used: ContinuousWithinAt, Set.Ici
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
hcontra : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ ContinuousWithinAt f (Ioi a) a

Tactic:
have := hcontra.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
hcontra : DifferentiableWithinAt ℝ f (Ioi a) a
this : ContinuousWithinAt f (Ioi a) a
⊢ ¬ContinuousWithinAt f (Ici a \ Ioi a) a

Tactic:
rw [← ContinuousWithinAt.diff_iff this] at hcont_at_a

Premises used: ContinuousWithinAt.diff_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
hcontra : DifferentiableWithinAt ℝ f (Ioi a) a
this : ContinuousWithinAt f (Ioi a) a
hcont_at_a₁ : ¬ContinuousWithinAt f (Ici a \ Ioi a) a
⊢ DifferentiableWithinAt ℝ f (Ioi a) a

Tactic:
rw [← ContinuousWithinAt.diff_iff this] at hcont_at_a

Premises used: ContinuousWithinAt.diff_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
hcontra : DifferentiableWithinAt ℝ f (Ioi a) a
this : ContinuousWithinAt f (Ioi a) a
hcont_at_a₁ : ¬ContinuousWithinAt f (Ici a \ Ioi a) a
hcontra₁ : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ ContinuousWithinAt f (Ioi a) a

Tactic:
rw [← ContinuousWithinAt.diff_iff this] at hcont_at_a

Premises used: ContinuousWithinAt.diff_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a \ Ioi a) a
hcontra : DifferentiableWithinAt ℝ f (Ioi a) a
this : ContinuousWithinAt f (Ioi a) a
⊢ False

Tactic:
simp at hcont_at_a
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ¬ContinuousWithinAt f (Ici a) a
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a

Tactic:
case neg =>
    intro hcontra
    have := hcontra.continuousWithinAt
    rw [← ContinuousWithinAt.diff_iff this] at hcont_at_a
    simp at hcont_at_a
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ HasDerivWithinAt f (derivWithin f (Ioi a) a) (Ioi a) a

Tactic:
replace hdiff := hdiff.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
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
⊢ Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))

Tactic:
rw [hasDerivWithinAt_iff_tendsto_slope, Set.diff_singleton_eq_self self_notMem_Ioi] at hdiff

Premises used: Set.diff_singleton_eq_self, Set.self_notMem_Ioi, hasDerivWithinAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
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))
rw :
  ∃ (i : ℝ),
    a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x

Tactic:
rw [(nhdsGT_basis a).eventually_iff]

Premises used: nhdsGT_basis, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
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))
⊢ ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t

Tactic:
rw [(nhdsGT_basis a).tendsto_left_iff] at hf

Premises used: nhdsGT_basis, Filter.HasBasis.tendsto_left_iff