awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
u : 𝕜
contrapose :
  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 : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
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 : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
⊢ (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)

Tactic:
have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
rw :
  ∀ x_1 ∈ Finite.toFinset (s := support d) h₁, (x - x_1) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x_1 = (x - x_1) ^ d x_1
⊢ Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)

Tactic:
rw [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 : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h₁
e_a : update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = d y
⊢ (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = (x - y) ^ d y

Tactic:
congr
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h₁
e_a : y ≠ x
⊢ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = d y

Tactic:
apply Function.update_of_ne

Premises used: Function.update_of_ne
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h₁
e_a : ∀ (hCon : y = x), False
⊢ y ≠ x

Tactic:
by_contra hCon
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h₁
hCon : y = x
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
rw : Eq.{u_1 + 1} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₁ rw₂ rw₃ :
  Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₄ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)),
    Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
      (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₅ rw₆ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
    (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁),
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = (x - y) ^ d y
e_a :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
    (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁), update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = d y
e_a₁ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
    (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁), y ≠ x
e_a₂ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
    (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁) (hCon : y = x), False
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)

Tactic:
classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
  have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
  intro y hy
  congr
  apply Function.update_of_ne
  by_contra hCon
  simp_all

Premises used: _private.0.Function.FactorizedRational.mulSupport_update, Finset.prod_congr, Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational, finprod_eq_prod_of_mulSupport_subset, rfl, Function.update_of_ne
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
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‖

Tactic:
rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]

Premises used: _private.0.Function.FactorizedRational.mulSupport_update, Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
y : 𝕜
_ : y ∈ Finite.toFinset (s := support d) h → ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
⊢ y ∈ Finite.toFinset (s := support d) h → ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0

Tactic:
_
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
y : 𝕜
h_1 : y ∈ Finite.toFinset (s := support d) h
pos : ∀ (h : x = y), ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
neg : ∀ (h : ¬x = y), ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
⊢ ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0

Tactic:
by_cases h : x = y
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h_1 : HasFiniteSupport d
y : 𝕜
h_2 : y ∈ Finite.toFinset (s := support d) h_1
h : x = y
pos : ‖(y - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d y 0 y‖ ≠ 0
⊢ ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h_1 : HasFiniteSupport d
y : 𝕜
h_2 : y ∈ Finite.toFinset (s := support d) h_1
h : x = y
⊢ ‖(y - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d y 0 y‖ ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h_1 : HasFiniteSupport d
y : 𝕜
h_2 : y ∈ Finite.toFinset (s := support d) h_1
h : ¬x = y
⊢ ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 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 : HasFiniteSupport d
⊢ ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0

Tactic:
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]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
rw :
  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 := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖

Tactic:
rw [norm_prod, log_prod this]

Premises used: Real.log_prod, norm_prod
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
u : 𝕜
contrapose :
  u ∉ (↑(Finite.toFinset (s := support d) h) : Set 𝕜) → u ∉ support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖
⊢ Membership.mem (γ := Set 𝕜) (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) u →
    u ∈ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)

Tactic:
contrapose
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
u : 𝕜
⊢ u ∉ (↑(Finite.toFinset (s := support d) h) : Set 𝕜) → u ∉ support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
⊢ (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)

Tactic:
have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ 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 𝕜)
rw :
  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‖)
⊢ 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:
rw [finsum_eq_sum_of_support_subset _ this]

Premises used: finsum_eq_sum_of_support_subset
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ 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 𝕜)
apply :
  ∀ 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‖
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ 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 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
rw : (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
⊢ log ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ = (↑(d y) : ℝ) * log ‖x - y‖

Tactic:
rw [norm_zpow, Real.log_zpow]

Premises used: Real.log_zpow, norm_zpow
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ 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 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
pos : ∀ (h : x = y), (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
neg : ∀ (h : ¬x = y), (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
⊢ (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖

Tactic:
by_cases h : x = y
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h_1 : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h_1, ‖(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_1) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h_1
h : x = y
⊢ (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h_1 : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h_1, ‖(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_1) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h_1
h : ¬x = y
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : y = x → False
⊢ y ≠ x

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h_1 : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h_1, ‖(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_1) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h_1
h : ¬x = y
neg neg₁ : (↑(d y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
⊢ (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖

Tactic:
rw [Function.update_of_ne (by tauto)]

Premises used: Function.update_of_ne
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 : ℤ)
⊢ MeromorphicOn φ U

Tactic:
have hφ : MeromorphicOn φ U := (meromorphicNFOn (divisor f U) U).meromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ MeromorphicNFOn g U

Tactic:
apply meromorphicNFOn_toMeromorphicNFOn

Premises used: meromorphicNFOn_toMeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
⊢ MeromorphicNFOn g U

Tactic:
have hg : MeromorphicNFOn g U := by apply meromorphicNFOn_toMeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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

Tactic:
⟨g, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
refine_3 :
  f =ᶠ[codiscreteWithin U]
    HSMul.hSMul (α := 𝕜 → 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((divisor f U : (a : 𝕜) → ℤ) u : ℤ)) g
⊢ ∃ (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

Tactic:
refine ⟨g, ?_, ?_, ?_⟩
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
rw : ∀ z ∈ U, meromorphicOrderAt φ⁻¹ z ≠ ⊤
⊢ AnalyticOnNhd 𝕜 g U

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]

Premises used: Function.FactorizedRational.divisor, MeromorphicOn.divisor_inv, MeromorphicOn.inv, Subtype.mk, MeromorphicOn.divisor_of_toMeromorphicNFOn, MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd, neg_add_cancel, MeromorphicOn.smul, MeromorphicOn.divisor_smul
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
z : 𝕜
hz : z ∈ U
⊢ meromorphicOrderAt φ⁻¹ z ≠ ⊤

Tactic:
simpa [meromorphicOrderAt_inv] using meromorphicOrderAt_ne_top (divisor f U)

Premises used: MeromorphicOn.divisor, meromorphicOrderAt_inv, Function.FactorizedRational.meromorphicOrderAt_ne_top, DFunLike.coe
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
refine_2 :
  HAdd.hAdd (α := WithTop ℤ) (-(↑((divisor f U : (a : 𝕜) → ℤ) u) : WithTop ℤ) : WithTop ℤ) (meromorphicOrderAt f u) = 0
⊢ g (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) u hu) : 𝕜) ≠ 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]

Premises used: MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE, Function.FactorizedRational.meromorphicOrderAt_eq, meromorphicOrderAt_inv, meromorphicOrderAt_smul, MeromorphicOn.inv, MeromorphicOn.smul, MeromorphicAt.inv, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff, Filter.EventuallyEq.symm, meromorphicOrderAt_congr
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
refine_2 : -(↑(meromorphicOrderAt f u).untop₀ : WithTop ℤ) + meromorphicOrderAt f u = 0
⊢ HAdd.hAdd (α := WithTop ℤ) (-(↑((divisor f U : (a : 𝕜) → ℤ) u) : WithTop ℤ) : WithTop ℤ) (meromorphicOrderAt f u) = 0

Tactic:
simp only [h₁f, hu, divisor_apply]

Premises used: MeromorphicOn.divisor_apply