awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw : log (Norm.norm.{u_1} (E := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)) =
  ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
rw :
  log (Norm.norm.{u_1} (E := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw₁ : log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
  ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
rw :
  log (Norm.norm.{u_1} (E := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₁ rw₂ rw₃ :
  log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw₄ : ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
  log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
rw :
  log (Norm.norm.{u_1} (E := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₁ rw₂ rw₃ :
  log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₄ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
    log
        (Norm.norm (E := 𝕜)
          (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
      ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw₅ : ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
  Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
    (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
rw :
  log (Norm.norm.{u_1} (E := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₁ rw₂ rw₃ :
  log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₄ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
    log
        (Norm.norm (E := 𝕜)
          (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
      ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₅ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
    Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
      (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw₆ : ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0)
  (this :
    (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)),
  Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
    (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
rw :
  log (Norm.norm.{u_1} (E := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₁ rw₂ rw₃ :
  log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₄ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
    log
        (Norm.norm (E := 𝕜)
          (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
      ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₅ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
    Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
      (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
rw₆ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0)
    (this :
      (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)),
    Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
      (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw₇ : ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0)
  (this :
    (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)),
  Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
    (∑ i ∈ Finite.toFinset (s := support d) h, (↑(d i) : ℝ) * log ‖x - i‖)
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
rw :
  log (Norm.norm.{u_1} (E := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₁ rw₂ rw₃ :
  log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₄ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
    log
        (Norm.norm (E := 𝕜)
          (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
      ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₅ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0),
    Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
      (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
rw₆ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0)
    (this :
      (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)),
    Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
      (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
rw₇ :
  ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0)
    (this :
      (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)),
    Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
      (∑ i ∈ Finite.toFinset (s := support d) h, (↑(d i) : ℝ) * log ‖x - i‖)
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw₈ : ∀ (this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0)
  (this :
    (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)),
  ∀ x_1 ∈ Finite.toFinset (s := support d) h,
    log ‖(x - x_1) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x_1‖ = (↑(d x_1) : ℝ) * log ‖x - x_1‖
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
⊢ ∃ (g : 𝕜 → E),
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0) ∧
        f =ᶠ[codiscreteWithin U]
          HSMul.hSMul (α := 𝕜 → 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g
have hφ : MeromorphicOn φ U
Tactic: have hφ : MeromorphicOn φ U := (meromorphicNFOn (divisor f U) U).meromorphicOn
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
⊢ ∃ (g : 𝕜 → E),
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0) ∧
        f =ᶠ[codiscreteWithin U]
          HSMul.hSMul (α := 𝕜 → 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g
have hg : MeromorphicNFOn g U
Tactic: have hg : MeromorphicNFOn g U := by apply meromorphicNFOn_toMeromorphicNFOn
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∃ (g : 𝕜 → E),
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0) ∧
        f =ᶠ[codiscreteWithin U]
          HSMul.hSMul (α := 𝕜 → 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g
have refine_1 : AnalyticOnNhd 𝕜 g U
Tactic: refine ⟨g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
refine_1 : AnalyticOnNhd 𝕜 g U
⊢ ∃ (g : 𝕜 → E),
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0) ∧
        f =ᶠ[codiscreteWithin U]
          HSMul.hSMul (α := 𝕜 → 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g
have refine_2 : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
Tactic: refine ⟨g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
refine_1 : AnalyticOnNhd 𝕜 g U
refine_2 : ∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0
⊢ ∃ (g : 𝕜 → E),
    AnalyticOnNhd 𝕜 g U ∧
      (∀ (u : (↑U : Type u_1)), g (↑u : 𝕜) ≠ 0) ∧
        f =ᶠ[codiscreteWithin U]
          HSMul.hSMul (α := 𝕜 → 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g
have refine_3 : f =ᶠ[codiscreteWithin U]
  HSMul.hSMul (α := 𝕜 → 𝕜)
    (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g
Tactic: refine ⟨g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ AnalyticOnNhd 𝕜 g U
have rw : ∀ z ∈ U, meromorphicOrderAt φ⁻¹ z ≠ ⊤
Tactic: rw [← hg.divisor_nonneg_iff_analyticOnNhd, divisor_of_toMeromorphicNFOn (hφ.inv.smul h₁f),
      divisor_smul hφ.inv h₁f _ (fun z hz ↦ h₂f ⟨z, hz⟩), divisor_inv,
      Function.FactorizedRational.divisor h₃f, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
⊢ g (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) u hu) : 𝕜) ≠ 0
have refine_2 : HAdd.hAdd (α := WithTop ℤ) (-(↑((divisor f U : (a : 𝕜) → ℤ) u) : WithTop ℤ) : WithTop ℤ) (meromorphicOrderAt f u) = 0
Tactic: rw [← (hg hu).meromorphicOrderAt_eq_zero_iff, ← meromorphicOrderAt_congr
        (toMeromorphicNFOn_eq_self_on_nhdsNE (hφ.inv.smul h₁f) hu).symm,
      meromorphicOrderAt_smul (hφ u hu).inv (h₁f u hu), meromorphicOrderAt_inv,
      meromorphicOrderAt_eq _ h₃f]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
⊢ HAdd.hAdd (α := WithTop ℤ) (-(↑((divisor f U : (a : 𝕜) → ℤ) u) : WithTop ℤ) : WithTop ℤ) (meromorphicOrderAt f u) = 0
have refine_2 : -(↑(meromorphicOrderAt f u).untop₀ : WithTop ℤ) + meromorphicOrderAt f u = 0
Tactic: simp only [h₁f, hu, divisor_apply]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
⊢ -(↑(meromorphicOrderAt f u).untop₀ : WithTop ℤ) + meromorphicOrderAt f u = 0
have refine_2 : ∀ (n : ℤ) (hn : (↑n : WithTop ℤ) = meromorphicOrderAt f u),
  -(↑(↑n : WithTop ℤ).untop₀ : WithTop ℤ) + (↑n : WithTop ℤ) = 0
Tactic: lift meromorphicOrderAt f u to ℤ using (h₂f ⟨u, hu⟩) with n hn
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
h₃f : (locallyFinsuppWithin.support (U := U) (divisor f U)).Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
u : 𝕜
hu : u ∈ U
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f u
⊢ -(↑(↑n : WithTop ℤ).untop₀ : WithTop ℤ) + (↑n : WithTop ℤ) = 0
have refine_2 : (↑(-n + n) : WithTop ℤ) = 0
Tactic: rw [WithTop.untop₀_coe, ← WithTop.LinearOrderedAddCommGroup.coe_neg, ← WithTop.coe_add]