awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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
⊢ MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
have neg : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) univ z
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z
have 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
Tactic: rw [extractFactor z hd]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) univ z
⊢ MeromorphicNFAt
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z) (d z) *
      ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u))
    z
have 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
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) univ z
⊢ ∃ (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
have 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))
Tactic: use d z, (∏ᶠ u, (· - u) ^ update d z 0 u)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : ¬(support d).Finite
⊢ MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
have hd₁ : ¬Set.Finite.{u_1} (α := 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u))
Tactic: rw [← mulSupport d] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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 := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
have neg : MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) 1 univ
Tactic: rw [finprod_of_infinite_mulSupport hd]
-- 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: classical
  by_cases hd : d.support.Finite
  · intro z hz
    rw [extractFactor z hd]
    right
    use d z, (∏ᶠ u, (· - u) ^ update d z 0 u)
    simp [analyticAt, ne_zero]
  · rw [← mulSupport d] at hd
    rw [finprod_of_infinite_mulSupport hd]
    exact AnalyticOnNhd.meromorphicNFOn analyticOnNhd_const
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
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
⊢ MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
have neg : ∀ (hd : ¬(support d).Finite),
  MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) univ
Tactic: classical
  by_cases hd : d.support.Finite
  · intro z hz
    rw [extractFactor z hd]
    right
    use d z, (∏ᶠ u, (· - u) ^ update d z 0 u)
    simp [analyticAt, ne_zero]
  · rw [← mulSupport d] at hd
    rw [finprod_of_infinite_mulSupport hd]
    exact AnalyticOnNhd.meromorphicNFOn analyticOnNhd_const
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z = (↑(d z) : WithTop ℤ)
have rw : ∃ (g : 𝕜 → 𝕜),
  AnalyticAt 𝕜 g z ∧
    g z ≠ 0 ∧
      ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 = (z_1 - z) ^ d z • g z_1
Tactic: rw [meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧
        ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
          (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 = (z_1 - z) ^ d z • g z_1
have 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 ∧
    ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
        HSMul.hSMul (β := 𝕜) ((z_1 - z) ^ d z)
          ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1)
Tactic: use ∏ᶠ u, (· - u) ^ update d z 0 u
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ 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 ∧
      ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
          HSMul.hSMul (β := 𝕜) ((z_1 - z) ^ d z)
            ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1)
have h : ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
  (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
    (z_1 - z) ^ d z *
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1
Tactic: simp only [update_self, le_refl, analyticAt, ne_eq, ne_zero, not_false_eq_true, smul_eq_mul,
    true_and]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
    (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
      (z_1 - z) ^ d z *
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1
have h : ∀ (a : 𝕜),
  (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) a =
    (a - z) ^ d z * (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z = (↑(d z) : WithTop ℤ)
have rw : ∃ (g : 𝕜 → 𝕜),
  AnalyticAt 𝕜 g z ∧
    g z ≠ 0 ∧
      ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 = (z_1 - z) ^ d z • g z_1
Tactic: classical
  rw [meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))]
  use ∏ᶠ u, (· - u) ^ update d z 0 u
  simp only [update_self, le_refl, analyticAt, ne_eq, ne_zero, not_false_eq_true, smul_eq_mul,
    true_and]
  filter_upwards
  simp [extractFactor z h₁d]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
rw rw₁ rw₂ :
  ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧
        ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
          (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 = (z_1 - z) ^ d z • g z_1
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z = (↑(d z) : WithTop ℤ)
have 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 ∧
    ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
        HSMul.hSMul (β := 𝕜) ((z_1 - z) ^ d z)
          ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1)
Tactic: classical
  rw [meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))]
  use ∏ᶠ u, (· - u) ^ update d z 0 u
  simp only [update_self, le_refl, analyticAt, ne_eq, ne_zero, not_false_eq_true, smul_eq_mul,
    true_and]
  filter_upwards
  simp [extractFactor z h₁d]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
rw rw₁ rw₂ :
  ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧
        ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
          (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 = (z_1 - z) ^ d z • g z_1
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 ∧
      ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
          HSMul.hSMul (β := 𝕜) ((z_1 - z) ^ d z)
            ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1)
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z = (↑(d z) : WithTop ℤ)
have h₁ : ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
  (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
    (z_1 - z) ^ d z *
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1
Tactic: classical
  rw [meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))]
  use ∏ᶠ u, (· - u) ^ update d z 0 u
  simp only [update_self, le_refl, analyticAt, ne_eq, ne_zero, not_false_eq_true, smul_eq_mul,
    true_and]
  filter_upwards
  simp [extractFactor z h₁d]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
rw rw₁ rw₂ :
  ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g z ∧
      g z ≠ 0 ∧
        ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
          (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 = (z_1 - z) ^ d z • g z_1
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 ∧
      ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
          HSMul.hSMul (β := 𝕜) ((z_1 - z) ^ d z)
            ((∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1)
h₁ :
  ∀ᶠ (z_1 : 𝕜) in nhdsWithin z {z}ᶜ,
    (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z_1 =
      (z_1 - z) ^ d z *
        (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) z_1
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z = (↑(d z) : WithTop ℤ)
have h₂ : ∀ (a : 𝕜),
  (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) a =
    (a - z) ^ d z * (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (update (β := fun (a : 𝕜) ↦ ℤ) d z 0 u)) a
Tactic: classical
  rw [meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))]
  use ∏ᶠ u, (· - u) ^ update d z 0 u
  simp only [update_self, le_refl, analyticAt, ne_eq, ne_zero, not_false_eq_true, smul_eq_mul,
    true_and]
  filter_upwards
  simp [extractFactor z h₁d]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
have pos : ∀ (hd : (support d).Finite),
  meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
Tactic: by_cases hd : d.support.Finite
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
pos :
  ∀ (hd : (support d).Finite),
    meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
have neg : ∀ (hd : ¬(support d).Finite),
  meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
Tactic: by_cases hd : d.support.Finite
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
hd : ¬(support d).Finite
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
have hd₁ : ¬Set.Finite.{u_1} (α := 𝕜)
    (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u))
Tactic: rw [← mulSupport] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
have pos : ∀ (hd : (support d).Finite),
  meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
Tactic: classical
  by_cases hd : d.support.Finite
  · simp [meromorphicOrderAt_eq d hd]
  · rw [← mulSupport] at hd
    simp [finprod_of_infinite_mulSupport hd]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
pos :
  ∀ (hd : (support d).Finite),
    meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
have neg : ∀ (hd : ¬(support d).Finite),
  meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤
Tactic: classical
  by_cases hd : d.support.Finite
  · simp [meromorphicOrderAt_eq d hd]
  · rw [← mulSupport] at hd
    simp [finprod_of_infinite_mulSupport hd]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support (U := U).Finite
⊢ MeromorphicOn.divisor (E := 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U =
    D
have h : ∀ (z : 𝕜),
  Eq (α := ℤ)
    ((MeromorphicOn.divisor (E := 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
          (a : 𝕜) → ℤ)
        z :
      ℤ)
    ((D : (a : 𝕜) → ℤ) z : ℤ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support (U := U).Finite
z : 𝕜
⊢ Eq (α := ℤ)
    ((MeromorphicOn.divisor (E := 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
          (a : 𝕜) → ℤ)
        z :
      ℤ)
    ((D : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hz : z ∈ U),
  Eq (α := ℤ)
    ((MeromorphicOn.divisor (E := 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
          (a : 𝕜) → ℤ)
        z :
      ℤ)
    ((D : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support (U := U).Finite
z : 𝕜
pos :
  ∀ (hz : z ∈ U),
    Eq (α := ℤ)
      ((MeromorphicOn.divisor (E := 𝕜)
              (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
            (a : 𝕜) → ℤ)
          z :
        ℤ)
      ((D : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ)
    ((MeromorphicOn.divisor (E := 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
          (a : 𝕜) → ℤ)
        z :
      ℤ)
    ((D : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hz : z ∉ U),
  Eq (α := ℤ)
    ((MeromorphicOn.divisor (E := 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
          (a : 𝕜) → ℤ)
        z :
      ℤ)
    ((D : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
⊢ Membership.mem (γ := Set 𝕜)
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u) u →
    u ∈ (↑(h.toFinset (s := support d)) : Set 𝕜)
have contrapose : u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) →
  u ∉ Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
⊢ u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) →
    u ∉ Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u
have simp : u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u = 1
Tactic: simp only [mem_mulSupport, ne_eq, Decidable.not_not]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
⊢ u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u = 1
have pos : ∀ (h₁ : u = x), u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u = 1
Tactic: by_cases h₁ : u = x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
pos : ∀ (h₁ : u = x), u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u = 1
⊢ u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u = 1
have neg : ∀ (h₁ : ¬u = x), u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u = 1
Tactic: by_cases h₁ : u = x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
⊢ u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u = 1
have pos : x ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - x) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x = 1
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)
have this : (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
  (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
Tactic: have : (fun u ↦ (· - u) ^ d u).mulSupport ⊆ h.toFinset := by
    simp [Function.FactorizedRational.mulSupport]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this :
  (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)
have rw : Eq (α := 𝕜)
  (∏ n ∈ Finite.toFinset (s := support d) h,
    meromorphicTrailingCoeffAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - n) (d n)) x)
  (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
Tactic: rw [finprod_eq_prod_of_mulSupport_subset _ this, meromorphicTrailingCoeffAt_prod
      (fun _ ↦ by fun_prop), finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]