awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (hypothesis)
Goal:
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + HSMul.hSMul (β := ℝ) t 1 ∈ s
have h₁ : ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s
Tactic: rw [mem_closure_iff_frequently, ← map_add_left_nhds_zero, frequently_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a ↔ ∃ᶠ (x : ℝ) in 𝓝[>] a, x ∈ s
have rw : (∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∩ Ioi a) ↔ ∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∧ x ∈ Ioi a
Tactic: rw [one_mem_posTangentConeAt_iff_mem_closure, mem_closure_iff_frequently,
    frequently_nhdsWithin_iff, inter_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
have inl : ∀ (hp' : Eq (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])),
  p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
Tactic: rcases eq_or_ne (derivative p) 0 with hp' | hp'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
inl :
  ∀ (hp' : Eq (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])),
    p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
have inr : ∀ (hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])),
  p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
Tactic: rcases eq_or_ne (derivative p) 0 with hp' | hp'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
hp' : Eq (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
have inl : Finset.card (α := ℝ) (Multiset.toFinset (roots ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) ≤
  Finset.card (α := ℝ)
      (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) \
        Multiset.toFinset (roots ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) +
    1
Tactic: rw [eq_C_of_derivative_eq_zero hp']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (hypothesis)
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
have hp : p ≠ 0
Tactic: have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
have inr : ∀ (x : ℝ) (hx : x ∈ p.roots.toFinset) (y : ℝ) (hy : y ∈ p.roots.toFinset) (hxy : x < y)
  (hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y),
  ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
Tactic: refine Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : x ∈ p.roots.toFinset
y : ℝ
hy : y ∈ p.roots.toFinset
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
⊢ ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
have inr : ∀ (hx : p.IsRoot x) (y : ℝ) (hy : p.IsRoot y) (hxy : x < y) (hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y),
  ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
Tactic: rw [Multiset.mem_toFinset, mem_roots hp] at hx hy
Cleared hypotheses: hx, y, hy, hxy, hxy'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
⊢ ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
have inr : ∀ (z : ℝ) (hz1 : z ∈ Set.Ioo x y) (hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0),
  ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
Tactic: obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0
⊢ ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
have inr : Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z
Tactic: refine ⟨z, ?_, hz1⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0
⊢ Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z
have inr : Membership.mem (γ := Multiset ℝ) (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) z
Tactic: rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0
inr : Membership.mem (γ := Multiset ℝ) (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) z
⊢ Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z
have inr₁ : IsRoot ((derivative : (a : ℝ[X]) → ℝ[X]) p) z
Tactic: rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0
inr : Membership.mem (γ := Multiset ℝ) (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) z
inr₁ : IsRoot ((derivative : (a : ℝ[X]) → ℝ[X]) p) z
⊢ Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z
have inr₂ : eval z ((derivative : (a : ℝ[X]) → ℝ[X]) p) = 0
Tactic: rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
⊢ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1 ≤
    Finset.card (α := ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) + 1
have grw : Finset.card (α := ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) + 1 ≤
  Finset.card (α := ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) + 1
Tactic: grw [Finset.sdiff_subset]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, rootMultiplicity x ((derivative : (a : ℝ[X]) → ℝ[X]) p) +
      ((Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ)
        (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset,
          Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)))
        1
have simp : ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
    HAdd.hAdd (α := ℕ) (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset, 1) 1 ≤
  ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
    HAdd.hAdd (α := ℕ)
      (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset,
        Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)))
      1
Tactic: simp only [← count_roots, Finset.card_eq_sum_ones]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ) (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset, 1)
        1 ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ)
        (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset,
          Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)))
        1
have bc : ∀ (x : ℝ) (hx : x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset),
  1 ≤ Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))
Tactic: gcongr with x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset
⊢ 1 ≤ Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))
have bc : Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) x
Tactic: rw [Nat.succ_le_iff, Multiset.count_pos, ← Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Polynomial (goal)
Goal:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ)
        (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset,
          Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)))
        1 =
    Multiset.card (α := ℝ) (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) + 1
have rw : ∀ x ∈ p.roots.toFinset ∪ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)),
  x ∉ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) →
    Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) = 0
Tactic: rw [← add_assoc, ← Finset.sum_union Finset.disjoint_sdiff, Finset.union_sdiff_self_eq_union, ←
        Multiset.toFinset_sum_count_eq, ← Finset.sum_subset Finset.subset_union_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Rolle (goal)
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
⊢ ∃ c ∈ Ioo a b, deriv f c = 0
have pos : ∀ (h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x), ∃ c ∈ Ioo a b, deriv f c = 0
Tactic: by_cases! h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Rolle (goal)
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
pos : ∀ (h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x), ∃ c ∈ Ioo a b, deriv f c = 0
⊢ ∃ c ∈ Ioo a b, deriv f c = 0
have neg : ∀ (h : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x), ∃ c ∈ Ioo a b, deriv f c = 0
Tactic: by_cases! h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Rolle (goal)
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
⊢ ∃ c ∈ Ioo a b, deriv f c = 0
have neg : ∀ (c : ℝ) (hc : c ∈ Ioo a b) (hcdiff : ¬DifferentiableAt ℝ f c), ∃ c ∈ Ioo a b, deriv f c = 0
Tactic: obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x := h
Cleared hypotheses: h
-- 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 𝕜 𝕜'
a : 𝕜'
⊢ Eq (α := (x : 𝕜) → 𝕜') (logDeriv fun (x : 𝕜) ↦ a) 0
have h : ∀ (x : 𝕜), Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ a) x) (0 x)
Tactic: ext
-- 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 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : ∀ i ∈ Finset.cons a s ha, f i x ≠ 0
hd : ∀ i ∈ Finset.cons a s ha, DifferentiableAt 𝕜 (f i) x
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ Finset.cons a s ha, f i x) x)
    (∑ i ∈ Finset.cons a s ha, logDeriv (f i) x)
have hf₁ : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
Tactic: rw [Finset.forall_mem_cons] at hf hd
Cleared hypotheses: hf, hd
-- 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 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : ∀ i ∈ Finset.cons a s ha, f i x ≠ 0
hd : ∀ i ∈ Finset.cons a s ha, DifferentiableAt 𝕜 (f i) x
hf₁ : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ Finset.cons a s ha, f i x) x)
    (∑ i ∈ Finset.cons a s ha, logDeriv (f i) x)
have hd₁ : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
Tactic: rw [Finset.forall_mem_cons] at hf hd
Cleared hypotheses: hf, hd
-- 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 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ Finset.cons a s ha, f i x) x)
    (∑ i ∈ Finset.cons a s ha, logDeriv (f i) x)
have cons : logDeriv (fun (x : 𝕜) ↦ f a x * ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x
Tactic: simp_rw [Finset.prod_cons, Finset.sum_cons]
-- 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 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ logDeriv (fun (x : 𝕜) ↦ f a x * ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x
have cons : f a x ≠ 0
Tactic: rw [logDeriv_mul, ih hf.2 hd.2]
-- 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 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
cons : f a x ≠ 0
⊢ logDeriv (fun (x : 𝕜) ↦ f a x * ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x
have cons₁ : Ne.{u_2 + 1} (α := 𝕜') (∏ i ∈ s, f i x) 0
Tactic: rw [logDeriv_mul, ih hf.2 hd.2]
-- 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 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
cons : f a x ≠ 0
cons₁ : Ne.{u_2 + 1} (α := 𝕜') (∏ i ∈ s, f i x) 0
⊢ logDeriv (fun (x : 𝕜) ↦ f a x * ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x
have cons₂ : DifferentiableAt 𝕜 (f a) x
Tactic: rw [logDeriv_mul, ih hf.2 hd.2]
-- 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 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
cons : f a x ≠ 0
cons₁ : Ne.{u_2 + 1} (α := 𝕜') (∏ i ∈ s, f i x) 0
cons₂ : DifferentiableAt 𝕜 (f a) x
⊢ logDeriv (fun (x : 𝕜) ↦ f a x * ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x
have cons₃ : DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x
Tactic: rw [logDeriv_mul, ih hf.2 hd.2]
-- 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 𝕜 𝕜'
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ i ∈ s, f i x ≠ 0
hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i x ≠ 0)
  (hd : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → DifferentiableAt 𝕜 (f i) x),
  Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ ∅, f i x) x) (∑ i ∈ ∅, logDeriv (f i) x)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    rw [Finset.forall_mem_cons] at hf hd
    simp_rw [Finset.prod_cons, Finset.sum_cons]
    rw [logDeriv_mul, ih hf.2 hd.2]
    · exact hf.1
    · simpa [Finset.prod_eq_zero_iff] using hf.2
    · exact hd.1
    · exact .fun_finsetProd hd.2
Cleared hypotheses: s, hf, hd
-- 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 𝕜 𝕜'
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ i ∈ s, f i x ≠ 0
hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i x ≠ 0)
    (hd : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ ∅, f i x) x) (∑ i ∈ ∅, logDeriv (f i) x)
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
      Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x))
  (hf : ∀ i ∈ Finset.cons a s ha, f i x ≠ 0) (hd : ∀ i ∈ Finset.cons a s ha, DifferentiableAt 𝕜 (f i) x),
  Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ Finset.cons a s ha, f i x) x)
    (∑ i ∈ Finset.cons a s ha, logDeriv (f i) x)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    rw [Finset.forall_mem_cons] at hf hd
    simp_rw [Finset.prod_cons, Finset.sum_cons]
    rw [logDeriv_mul, ih hf.2 hd.2]
    · exact hf.1
    · simpa [Finset.prod_eq_zero_iff] using hf.2
    · exact hd.1
    · exact .fun_finsetProd hd.2
Cleared hypotheses: s, hf, hd
-- 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 : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
have inl : logDeriv (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) (f x) 0) x = (↑0 : 𝕜') * logDeriv f x
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- 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 : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
inl : logDeriv (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) (f x) 0) x = (↑0 : 𝕜') * logDeriv f x
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
have inr : ∀ (hn : n ≠ 0), logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- 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 : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
have inr : ∀ (hf : f x = 0), logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
Tactic: rcases eq_or_ne (f x) 0 with hf | hf
-- 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 : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
inr : ∀ (hf : f x = 0), logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
have inr₁ : ∀ (hf : f x ≠ 0), logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
Tactic: rcases eq_or_ne (f x) 0 with hf | hf
-- 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 : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
have inr : (↑n : 𝕜') * f x ^ (n - 1) * deriv f x / f x ^ n = (↑n : 𝕜') * (deriv f x / f x)
Tactic: rw [logDeriv_apply, ← comp_def (· ^ n), deriv_comp _ (differentiableAt_zpow.2 <| .inl hf) hdf,
      deriv_zpow, logDeriv_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LogDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ logDeriv (fun (x : 𝕜) ↦ x ^ n) x = (↑n : 𝕜) / x
have rw : HMul.hMul (α := 𝕜) (↑n : 𝕜) (logDeriv (fun (x : 𝕜) ↦ x) x) = (↑n : 𝕜) / x
Tactic: rw [logDeriv_fun_zpow (by fun_prop), logDeriv_id', mul_one_div]