awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
rw : HMul.hMul (α := 𝕜) (↑n : 𝕜) (logDeriv (fun (x : 𝕜) ↦ x) x) = (↑n : 𝕜) / x
⊢ logDeriv (fun (x : 𝕜) ↦ x ^ n) x = (↑n : 𝕜) / x
have rw₁ : (↑n : 𝕜) * (1 / x) = (↑n : 𝕜) / x
Tactic: rw [logDeriv_fun_zpow (by fun_prop), logDeriv_id', mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
rw : HMul.hMul (α := 𝕜) (↑n : 𝕜) (logDeriv (fun (x : 𝕜) ↦ x) x) = (↑n : 𝕜) / x
rw₁ : (↑n : 𝕜) * (1 / x) = (↑n : 𝕜) / x
⊢ logDeriv (fun (x : 𝕜) ↦ x ^ n) x = (↑n : 𝕜) / x
have rw₂ : (↑n : 𝕜) / x = (↑n : 𝕜) / x
Tactic: rw [logDeriv_fun_zpow (by fun_prop), logDeriv_id', mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x
have simp : deriv f (g x) * deriv g x / f (g x) = deriv f (g x) / f (g x) * deriv g x
Tactic: simp only [logDeriv, Pi.div_apply, deriv_comp _ hf hg, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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
⊢ EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
have inl : ∀ (hf : DifferentiableOn 𝕜 f ∅) (hg : DifferentiableOn 𝕜 g ∅)
  (hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hsc : IsPreconnected.{u_1} (α := 𝕜) ∅)
  (hgn : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ∅ x → g x ≠ 0)
  (hfn : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ∅ x → f x ≠ 0),
  EqOn (logDeriv f) (logDeriv g) ∅ ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) ∅
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨t, ht⟩
Cleared hypotheses: s, hf, hg, hs2, hsc, hgn, hfn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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
inl :
  ∀ (hf : DifferentiableOn 𝕜 f ∅) (hg : DifferentiableOn 𝕜 g ∅)
    (hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hsc : IsPreconnected.{u_1} (α := 𝕜) ∅)
    (hgn : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ∅ x → g x ≠ 0)
    (hfn : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ∅ x → f x ≠ 0),
    EqOn (logDeriv f) (logDeriv g) ∅ ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) ∅
⊢ EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
have inr : ∀ (t : 𝕜) (ht : t ∈ s), EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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
⊢ EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
have inr : EqOn (logDeriv f) (logDeriv g) s → ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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
inr : EqOn (logDeriv f) (logDeriv g) s → ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
⊢ EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
have inr₁ : (∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s) → EqOn (logDeriv f) (logDeriv g) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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
⊢ EqOn (logDeriv f) (logDeriv g) s → ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
have inr : ∀ (h : EqOn (logDeriv f) (logDeriv g) s) (y : 𝕜) (hy : y ∈ s), f y = ((f t * (g t)⁻¹) • g) y
Tactic: refine fun h ↦ ⟨f t * (g t)⁻¹, by grind, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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
z : 𝕜
hz : z ∈ s
⊢ deriv (f * g⁻¹) z = (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) z
have rw : deriv f z * g⁻¹ z + f z * deriv g⁻¹ z = (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) z
Tactic: rw [deriv_mul (hf.differentiableAt (hs2.mem_nhds hz)) ((hg.differentiableAt
          (hs2.mem_nhds hz)).inv (hgn z hz))]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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
z : 𝕜
hz : z ∈ s
⊢ deriv f z * g⁻¹ z + f z * deriv g⁻¹ z = (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) z
have simp : deriv f z * (g z)⁻¹ + -(f z * ((HPow.hPow (β := ℕ) (g z) 2)⁻¹ * deriv g z)) =
  deriv f z * (g z)⁻¹ - f z * deriv g z / HPow.hPow (β := ℕ) (g z) 2
Tactic: simp only [Pi.inv_apply, show g⁻¹ = (fun x => x⁻¹) ∘ g by rfl, deriv_inv, neg_mul,
          deriv_comp z (differentiableAt_inv (hgn z hz)) (hg.differentiableAt (hs2.mem_nhds hz)),
          mul_neg, Pi.sub_apply, Pi.mul_apply, comp_apply, Pi.div_apply, Pi.pow_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (hypothesis)
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
⊢ f y = ((f t * (g t)⁻¹) • g) y
have hderiv : EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) s
Tactic: have hderiv : s.EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / g ^ 2) := by
        intro z hz
        rw [deriv_mul (hf.differentiableAt (hs2.mem_nhds hz)) ((hg.differentiableAt
          (hs2.mem_nhds hz)).inv (hgn z hz))]
        simp only [Pi.inv_apply, show g⁻¹ = (fun x => x⁻¹) ∘ g by rfl, deriv_inv, neg_mul,
          deriv_comp z (differentiableAt_inv (hgn z hz)) (hg.differentiableAt (hs2.mem_nhds hz)),
          mul_neg, Pi.sub_apply, Pi.mul_apply, comp_apply, Pi.div_apply, Pi.pow_apply]
        ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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
z : 𝕜
hz : z ∈ s
⊢ (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) z = 0 z
have simp : deriv f z * (g z)⁻¹ - f z * deriv g z / HPow.hPow (β := ℕ) (g z) 2 = 0
Tactic: simp only [Pi.sub_apply, Pi.mul_apply, Pi.inv_apply, Pi.div_apply, Pi.pow_apply,
          Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (hypothesis)
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
⊢ f y = ((f t * (g t)⁻¹) • g) y
have hfg : EqOn (deriv (f * g⁻¹)) 0 s
Tactic: have hfg : EqOn (deriv (f * g⁻¹)) 0 s := hderiv.trans fun z hz ↦ by
        simp only [Pi.sub_apply, Pi.mul_apply, Pi.inv_apply, Pi.div_apply, Pi.pow_apply,
          Pi.zero_apply]
        grind [logDeriv_apply, Pi.div_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (hypothesis)
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 (β := 𝕜) (fun (w : 𝕜) ↦ (w - x) * logDeriv f w) (𝓝[≠] x) (𝓝 1)
have h_slope : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (deriv f x))
Tactic: have h_slope := hasDerivAt_iff_tendsto_slope.mp hf.differentiableAt.hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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 (β := 𝕜) (fun (w : 𝕜) ↦ (w - x) * logDeriv f w) (𝓝[≠] x) (𝓝 1)
have rw : Tendsto (fun (w : 𝕜) ↦ (w - x) * logDeriv f w) (𝓝[≠] x) (𝓝 (deriv f x / deriv f x))
Tactic: rw [← div_self hf']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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 (fun (w : 𝕜) ↦ (w - x) * logDeriv f w) (𝓝[≠] x) (𝓝 (deriv f x / deriv f x))
have h : ∀ (x_1 : 𝕜), (x_1 - x) * logDeriv f x_1 = (deriv f / slope f x) x_1
Tactic: convert! hf.deriv.continuousAt.tendsto.mono_left nhdsWithin_le_nhds |>.div h_slope hf' using 2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
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) * logDeriv f x_1 = (deriv f / slope f x) x_1
have h : (x_1 - x) * (deriv f x_1 / f x_1) = deriv f x_1 / ((x_1 - x)⁻¹ * f x_1)
Tactic: simp [logDeriv, slope, hfx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDerivUniformlyOn (goal)
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
⊢ Eq (α := ℂ) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ι), f i x) x) (∑' (i : ι), logDeriv (f i) x)
have rw : HasSum (α := ℂ) (fun (i : ι) ↦ logDeriv (f i) x) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ι), f i x) x)
Tactic: rw [Eq.comm, ← hm.hasSum_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDerivUniformlyOn (goal)
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
⊢ HasSum (α := ℂ) (fun (i : ι) ↦ logDeriv (f i) x) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ι), f i x) x)
have refine : ∀ (b : Finset ι),
  Eq (α := ℂ) (logDeriv (fun (x2 : ℂ) ↦ ∏ i ∈ b, f i x2) x) (∑ b ∈ b, (fun (i : ι) ↦ logDeriv (f i) x) b)
Tactic: refine logDeriv_tendsto hs hx htend.hasProdLocallyUniformlyOn (.of_forall <| by fun_prop) hnez
    |>.congr fun b ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDerivUniformlyOn (goal)
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 ι
⊢ Eq (α := ℂ) (logDeriv (fun (x2 : ℂ) ↦ ∏ i ∈ b, f i x2) x) (∑ b ∈ b, (fun (i : ι) ↦ logDeriv (f i) x) b)
have rw : Eq (α := ℂ) (∑ i ∈ b, logDeriv (f i) 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))]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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
⊢ Icc a b ⊆ {x : ℝ | f x ≤ B x}
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
have simp : IsClosed (Icc a b ∩ {x : ℝ | f x ≤ B x})
Tactic: simp only [s, inter_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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)
⊢ Icc a b ⊆ {x : ℝ | f x ≤ B x}
have this : IsClosed s
Tactic: have : IsClosed s := by
    simp only [s, inter_comm]
    exact A.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ Icc a b ⊆ {x : ℝ | f x ≤ B x}
have apply : ∀ x ∈ {x : ℝ | f x ≤ B x} ∩ Ico a b, ∀ y ∈ Ioi x, ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
Tactic: apply this.Icc_subset_of_forall_exists_gt ha
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
have inl : ∀ (hxB : f x < B x), ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
Tactic: rcases hxB.lt_or_eq with hxB | hxB
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
have inr : ∀ (hxB : f x = B x), ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
Tactic: rcases hxB.lt_or_eq with hxB | hxB
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
have inl : {x : ℝ | f x ≤ B x} ∈ 𝓝[>] x
Tactic: refine nonempty_of_mem (inter_mem ?_ (Ioc_mem_nhdsGT hy))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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} ∈ 𝓝[>] x
have this₁ : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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 : ℝ | f x ≤ B x} ∈ 𝓝[>] x
have this₁ : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
have inr : ∀ (r : ℝ) (hfr : f' x < r) (hrB : r < B' x), ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
Tactic: rcases exists_between (bound x xab hxB) with ⟨r, hfr, hrB⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
have hf'₁ : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
Tactic: specialize hf' x xab r hfr
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (hypothesis)
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
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
have HB : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.MeanValue (goal)
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
⊢ ({x : ℝ | f x ≤ B x} ∩ Ioc x y).Nonempty
have 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
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