awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
rw :
  meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x =
    meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x =
    meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x
have rw₁ : meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x =
  meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x
Tactic: rw [meromorphicTrailingCoeffAt_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x ≠ 0
have h₃ : meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x ≠ 0
Tactic: rwa [meromorphicTrailingCoeffAt_neg, ←sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
have pos : ∀ (h₁f₁ : meromorphicOrderAt f₁ x = ⊤),
  meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
Tactic: by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
pos :
  ∀ (h₁f₁ : meromorphicOrderAt f₁ x = ⊤),
    meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
have neg : ∀ (h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤),
  meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
Tactic: by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
have pos : ∀ (h₁f₂ : meromorphicOrderAt f₂ x = ⊤),
  meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
Tactic: by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
pos :
  ∀ (h₁f₂ : meromorphicOrderAt f₂ x = ⊤),
    meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
have neg : ∀ (h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤),
  meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
Tactic: by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
have neg : ∀ (g₁ : 𝕜 → 𝕜) (h₁g₁ : AnalyticAt 𝕜 g₁ x) (h₂g₁ : g₁ x ≠ 0)
  (h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z),
  meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
Tactic: obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_ne_top_iff hf₁).1 h₁f₁
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
have neg : ∀ (g₂ : 𝕜 → E) (h₁g₂ : AnalyticAt 𝕜 g₂ x) (h₂g₂ : g₂ x ≠ 0)
  (h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z),
  meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
Tactic: obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_ne_top_iff hf₂).1 h₁f₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z
⊢ f₁ • f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z
have h : ∀ (y : 𝕜) (h₁y : f₁ y = (y - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ y)
  (h₂y : f₂ y = (y - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ y) (h₃y : Membership.mem (γ := Set 𝕜) {x}ᶜ y),
  (f₁ • f₂) y = (y - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) y
Tactic: filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin] with y h₁y h₂y h₃y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z
y : 𝕜
h₁y : f₁ y = (y - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ y
h₂y : f₂ y = (y - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ y
h₃y : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ (f₁ • f₂) y = (y - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) y
have h : ∀ (h₂g₁ : ¬g₁ x = 0) (h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ * g₁ z)
  (h₁g₂ : AnalyticAt 𝕜 g₂ x) (h₂g₂ : ¬g₂ x = 0)
  (h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z)
  (h₁y : f₁ y = (y - x) ^ (meromorphicOrderAt f₁ x).untop₀ * g₁ y)
  (h₂y : f₂ y = (y - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ y) (h₃y : ¬y = x),
  ((y - x) ^ (meromorphicOrderAt f₁ x).untop₀ * g₁ y) • (y - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ y =
    ((y - x) ^ (meromorphicOrderAt f₁ x).untop₀ * (y - x) ^ (meromorphicOrderAt f₂ x).untop₀) • g₁ y • g₂ y
Tactic: simp_all [meromorphicOrderAt_smul hf₁ hf₂, zpow_add₀ (sub_ne_zero.2 h₃y)]
Cleared hypotheses: h₂g₁, h₃g₁, h₁g₂, h₂g₂, h₃g₂, h₁y, h₂y, h₃y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
have this : f₁ • f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z
Tactic: have : f₁ • f₂ =ᶠ[𝓝[≠] x]
      fun z ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z := by
    filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin] with y h₁y h₂y h₃y
    simp_all [meromorphicOrderAt_smul hf₁ hf₂, zpow_add₀ (sub_ne_zero.2 h₃y)]
    module
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : f₁ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₁ x).untop₀ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f₂ x).untop₀ • g₂ z
this : f₁ • f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
have neg : (g₁ • g₂) x = g₁ x • g₂ x
Tactic: rw [h₁g₁.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g₁ h₃g₁,
    h₁g₂.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g₂ h₃g₂,
    (h₁g₁.smul h₁g₂).meromorphicTrailingCoeffAt_of_eq_nhdsNE this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  ∀ (h : ∀ σ ∈ s₁, MeromorphicAt (f σ) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x) (∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x)
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ insert σ s₁, f n) x)
    (∏ n ∈ insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
have this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
Tactic: have : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x := by
      intro τ hτ
      apply h τ (Finset.mem_insert_of_mem hτ)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  ∀ (h : ∀ σ ∈ s₁, MeromorphicAt (f σ) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x) (∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x)
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ insert σ s₁, f n) x)
    (∏ n ∈ insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
have insert : meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x = ∏ n ∈ insert σ s₁, meromorphicTrailingCoeffAt (f n) x
Tactic: rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  ∀ (h : ∀ σ ∈ s₁, MeromorphicAt (f σ) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x) (∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x)
h : ∀ σ_1 ∈ Insert.insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
insert :
  meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x = ∏ n ∈ Insert.insert σ s₁, meromorphicTrailingCoeffAt (f n) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ Insert.insert σ s₁, f n) x)
    (∏ n ∈ Insert.insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
have insert₁ : meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x =
  meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x
Tactic: rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  ∀ (h : ∀ σ ∈ s₁, MeromorphicAt (f σ) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x) (∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x)
h : ∀ σ_1 ∈ Insert.insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
insert :
  meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x = ∏ n ∈ Insert.insert σ s₁, meromorphicTrailingCoeffAt (f n) x
insert₁ :
  meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x =
    meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ Insert.insert σ s₁, f n) x)
    (∏ n ∈ Insert.insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
have insert₂ : meromorphicTrailingCoeffAt (f σ) x * meromorphicTrailingCoeffAt (∏ i ∈ s₁, f i) x =
  meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x
Tactic: rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  ∀ (h : ∀ σ ∈ s₁, MeromorphicAt (f σ) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x) (∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x)
h : ∀ σ_1 ∈ Insert.insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
insert :
  meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x = ∏ n ∈ Insert.insert σ s₁, meromorphicTrailingCoeffAt (f n) x
insert₁ :
  meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x =
    meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x
insert₂ :
  meromorphicTrailingCoeffAt (f σ) x * meromorphicTrailingCoeffAt (∏ i ∈ s₁, f i) x =
    meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ Insert.insert σ s₁, f n) x)
    (∏ n ∈ Insert.insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
have insert₃ : meromorphicTrailingCoeffAt (f σ) x * ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x =
  meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x
Tactic: rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x) (∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x)
have empty : ∀ (h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (f σ) x),
  Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ ∅, f n) x) (∏ n ∈ ∅, meromorphicTrailingCoeffAt (f n) x)
Tactic: induction s using Finset.induction with
  | empty =>
    apply meromorphicTrailingCoeffAt_const
  | insert σ s₁ hσ hind =>
    have : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x := by
      intro τ hτ
      apply h τ (Finset.mem_insert_of_mem hτ)
    rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
empty :
  ∀ (h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (f σ) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ ∅, f n) x) (∏ n ∈ ∅, meromorphicTrailingCoeffAt (f n) x)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x) (∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x)
have insert : ∀ (σ : ι) (s₁ : Finset ι) (hσ : σ ∉ s₁)
  (hind :
    ∀ (h : ∀ σ ∈ s₁, MeromorphicAt (f σ) x),
      Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x) (∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x))
  (h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x),
  Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ insert σ s₁, f n) x)
    (∏ n ∈ insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
Tactic: induction s using Finset.induction with
  | empty =>
    apply meromorphicTrailingCoeffAt_const
  | insert σ s₁ hσ hind =>
    have : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x := by
      intro τ hτ
      apply h τ (Finset.mem_insert_of_mem hτ)
    rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x) (∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x)
have empty : ∀ (h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (f σ) x),
  Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ ∅, f n) x) (∏ n ∈ ∅, meromorphicTrailingCoeffAt (f n) x)
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    apply meromorphicTrailingCoeffAt_const
  | insert σ s₁ hσ hind =>
    have : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x := by
      intro τ hτ
      apply h τ (Finset.mem_insert_of_mem hτ)
    rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
empty :
  ∀ (h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (f σ) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ ∅, f n) x) (∏ n ∈ ∅, meromorphicTrailingCoeffAt (f n) x)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x) (∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x)
have insert : ∀ (σ : ι) (s₁ : Finset ι) (hσ : σ ∉ s₁)
  (hind :
    ∀ (h : ∀ σ ∈ s₁, MeromorphicAt (f σ) x),
      Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x) (∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x))
  (h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x),
  Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ insert σ s₁, f n) x)
    (∏ n ∈ insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    apply meromorphicTrailingCoeffAt_const
  | insert σ s₁ hσ hind =>
    have : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x := by
      intro τ hτ
      apply h τ (Finset.mem_insert_of_mem hτ)
    rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ ∏ n ∈ s, f n z) x)
    (∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x)
have h₁ : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ n ∈ s, f n x) ((∏ n ∈ s, f n) x)
Tactic: convert! meromorphicTrailingCoeffAt_prod h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
have pos : ∀ (h₁ : MeromorphicAt f x), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
Tactic: by_cases h₁ : MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
pos : ∀ (h₁ : MeromorphicAt f x), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
have neg : ∀ (h₁ : ¬MeromorphicAt f x), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
Tactic: by_cases h₁ : MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
have pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
have neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ f⁻¹ * f =ᶠ[𝓝[≠] x] 1
have h : ∀ (a : 𝕜), f a ≠ 0 → (f⁻¹ * f) a = 1 a
Tactic: filter_upwards [(meromorphicOrderAt_ne_top_iff_eventually_ne_zero h₁).1 h₂]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
have this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
Tactic: have : f⁻¹ * f =ᶠ[𝓝[≠] x] 1 := by
      filter_upwards [(meromorphicOrderAt_ne_top_iff_eventually_ne_zero h₁).1 h₂]
      simp_all