awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
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
⊢ f₁ • f₂ =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) z

Tactic:
filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin] with y h₁y h₂y h₃y

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
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
⊢ (f₁ • f₂) y = (y - x) ^ (meromorphicOrderAt (f₁ • f₂) x).untop₀ • (g₁ • g₂) y

Tactic:
simp_all [meromorphicOrderAt_smul hf₁ hf₂, zpow_add₀ (sub_ne_zero.2 h₃y)]

Premises used: Iff.mpr, sub_ne_zero, meromorphicOrderAt_smul, zpow_add₀
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
g₂ : 𝕜 → E
y : 𝕜
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:
module
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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

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
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
neg : (g₁ • g₂) x = g₁ x • g₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ 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]

Premises used: AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE, AnalyticAt.smul, AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ (g₁ • g₂) x = g₁ x • g₂ x

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 (fun (z : 𝕜) ↦ f₁ z • f₂ z) x =
    meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_smul hf₁ hf₂

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_smul
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f₁ f₂ : 𝕜 → 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ * f₂) x = meromorphicTrailingCoeffAt f₁ x * meromorphicTrailingCoeffAt f₂ x

Tactic:
meromorphicTrailingCoeffAt_smul hf₁ hf₂

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_smul
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f₁ f₂ : 𝕜 → 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
⊢ meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ f₁ z * f₂ z) x =
    meromorphicTrailingCoeffAt f₁ x * meromorphicTrailingCoeffAt f₂ x

Tactic:
meromorphicTrailingCoeffAt_smul hf₁ hf₂

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_smul
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ (σ : ι), Membership.mem (γ := Finset ι) ∅ σ → MeromorphicAt (f σ) x
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ ∅, f n) x) (∏ n ∈ ∅, meromorphicTrailingCoeffAt (f n) x)

Tactic:
apply meromorphicTrailingCoeffAt_const

Premises used: meromorphicTrailingCoeffAt_const
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
τ : ι
hτ : τ ∈ s₁
⊢ MeromorphicAt (f τ) x

Tactic:
apply h τ (Finset.mem_insert_of_mem hτ)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x

Tactic:
have : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x := by
      intro τ hτ
      apply h τ (Finset.mem_insert_of_mem hτ)
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
insert₃ insert₄ :
  meromorphicTrailingCoeffAt (f σ) x * ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) 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)

Tactic:
rw [Finset.prod_insert hσ, Finset.prod_insert hσ,
      (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this), hind this]

Premises used: Finset.prod_insert, Finset.mem_insert_self, MeromorphicAt.prod, MeromorphicAt.meromorphicTrailingCoeffAt_mul
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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)
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.insert σ s₁, MeromorphicAt (f σ_1) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ Insert.insert σ s₁, f n) x)
      (∏ n ∈ Insert.insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x) (∏ n ∈ 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]

Premises used: Insert.insert, meromorphicTrailingCoeffAt_const
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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)
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.insert σ s₁, MeromorphicAt (f σ_1) x),
    Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ Insert.insert σ s₁, f n) x)
      (∏ n ∈ Insert.insert σ s₁, meromorphicTrailingCoeffAt (f n) x)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x) (∏ n ∈ 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]

Premises used: Insert.insert, meromorphicTrailingCoeffAt_const
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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)

Tactic:
meromorphicTrailingCoeffAt_prod h

Premises used: meromorphicTrailingCoeffAt_prod
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
h₁ : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ n ∈ s, f n x) ((∏ n ∈ s, f n) x)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ ∏ n ∈ s, f n z) x)
    (∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x)

Tactic:
convert! meromorphicTrailingCoeffAt_prod h

Premises used: meromorphicTrailingCoeffAt_prod
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
x_1 : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∏ n ∈ s, f n x_1) ((∏ n ∈ s, f n) x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
pos : ∀ (h₁ : MeromorphicAt f x), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
neg : ∀ (h₁ : ¬MeromorphicAt f x), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
by_cases h₁ : MeromorphicAt f x

Premises used: MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
by_cases h₂ : meromorphicOrderAt f x = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
simp_all [meromorphicOrderAt_inv (f := f) (x := x)]

Premises used: meromorphicOrderAt_inv
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
h : ∀ (a : 𝕜), f a ≠ 0 → (f⁻¹ * f) a = 1 a
⊢ f⁻¹ * f =ᶠ[𝓝[≠] x] 1

Tactic:
filter_upwards [(meromorphicOrderAt_ne_top_iff_eventually_ne_zero h₁).1 h₂]

Premises used: Iff.mp, meromorphicOrderAt_ne_top_iff_eventually_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ ∀ (a : 𝕜), f a ≠ 0 → (f⁻¹ * f) a = 1 a

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ 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
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
neg : Ne.{u_1 + 1} (α := 𝕜) 1 0
neg₁ : (𝓝[≠] x).EventuallyEq (β := 𝕜) 1 fun (z : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - x) 0) 1
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
rw [← mul_eq_one_iff_eq_inv₀ (h₁.meromorphicTrailingCoeffAt_ne_zero h₂),
      ← h₁.inv.meromorphicTrailingCoeffAt_mul h₁, meromorphicTrailingCoeffAt_congr_nhdsNE this,
      analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0)]

Premises used: analyticAt_const, mul_eq_one_iff_eq_inv₀, meromorphicTrailingCoeffAt_congr_nhdsNE, MeromorphicAt.inv, MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero, MeromorphicAt.meromorphicTrailingCoeffAt_mul, AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ Ne.{u_1 + 1} (α := 𝕜) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
neg : (𝓝[≠] x).EventuallyEq (β := 𝕜) 1 fun (z : 𝕜) ↦ 1
⊢ (𝓝[≠] x).EventuallyEq (β := 𝕜) 1 fun (z : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - x) 0) 1

Tactic:
simp only [zpow_zero, smul_eq_mul, mul_one]

Premises used: zpow_zero, smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ (𝓝[≠] x).EventuallyEq (β := 𝕜) 1 fun (z : 𝕜) ↦ 1

Tactic:
eventuallyEq_nhdsWithin_of_eqOn fun _ ↦ congrFun rfl

Premises used: congrFun, rfl, eventuallyEq_nhdsWithin_of_eqOn
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ (𝓝[≠] x).EventuallyEq (β := 𝕜) 1 fun (z : 𝕜) ↦ 1

Tactic:
exact eventuallyEq_nhdsWithin_of_eqOn fun _ ↦ congrFun rfl

Premises used: congrFun, rfl, eventuallyEq_nhdsWithin_of_eqOn
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : ¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
⊢ meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ (f z)⁻¹) x = (meromorphicTrailingCoeffAt f x)⁻¹

Tactic:
meromorphicTrailingCoeffAt_inv

Premises used: meromorphicTrailingCoeffAt_inv
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
by_cases h₂ : meromorphicOrderAt f x = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
pos : ∀ (h₃ : n = 0), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
neg : ∀ (h₃ : ¬n = 0), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
by_cases h₃ : n = 0
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
h₃ : n = 0
pos : Eq (α := 𝕜) (meromorphicTrailingCoeffAt 1 x) 1
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
simp only [h₃, zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
h₃ : n = 0
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt 1 x) 1

Tactic:
apply analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero (ne_zero_of_eq_one rfl)

Premises used: ne_zero_of_eq_one, analyticAt_const, AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero, rfl
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
h₃ : ¬n = 0
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
simp_all [meromorphicOrderAt_zpow h₁, zero_zpow n h₃]

Premises used: zero_zpow, meromorphicOrderAt_zpow
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
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 ^ n) x = meromorphicTrailingCoeffAt f x ^ n
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂

Premises used: meromorphicOrderAt_ne_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬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 ^ n) x ≠ 0

Tactic:
simp_all [zpow_ne_zero]

Premises used: zpow_ne_zero