awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
have pos : ∀ (hu : x ∈ U), Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
Tactic: by_cases hu : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
pos : ∀ (hu : x ∈ U), Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
have neg : ∀ (hu : x ∉ U), Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
Tactic: by_cases hu : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) x : ℤ) (0 : ℤ)
have pos : (meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) x).untop₀ = untop₀ (↑0 : WithTop ℤ)
Tactic: rw [divisor_apply (show MeromorphicOn (· - z₀) U from fun_sub id <| const z₀) hu,
      ← untop₀_coe 0]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
⊢ (meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) x).untop₀ = untop₀ (↑0 : WithTop ℤ)
have pos : meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) x = (↑0 : WithTop ℤ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
U : Set 𝕜
h : z₀ ∈ U
⊢ Eq (α := ℤ) ((divisor (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) U : (a : 𝕜) → ℤ) z₀ : ℤ) (1 : ℤ)
have rw : (meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) z₀).untop₀ = untop₀ (↑1 : WithTop ℤ)
Tactic: rw [divisor_apply (show MeromorphicOn (· - z₀) U from fun_sub id <| const z₀) h, ← untop₀_coe 1]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
U : Set 𝕜
h : z₀ ∈ U
⊢ (meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) z₀).untop₀ = untop₀ (↑1 : WithTop ℤ)
have e_a : meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ x - z₀) z₀ = (↑1 : WithTop ℤ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
⊢ (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) = support d
have h : ∀ (u : 𝕜),
  Membership.mem (γ := Set 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u ↔
    u ∈ support d
Tactic: ext u
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
⊢ Membership.mem (γ := Set 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u ↔
    u ∈ support d
have h : Membership.mem (γ := Set 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u →
  u ∈ support d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h :
  Membership.mem (γ := Set 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u →
    u ∈ support d
⊢ Membership.mem (γ := Set 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u ↔
    u ∈ support d
have h₁ : u ∈ support d →
  Membership.mem (γ := Set 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h :
  Membership.mem (γ := Set 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u
⊢ u ∈ support d
have h₁ : ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) = 1
Tactic: simp_all only [mem_mulSupport, ne_eq, mem_support]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
⊢ Membership.mem (γ := Set 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) u
have h₁ : ∃ (a : 𝕜), ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) a = 1 a
Tactic: simp_all only [mem_mulSupport, ne_eq, ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
⊢ ∃ (a : 𝕜), ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) a = 1 a
have h₁ : ¬HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u) u = 1 u
Tactic: use u
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
⊢ Eq.{u_1 + 1} (α := 𝕜 → 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) fun (x : 𝕜) ↦
    ∏ᶠ (u : 𝕜), (x - u) ^ d u
have h₁ : ∀ (x : 𝕜),
  Eq.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have h₁ : 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: rw [finprod_eq_prod_of_mulSupport_subset (s := h.toFinset),
    finprod_eq_prod_of_mulSupport_subset (s := h.toFinset)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
h₁ :
  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)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have h₂ : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
Tactic: rw [finprod_eq_prod_of_mulSupport_subset (s := h.toFinset),
    finprod_eq_prod_of_mulSupport_subset (s := h.toFinset)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x : 𝕜
h₁ :
  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)
h₂ : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have h₃ : (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
  (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
Tactic: rw [finprod_eq_prod_of_mulSupport_subset (s := h.toFinset),
    finprod_eq_prod_of_mulSupport_subset (s := h.toFinset)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
h : HasFiniteSupport d
x u : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) u →
    u ∈ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
have h₁ : u ∉ (↑(Finite.toFinset (s := support d) h) : Set 𝕜) → u ∉ Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
⊢ AnalyticAt 𝕜 (F := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
have h₁ : ∀ (a : 𝕜), AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - a) (d a)) x
Tactic: apply analyticAt_finprod
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
have pos : ∀ (h₂ : x = u), AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
Tactic: by_cases h₂ : x = u
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
have neg : ∀ (h₂ : ¬x = u), AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
Tactic: by_cases h₂ : x = u
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : x = u
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
have pos : 0 ≤ d u
Tactic: apply AnalyticAt.fun_zpow_nonneg (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : ¬x = u
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x
have neg : x - u ≠ 0
Tactic: apply AnalyticAt.fun_zpow (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : 0 ≤ d x
u : 𝕜
h₂ : ¬x = u
⊢ x - u ≠ 0
have neg : x ≠ u
Tactic: rwa [sub_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
⊢ Ne.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) 0
have 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
Tactic: by_cases h₁ : (fun u ↦ (· - u) ^ d u).HasFiniteMulSupport
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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
⊢ Ne.{u_1 + 1} (α := 𝕜) ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x) 0
have 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
Tactic: by_cases h₁ : (fun u ↦ (· - u) ^ d u).HasFiniteMulSupport
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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
have 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
Tactic: rw [finprod_eq_prod _ h₁, Finset.prod_apply, Finset.prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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₁
⊢ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) x ≠ 0
have pos : ¬(x - z) ^ d z = 0
Tactic: simp only [Pi.pow_apply, ne_eq]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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₁
⊢ ¬(x - z) ^ d z = 0
have pos : ∀ (h₂ : x = z), ¬(x - z) ^ d z = 0
Tactic: by_cases h₂ : x = z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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
⊢ ¬(x - z) ^ d z = 0
have neg : ∀ (h₂ : ¬x = z), ¬(x - z) ^ d z = 0
Tactic: by_cases h₂ : x = z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
⊢ ∏ᶠ (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)
have 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)
Tactic: by_cases h₁d : d u₀ = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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)
⊢ ∏ᶠ (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)
have 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)
Tactic: by_cases h₁d : d u₀ = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
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)
have this : (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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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 : 𝕜), 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)
have 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)
Tactic: rw [finprod_eq_prod_of_mulSupport_subset _ this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
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 𝕜)
⊢ ∏ 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)
have this₁ : u₀ ∈ Finite.toFinset (s := support d) hd
Tactic: have : u₀ ∈ hd.toFinset := by simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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
⊢ ∏ 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)
have 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)
Tactic: rw [← Finset.mul_prod_erase hd.toFinset _ this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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
⊢ 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)
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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 𝕜)
have rw : support (update (β := fun (a : 𝕜) ↦ ℤ) d u₀ 0) ⊆ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
Tactic: rw [mulSupport]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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)
⊢ x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
have pos : ∀ (h₁x : x = u₀), x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
Tactic: by_cases h₁x : x = u₀
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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 𝕜)
⊢ x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
have neg : ∀ (h₁x : ¬x = u₀), x ∈ (↑((Finite.toFinset (s := support d) hd).erase u₀) : Set 𝕜)
Tactic: by_cases h₁x : x = u₀
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
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
⊢ 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))
have 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 𝕜)
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
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
⊢ MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
have pos : ∀ (hd : (support d).Finite),
  MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
Tactic: by_cases hd : d.support.Finite