awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
⊢ Eq (α := 𝕜) ((∏ i ∈ Finite.toFinset (s := support d) h, HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - i) (d i)) x)
    (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ d i)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x u : 𝕜
h₁ : u ∉ (↑(Finite.toFinset (s := support d) h) : Set 𝕜) → u ∉ Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u
⊢ Membership.mem (γ := Set 𝕜) (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) u →
    u ∈ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)

Tactic:
contrapose
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x u : 𝕜
⊢ u ∉ (↑(Finite.toFinset (s := support d) h) : Set 𝕜) → u ∉ Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
⊢ (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) h) : Set 𝕜)

Tactic:
simp [mulSupport d]

Premises used: Function.FactorizedRational.mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
h₁ : ∀ (a : 𝕜), AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - a) (d a)) x
⊢ AnalyticAt 𝕜 (F := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x

Tactic:
apply analyticAt_finprod

Premises used: analyticAt_finprod
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
pos : ∀ (h₂ : x = u), AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
neg : ∀ (h₂ : ¬x = u), AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x

Tactic:
by_cases h₂ : x = u
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : x = u
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x - u) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : x = u
pos : 0 ≤ d u
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x

Tactic:
apply AnalyticAt.fun_zpow_nonneg (by fun_prop)

Premises used: AnalyticAt.fun_zpow_nonneg
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : x = u
pos pos₁ pos₂ pos₃ : 0 ≤ d x
⊢ 0 ≤ d u

Tactic:
rwa [← h₂]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : ¬x = u
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x - u) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : ¬x = u
neg : x - u ≠ 0
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x

Tactic:
apply AnalyticAt.fun_zpow (by fun_prop)

Premises used: AnalyticAt.fun_zpow
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : ¬x = u
neg neg₁ neg₂ neg₃ : x ≠ u
⊢ x - u ≠ 0

Tactic:
rwa [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
pos :
  ∀ (h₁ : HasFiniteMulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)),
    Ne.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) 0
neg :
  ∀ (h₁ : ¬HasFiniteMulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)),
    Ne.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) 0
⊢ Ne.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) 0

Tactic:
by_cases h₁ : (fun u ↦ (· - u) ^ d u).HasFiniteMulSupport

Premises used: Function.HasFiniteMulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)
pos :
  ∀
    a ∈
      Finite.toFinset (s :=
        Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) h₁,
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - a) (d a) x ≠ 0
⊢ Ne.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) 0

Tactic:
rw [finprod_eq_prod _ h₁, Finset.prod_apply, Finset.prod_ne_zero_iff]

Premises used: Finset.prod_apply, Finset.prod_ne_zero_iff, finprod_eq_prod
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)
z : 𝕜
hz :
  z ∈
    Finite.toFinset (s :=
      Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) h₁
pos : ¬(x - z) ^ d z = 0
⊢ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) x ≠ 0

Tactic:
simp only [Pi.pow_apply, ne_eq]

Premises used: ne_eq, Pi.pow_apply
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)
z : 𝕜
hz :
  z ∈
    Finite.toFinset (s :=
      Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) h₁
pos : ∀ (h₂ : x = z), ¬(x - z) ^ d z = 0
neg : ∀ (h₂ : ¬x = z), ¬(x - z) ^ d z = 0
⊢ ¬(x - z) ^ d z = 0

Tactic:
by_cases h₂ : x = z
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)
z : 𝕜
hz :
  z ∈
    Finite.toFinset (s :=
      Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) h₁
h₂ : x = z
⊢ ¬(x - z) ^ d z = 0

Tactic:
simp_all [zpow_ne_zero, sub_ne_zero]

Premises used: sub_ne_zero, zpow_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)
z : 𝕜
hz :
  z ∈
    Finite.toFinset (s :=
      Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) h₁
h₂ : ¬x = z
⊢ ¬(x - z) ^ d z = 0

Tactic:
simp_all [zpow_ne_zero, sub_ne_zero]

Premises used: sub_ne_zero, zpow_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : ¬HasFiniteMulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)
⊢ Ne.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) 0

Tactic:
simp [finprod_of_infinite_mulSupport h₁]

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
pos :
  ∀ (h₁d : d u₀ = 0),
    ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) =
      HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
        ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)
neg :
  ∀ (h₁d : ¬d u₀ = 0),
    ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) =
      HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
        ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)
⊢ ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) =
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)

Tactic:
by_cases h₁d : d u₀ = 0
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : d u₀ = 0
⊢ ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) =
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)

Tactic:
simp [← eq_update_self_iff.2 h₁d, h₁d]

Premises used: Iff.mpr, Function.eq_update_self_iff
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
⊢ (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)

Tactic:
simp [mulSupport]

Premises used: Function.FactorizedRational.mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
⊢ (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)

Tactic:
have : (fun u ↦ (fun x ↦ x - u) ^ d u).mulSupport ⊆ hd.toFinset := by
      simp [mulSupport]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
neg :
  ∏ i ∈ Finite.toFinset (s := support d) hd, HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - i) (d i) =
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)
⊢ ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) =
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _ this]

Premises used: finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
⊢ u₀ ∈ Finite.toFinset (s := support d) hd

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
⊢ u₀ ∈ Finite.toFinset (s := support d) hd

Tactic:
have : u₀ ∈ hd.toFinset := by simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this_1 :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
this : u₀ ∈ Finite.toFinset (s := support d) hd
neg :
  HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ x ∈ (Finite.toFinset (s := support d) hd).erase u₀,
        HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (d x) =
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)
⊢ ∏ i ∈ Finite.toFinset (s := support d) hd, HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - i) (d i) =
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)

Tactic:
rw [← Finset.mul_prod_erase hd.toFinset _ this]

Premises used: Finset.mul_prod_erase, Set.Finite.toFinset
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this_1 :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
this : u₀ ∈ Finite.toFinset (s := support d) hd
neg :
  Eq (α := (x : 𝕜) → 𝕜)
    (∏ x ∈ (Finite.toFinset (s := support d) hd).erase u₀, HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (d x))
    (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u))
⊢ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ x ∈ (Finite.toFinset (s := support d) hd).erase u₀,
        HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (d x) =
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u₀) (d u₀) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this_1 :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
this : u₀ ∈ Finite.toFinset (s := support d) hd
rw : support (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0) ⊆ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
⊢ (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦
      HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)) ⊆
    (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)

Tactic:
rw [mulSupport]

Premises used: Function.FactorizedRational.mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this_1 :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
this : u₀ ∈ Finite.toFinset (s := support d) hd
x : 𝕜
hx : x ∈ support (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0)
pos : ∀ (h₁x : x = u₀), x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
neg : ∀ (h₁x : ¬x = u₀), x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
⊢ x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)

Tactic:
by_cases h₁x : x = u₀
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this_1 :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
this : u₀ ∈ Finite.toFinset (s := support d) hd
x : 𝕜
hx : x ∈ support (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0)
h₁x : x = u₀
⊢ x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this_1 :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
this : u₀ ∈ Finite.toFinset (s := support d) hd
x : 𝕜
hx : x ∈ support (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0)
h₁x : ¬x = u₀
⊢ x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this_1 :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
this : u₀ ∈ Finite.toFinset (s := support d) hd
⊢ (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦
      HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)) ⊆
    (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)

Tactic:
have : (fun u ↦ (· - u) ^ (update d u₀ 0 u)).mulSupport ⊆ hd.toFinset.erase u₀ := by
      rw [mulSupport]
      intro x hx
      by_cases h₁x : x = u₀ <;> simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this_1 :
  (Function.mulSupport (M := (x : 𝕜) → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) hd) : Set 𝕜)
this_2 : u₀ ∈ Finite.toFinset (s := support d) hd
this :
  (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦
      HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u)) ⊆
    (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
⊢ Eq (α := (x : 𝕜) → 𝕜)
    (∏ x ∈ (Finite.toFinset (s := support d) hd).erase u₀, HPow.hPow (α := (x : 𝕜) → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (d x))
    (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0 u))

Tactic:
simp_all [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]

Premises used: Finset.prod_congr, finprod_eq_prod_of_mulSupport_subset, rfl
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
pos :
  ∀ (hd : (support d).Finite),
    MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
neg :
  ∀ (hd : ¬(support d).Finite),
    MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
⊢ MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ

Tactic:
by_cases hd : d.support.Finite

Premises used: Set.Finite, Function.support
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) univ z
pos :
  MeromorphicNFAt
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u))
    z
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z

Tactic:
rw [extractFactor z hd]

Premises used: Function.FactorizedRational.extractFactor
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) univ z
pos :
  ∃ (n : ℤ) (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧
        HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) *
            ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u) =ᶠ[nhds z]
          HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) n • g
⊢ MeromorphicNFAt
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u))
    z

Tactic:
right
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) univ z
h :
  AnalyticAt 𝕜 (F := 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z ∧
    Ne.{u_1 + 1} (α := 𝕜)
        ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z) 0 ∧
      HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) *
          ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u) =ᶠ[nhds z]
        HSMul.hSMul (β := 𝕜 → 𝕜) (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z))
          (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u))
⊢ ∃ (n : ℤ) (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧
        HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) *
            ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u) =ᶠ[nhds z]
          HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) n • g

Tactic:
use d z, (∏ᶠ u, (· - u) ^ update d z 0 u)

Premises used: Function.update, HSub.hSub, finprod, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) univ z
⊢ AnalyticAt 𝕜 (F := 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z ∧
    Ne.{u_1 + 1} (α := 𝕜)
        ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z) 0 ∧
      HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) *
          ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u) =ᶠ[nhds z]
        HSMul.hSMul (β := 𝕜 → 𝕜) (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z))
          (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u))

Tactic:
simp [analyticAt, ne_zero]

Premises used: Function.FactorizedRational.ne_zero, Function.FactorizedRational.analyticAt
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : ¬(support d).Finite
⊢ ¬Set.Finite.{u_1} (α := 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u))

Tactic:
rw [← mulSupport d] at hd

Premises used: Function.FactorizedRational.mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd :
  ¬Set.Finite.{u_1} (α := 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u))
neg : MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) 1 univ
⊢ MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ

Tactic:
rw [finprod_of_infinite_mulSupport hd]

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd :
  ¬Set.Finite.{u_1} (α := 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u))
⊢ MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) 1 univ

Tactic:
AnalyticOnNhd.meromorphicNFOn analyticOnNhd_const

Premises used: analyticOnNhd_const, AnalyticOnNhd.meromorphicNFOn