awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
hderiv : EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) s
hfg : EqOn (deriv (f * g⁻¹)) 0 s
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
a : 𝕜'
ha : ∀ x ∈ s, (f * g⁻¹) x = a
⊢ f y = ((f t * (g t)⁻¹) • g) y

Tactic:
grind [Pi.mul_apply, Pi.inv_apply, Pi.smul_apply, smul_eq_mul]

Premises used: Pi.mul_apply, smul_eq_mul, Pi.inv_apply, Pi.smul_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
z : 𝕜'
hz0 : z ≠ 0
hz : EqOn f (z • g) s
x : 𝕜
hx : x ∈ s
⊢ logDeriv f x = logDeriv g x

Tactic:
simp [logDeriv_apply, hz.deriv hs2 hx, hz hx, deriv_const_smul _
        (hg.differentiableAt (hs2.mem_nhds hx)), mul_div_mul_left (deriv g x) (g x) hz0]

Premises used: deriv_const_smul, deriv, DifferentiableOn.differentiableAt, logDeriv_apply, IsOpen.mem_nhds, mul_div_mul_left, Set.EqOn.deriv
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hfx : f x = 0
hf' : deriv f x ≠ 0
⊢ Tendsto (slope f x) (𝓝[≠] x) (𝓝 (deriv f x))

Tactic:
have h_slope := hasDerivAt_iff_tendsto_slope.mp hf.differentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hfx : f x = 0
hf' : deriv f x ≠ 0
h_slope : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (deriv f x))
rw : Tendsto (fun (w : 𝕜) ↦ (w - x) * logDeriv f w) (𝓝[≠] x) (𝓝 (deriv f x / deriv f x))
⊢ Tendsto (β := 𝕜) (fun (w : 𝕜) ↦ (w - x) * logDeriv f w) (𝓝[≠] x) (𝓝 1)

Tactic:
rw [← div_self hf']

Premises used: div_self
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hfx : f x = 0
hf' : deriv f x ≠ 0
h_slope : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (deriv f x))
⊢ Tendsto (deriv f / slope f x) (𝓝[≠] x) (𝓝 (deriv f x / deriv f x))

Tactic:
hf.deriv.continuousAt.tendsto.mono_left nhdsWithin_le_nhds |>.div h_slope hf'

Premises used: AnalyticAt.deriv, Filter.Tendsto.div, nhdsWithin_le_nhds, ContinuousAt.tendsto, Filter.Tendsto.mono_left, AnalyticAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hfx : f x = 0
hf' : deriv f x ≠ 0
h_slope : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (deriv f x))
h : ∀ (x_1 : 𝕜), (x_1 - x) * logDeriv f x_1 = (deriv f / slope f x) x_1
⊢ Tendsto (fun (w : 𝕜) ↦ (w - x) * logDeriv f w) (𝓝[≠] x) (𝓝 (deriv f x / deriv f x))

Tactic:
convert! hf.deriv.continuousAt.tendsto.mono_left nhdsWithin_le_nhds |>.div h_slope hf' using 2

Premises used: AnalyticAt.deriv, Filter.Tendsto.div, nhdsWithin_le_nhds, ContinuousAt.tendsto, Filter.Tendsto.mono_left, AnalyticAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hfx : f x = 0
hf' : deriv f x ≠ 0
h_slope : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (deriv f x))
x_1 : 𝕜
h : (x_1 - x) * (deriv f x_1 / f x_1) = deriv f x_1 / ((x_1 - x)⁻¹ * f x_1)
⊢ (x_1 - x) * logDeriv f x_1 = (deriv f / slope f x) x_1

Tactic:
simp [logDeriv, slope, hfx]

Premises used: logDeriv, slope
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hfx : f x = 0
hf' : deriv f x ≠ 0
h_slope : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (deriv f x))
x_1 : 𝕜
⊢ (x_1 - x) * (deriv f x_1 / f x_1) = deriv f x_1 / ((x_1 - x)⁻¹ * f x_1)

Tactic:
field
-- Module: Mathlib.Analysis.Calculus.LogDerivUniformlyOn
Goal:
ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable (α := ℂ) fun (i : ι) ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : Ne (α := ℂ) (∏' (i : ι), f i x) 0
rw : HasSum (α := ℂ) (fun (i : ι) ↦ logDeriv (f i) x) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ι), f i x) x)
⊢ Eq (α := ℂ) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ι), f i x) x) (∑' (i : ι), logDeriv (f i) x)

Tactic:
rw [Eq.comm, ← hm.hasSum_iff]

Premises used: Summable.hasSum_iff, Eq.comm
-- Module: Mathlib.Analysis.Calculus.LogDerivUniformlyOn
Goal:
ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable (α := ℂ) fun (i : ι) ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : Ne (α := ℂ) (∏' (i : ι), f i x) 0
⊢ ∀ (x : Finset ι), DifferentiableOn ℂ (F := ℂ) (fun (x2 : ℂ) ↦ ∏ i ∈ x, f i x2) s

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LogDerivUniformlyOn
Goal:
ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable (α := ℂ) fun (i : ι) ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : Ne (α := ℂ) (∏' (i : ι), f i x) 0
refine :
  ∀ (b : Finset ι),
    Eq (α := ℂ) (logDeriv (fun (x2 : ℂ) ↦ ∏ i ∈ b, f i x2) x) (∑ b ∈ b, (fun (i : ι) ↦ logDeriv (f i) x) b)
⊢ HasSum (α := ℂ) (fun (i : ι) ↦ logDeriv (f i) x) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ι), f i x) x)

Tactic:
refine logDeriv_tendsto hs hx htend.hasProdLocallyUniformlyOn (.of_forall <| by fun_prop) hnez
    |>.congr fun b ↦ ?_

Premises used: Complex.logDeriv_tendsto, Filter.Eventually.of_forall, Filter.Tendsto.congr, MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn
-- Module: Mathlib.Analysis.Calculus.LogDerivUniformlyOn
Goal:
ι : Type u_1
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
f : ι → ℂ → ℂ
hf : ∀ (i : ι), f i x ≠ 0
hd : ∀ (i : ι), DifferentiableOn ℂ (f i) s
hm : Summable (α := ℂ) fun (i : ι) ↦ logDeriv (f i) x
htend : MultipliableLocallyUniformlyOn f s
hnez : Ne (α := ℂ) (∏' (i : ι), f i x) 0
b : Finset ι
rw rw₁ : Eq (α := ℂ) (∑ i ∈ b, logDeriv (f i) x) (∑ b ∈ b, (fun (i : ι) ↦ logDeriv (f i) x) b)
⊢ Eq (α := ℂ) (logDeriv (fun (x2 : ℂ) ↦ ∏ i ∈ b, f i x2) x) (∑ b ∈ b, (fun (i : ι) ↦ logDeriv (f i) x) b)

Tactic:
rw [logDeriv_prod (fun i _ ↦ hf i) (fun i _ ↦ (hd i x hx).differentiableAt (hs.mem_nhds hx))]

Premises used: DifferentiableWithinAt.differentiableAt, IsOpen.mem_nhds, logDeriv_prod
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
⊢ ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)

Tactic:
have A : ContinuousOn (fun x => (f x, B x)) (Icc a b) := hf.prodMk hB
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
simp : IsClosed (Icc a b ∩ {x : ℝ | f x ≤ B x})
⊢ IsClosed s

Tactic:
simp only [s, inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {x : ℝ | f x ≤ B x})

Tactic:
A.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, Set.Mem, setOf, OrderClosedTopology.isClosed_le', isClosed_Icc, Set.preimage
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {x : ℝ | f x ≤ B x})

Tactic:
exact A.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, OrderClosedTopology.isClosed_le', isClosed_Icc
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
⊢ IsClosed s

Tactic:
have : IsClosed s := by
    simp only [s, inter_comm]
    exact A.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
apply : ∀ x ∈ {x : ℝ | f x ≤ B x} ∩ Ico a b, ∀ y ∈ Ioi x, ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
⊢ Icc a b ⊆ {x : ℝ | f x ≤ B x}

Tactic:
apply this.Icc_subset_of_forall_exists_gt ha

Premises used: IsClosed.Icc_subset_of_forall_exists_gt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
inl : ∀ (hxB : f x < B x), ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
inr : ∀ (hxB : f x = B x), ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
rcases hxB.lt_or_eq with hxB | hxB

Premises used: LE.le.lt_or_eq
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
nonempty_of_mem (inter_mem ?_ (Ioc_mem_nhdsGT hy))

Premises used: Filter.inter_mem, Ioc_mem_nhdsGT, Filter.nonempty_of_mem
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
inl : {x : ℝ | f x ≤ B x} ∈ 𝓝[>] x
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
refine nonempty_of_mem (inter_mem ?_ (Ioc_mem_nhdsGT hy))
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x

Tactic:
have : ∀ᶠ x in 𝓝[Icc a b] x, f x < B x :=
      A x (Ico_subset_Icc_self xab) (IsOpen.mem_nhds (isOpen_lt continuous_fst continuous_snd) hxB)
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
this : ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x < B x

Tactic:
have : ∀ᶠ x in 𝓝[>] x, f x < B x := nhdsWithin_le_of_mem (Icc_mem_nhdsGT_of_mem xab) this
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
this_2 : ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x
this : ∀ᶠ (x : ℝ) in 𝓝[>] x, f x < B x
⊢ {x : ℝ | f x ≤ B x} ∈ 𝓝[>] x

Tactic:
this.mono fun y => le_of_lt

Premises used: Set.Mem, Filter.Eventually, setOf, le_of_lt, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
this_2 : ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x
this : ∀ᶠ (x : ℝ) in 𝓝[>] x, f x < B x
⊢ {x : ℝ | f x ≤ B x} ∈ 𝓝[>] x

Tactic:
exact this.mono fun y => le_of_lt

Premises used: le_of_lt, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
inr : ∀ (r : ℝ) (hfr : f' x < r) (hrB : r < B' x), ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
rcases exists_between (bound x xab hxB) with ⟨r, hfr, hrB⟩

Premises used: exists_between
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r

Tactic:
specialize hf' x xab r hfr
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z

Tactic:
have HB : ∀ᶠ z in 𝓝[>] x, r < slope B x z :=
      (hasDerivWithinAt_iff_tendsto_slope' <| lt_irrefl x).1 (hB' x xab).Ioi_of_Ici
        (Ioi_mem_nhds hrB)
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
⊢ ∃ (z : ℝ), slope f x z < r ∧ r < slope B x z ∧ z ∈ Ioc x y

Tactic:
hf'.and_eventually (HB.and (Ioc_mem_nhdsGT hy)) |>.exists

Premises used: Set.Ioc, Set.Mem, setOf, Filter.Eventually.and, Ioc_mem_nhdsGT, Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
inr :
  ∀ (z : ℝ) (hfz : slope f x z < r) (hzB : r < slope B x z) (hz : z ∈ Ioc x y), ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
obtain ⟨z, hfz, hzB, hz⟩ : ∃ z, slope f x z < r ∧ r < slope B x z ∧ z ∈ Ioc x y :=
      hf'.and_eventually (HB.and (Ioc_mem_nhdsGT hy)) |>.exists

Premises used: Set.Ioc, Filter.Eventually.and, Ioc_mem_nhdsGT, Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
⟨z, ?_, hz⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
inr : Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
refine ⟨z, ?_, hz⟩
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ slope f x z ≤ slope B x z

Tactic:
have := (hfz.trans hzB).le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x : ℝ | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (Y := ℝ × ℝ) (fun (x : ℝ) ↦ (f x, B x)) (Icc a b)
this_1 : IsClosed s
x : ℝ
hxB_1 : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : slope f x z ≤ slope B x z
inr : ∀ (this : (f z - f x) / (z - x) ≤ slope B x z), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₁ : ∀ (this : (f z - f x) / (z - x) ≤ (B z - B x) / (z - x)), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₂ : ∀ (this : f z - f x ≤ B z - B x), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₃ : ∀ (this : f z - B x ≤ B z - B x), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
inr₄ inr₅ inr₆ inr₇ : ∀ (this : f z ≤ B z), Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | f x ≤ B x} z

Tactic:
rwa [slope_def_field, slope_def_field, div_le_div_iff_of_pos_right (sub_pos.2 hz.1), hxB,
      sub_le_sub_iff_right] at this

Premises used: Iff.mpr, sub_pos, sub_le_sub_iff_right, div_le_div_iff_of_pos_right, slope_def_field, And.left