awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd :
  ¬Set.Finite.{u_1} (α := 𝕜)
      (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u))
⊢ MeromorphicNFOn.{u_1, u_1} (𝕜 := 𝕜) (E := 𝕜) 1 univ

Tactic:
exact AnalyticOnNhd.meromorphicNFOn analyticOnNhd_const

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

Tactic:
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

Premises used: Function.FactorizedRational.mulSupport, Set.Finite, Function.FactorizedRational.ne_zero, analyticOnNhd_const, Function.FactorizedRational.analyticAt, AnalyticOnNhd.meromorphicNFOn, Function.support
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
U : Set 𝕜
⊢ MeromorphicNFOn (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) U

Tactic:
fun _ _ ↦ meromorphicNFOn_univ d (trivial)

Premises used: trivial, Function.FactorizedRational.meromorphicNFOn_univ, MeromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
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 ℤ)

Tactic:
rw [meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))]

Premises used: meromorphicOrderAt_eq_int_iff, Function.FactorizedRational.meromorphicNFOn_univ, Set.mem_univ, MeromorphicNFOn.meromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
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)
⊢ ∃ (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:
use ∏ᶠ u, (· - u) ^ update d z 0 u
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
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
⊢ 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:
simp only [update_self, le_refl, analyticAt, ne_eq, ne_zero, not_false_eq_true, smul_eq_mul,
    true_and]

Premises used: le_refl, Function.FactorizedRational.ne_zero, Function.FactorizedRational.analyticAt, ne_eq, smul_eq_mul, Function.update_self, not_false_eq_true, true_and
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
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
⊢ ∀ᶠ (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:
filter_upwards
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
h₁d : HasFiniteSupport d
⊢ ∀ (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:
simp [extractFactor z h₁d]

Premises used: Function.FactorizedRational.extractFactor
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
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
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z = (↑(d z) : WithTop ℤ)

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]

Premises used: le_refl, meromorphicOrderAt_eq_int_iff, Function.FactorizedRational.meromorphicNFOn_univ, Function.FactorizedRational.ne_zero, Function.FactorizedRational.analyticAt, ne_eq, Set.mem_univ, MeromorphicNFOn.meromorphicOn, Function.FactorizedRational.extractFactor, smul_eq_mul, Function.update_self, not_false_eq_true, true_and
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 ≠ ⊤
neg :
  ∀ (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 ≠ ⊤

Tactic:
by_cases hd : d.support.Finite

Premises used: Set.Finite, Function.support
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
⊢ meromorphicOrderAt (E := 𝕜) (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) z ≠ ⊤

Tactic:
simp [meromorphicOrderAt_eq d hd]

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

Tactic:
rw [← mulSupport] at hd

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

Tactic:
simp [finprod_of_infinite_mulSupport hd]

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 ≠ ⊤
neg neg₁ :
  ∀ (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 ≠ ⊤

Tactic:
classical
  by_cases hd : d.support.Finite
  · simp [meromorphicOrderAt_eq d hd]
  · rw [← mulSupport] at hd
    simp [finprod_of_infinite_mulSupport hd]

Premises used: Function.FactorizedRational.mulSupport, Set.Finite, Function.support
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support (U := U).Finite
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ)
      ((MeromorphicOn.divisor (E := 𝕜)
              (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
            (a : 𝕜) → ℤ)
          z :
        ℤ)
      ((D : (a : 𝕜) → ℤ) z : ℤ)
⊢ MeromorphicOn.divisor (E := 𝕜)
      (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U =
    D

Tactic:
ext z
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 : ℤ)
neg :
  ∀ (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 : ℤ)

Tactic:
by_cases hz : z ∈ U
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support (U := U).Finite
z : 𝕜
hz : z ∈ U
⊢ Eq (α := ℤ)
    ((MeromorphicOn.divisor (E := 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
          (a : 𝕜) → ℤ)
        z :
      ℤ)
    ((D : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
simp [(meromorphicNFOn D U).meromorphicOn, hz, meromorphicOrderAt_eq D hD]

Premises used: Function.FactorizedRational.meromorphicOrderAt_eq, MeromorphicNFOn.meromorphicOn, DFunLike.coe, Function.FactorizedRational.meromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support (U := U).Finite
z : 𝕜
hz : z ∉ U
⊢ Eq (α := ℤ)
    ((MeromorphicOn.divisor (E := 𝕜)
            (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x : 𝕜) ↦ x - u) ((D : (a : 𝕜) → ℤ) u : ℤ)) U :
          (a : 𝕜) → ℤ)
        z :
      ℤ)
    ((D : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
simp [(meromorphicNFOn D U).meromorphicOn, hz, meromorphicOrderAt_eq D hD]

Premises used: Function.FactorizedRational.meromorphicOrderAt_eq, MeromorphicNFOn.meromorphicOn, DFunLike.coe, Function.FactorizedRational.meromorphicNFOn
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
contrapose :
  u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) →
    u ∉ Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 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 𝕜)

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

Tactic:
simp only [mem_mulSupport, ne_eq, Decidable.not_not]

Premises used: Function.mem_mulSupport, ne_eq, Decidable.not_not
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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
neg :
  ∀ (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

Tactic:
by_cases h₁ : u = x
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
pos : x ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - x) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x = 1
⊢ u ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u = 1

Tactic:
rw [h₁]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
⊢ x ∉ (↑(h.toFinset (s := support d)) : Set 𝕜) → (x - x) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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

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

Tactic:
simp [Function.FactorizedRational.mulSupport]

Premises used: Function.FactorizedRational.mulSupport
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ (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]
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
x_1 : 𝕜
⊢ x_1 ∈ Finite.toFinset (s := support d) h → MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - x_1) (d x_1)) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
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)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _ this, meromorphicTrailingCoeffAt_prod
      (fun _ ↦ by fun_prop), finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]

Premises used: _private.0.Function.FactorizedRational.mulSupport_update, meromorphicTrailingCoeffAt_prod, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
apply :
  ∀ x_1 ∈ Finite.toFinset (s := support d) h,
    meromorphicTrailingCoeffAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - x_1) (d x_1)) x =
      (x - x_1) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x_1
⊢ 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:
apply Finset.prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
⊢ MeromorphicAt (E := 𝕜) (fun (x : 𝕜) ↦ x - y) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
rw :
  HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
⊢ meromorphicTrailingCoeffAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - y) (d y)) x =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y

Tactic:
rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop)]

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_zpow
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
pos :
  ∀ (hxy : x = y),
    HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
      (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
neg :
  ∀ (hxy : ¬x = y),
    HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
      (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
⊢ HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y

Tactic:
by_cases hxy : x = y
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
hxy : x = y
pos : (if y = y then 1 else y - y) ^ d y = (y - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d y 0 y
⊢ HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y

Tactic:
rw [hxy, meromorphicTrailingCoeffAt_id_sub_const]

Premises used: meromorphicTrailingCoeffAt_id_sub_const
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
hxy : x = y
⊢ (if y = y then 1 else y - y) ^ d y = (y - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d y 0 y

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
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 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
hxy : ¬x = y
⊢ HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y

Tactic:
grind [meromorphicTrailingCoeffAt_id_sub_const]

Premises used: meromorphicTrailingCoeffAt_id_sub_const
-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
rw :
  Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d 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