mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ 0 ≤ meromorphicOrderAt f x → AnalyticAt 𝕜 f x

pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ AnalyticAt 𝕜 f x → 0 ≤ meromorphicOrderAt f x

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ 0 ≤ meromorphicOrderAt f x → AnalyticAt 𝕜 f x

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
⊢ AnalyticAt 𝕜 f x → 0 ≤ meromorphicOrderAt f x
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : x ∉ U + {c}
⊢ x ∉ U + {c}

pp: case pos.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : x ∉ U + {c}
⊢ x - c ∉ U

Tactic:
<;>

Goal state after:
case pos.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : x ∉ U + {c}
⊢ x ∉ U + {c}

case pos.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : x ∉ U + {c}
⊢ x - c ∉ U
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ (meromorphicOrderAt (f ∘ fun x ↦ x + c) (x - c)).untop₀ = (meromorphicOrderAt f x).untop₀

pp: case neg.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ MeromorphicOn f (U + {c})

pp: case neg.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ x ∈ U + {c}

pp: case neg.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ MeromorphicOn (f ∘ fun x ↦ x + c) U

pp: case neg.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ x - c ∈ U

Tactic:
<;>

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ (meromorphicOrderAt (f ∘ fun x ↦ x + c) (x - c)).untop₀ = (meromorphicOrderAt f x).untop₀

case neg.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ MeromorphicOn f (U + {c})

case neg.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ x ∈ U + {c}

case neg.hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ MeromorphicOn (f ∘ fun x ↦ x + c) U

case neg.hz
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c x : 𝕜
f : 𝕜 → E
h : MeromorphicOn f (U + {c})
this : MeromorphicOn (f ∘ fun x ↦ x + c) U
h₁ : ¬x ∉ U + {c}
⊢ x - c ∈ U
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
⊢ MeromorphicNFAt (g • f) x

Tactic:
right
    use n, g • g_f, h₁g.smul h₁g_f
    constructor
    · simp [smul_ne_zero h₂g h₂g_f]
    · filter_upwards [h₃g_f]
      intro y hy
      simp only [Pi.smul_apply', hy, Pi.pow_apply]
      rw [smul_comm]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
⊢ 0 ≤ MeromorphicOn.divisor f U → AnalyticOnNhd 𝕜 f U

pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
⊢ AnalyticOnNhd 𝕜 f U → 0 ≤ MeromorphicOn.divisor f U

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
⊢ 0 ≤ MeromorphicOn.divisor f U → AnalyticOnNhd 𝕜 f U

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
⊢ AnalyticOnNhd 𝕜 f U → 0 ≤ MeromorphicOn.divisor f U
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
⊢ u ∈ U ∩ f ⁻¹' {0} → u ∈ Function.support ⇑(MeromorphicOn.divisor f U)

pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
⊢ u ∈ Function.support ⇑(MeromorphicOn.divisor f U) → u ∈ U ∩ f ⁻¹' {0}

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
⊢ u ∈ U ∩ f ⁻¹' {0} → u ∈ Function.support ⇑(MeromorphicOn.divisor f U)

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
⊢ u ∈ Function.support ⇑(MeromorphicOn.divisor f U) → u ∈ U ∩ f ⁻¹' {0}
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g • f) U → MeromorphicNFOn f U

pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn f U → MeromorphicNFOn (g • f) U

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g • f) U → MeromorphicNFOn f U

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn f U → MeromorphicNFOn (g • f) U
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
⊢ toMeromorphicNFOn f U = f → MeromorphicNFOn f U

pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
⊢ MeromorphicNFOn f U → toMeromorphicNFOn f U = f

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
⊢ toMeromorphicNFOn f U = f → MeromorphicNFOn f U

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
⊢ MeromorphicNFOn f U → toMeromorphicNFOn f U = f
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
⊢ (divisor (toMeromorphicNFOn f U) U) z = (divisor f U) z

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∉ U
⊢ (divisor (toMeromorphicNFOn f U) U) z = (divisor f U) z

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
⊢ (divisor (toMeromorphicNFOn f U) U) z = (divisor f U) z

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∉ U
⊢ (divisor (toMeromorphicNFOn f U) U) z = (divisor f U) z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : 0 < meromorphicOrderAt f x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
have hf : MeromorphicAt f x := meromorphicAt_of_meromorphicOrderAt_ne_zero ho.ne'
  cases h'o : meromorphicOrderAt f x with
  | top =>
    apply tendsto_const_nhds.congr'
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h'o] with y hy using hy.symm
  | coe n =>
    rcases (meromorphicOrderAt_eq_int_iff hf).1 h'o with ⟨g, g_an, gx, hg⟩
    lift n to ℕ using by simpa [h'o] using ho.le
    have : (0 : E) = (x - x) ^ n • g x := by
      have : 0 < n := by simpa [h'o] using ho
      simp [zero_pow_eq_zero.2 this.ne']
    rw [this]
    have : ContinuousAt (fun z ↦ (z - x) ^ n • g z) x := by fun_prop
    apply this.continuousWithinAt.tendsto.congr'
    filter_upwards [hg] with y hy using by simp [hy]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
⊢ (u ∈ Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) → u ∈ support d

pp: case mpr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
⊢ u ∈ support d → u ∈ Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
⊢ (u ∈ Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) → u ∈ support d

case mpr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
⊢ u ∈ support d → u ∈ Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
hz : z ∈ Finite.toFinset h₁
h₂ : x = z
⊢ ¬(x - z) ^ d z = 0

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
hz : z ∈ Finite.toFinset h₁
h₂ : ¬x = z
⊢ ¬(x - z) ^ d z = 0

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
hz : z ∈ Finite.toFinset h₁
h₂ : x = z
⊢ ¬(x - z) ^ d z = 0

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : d x = 0
h₁ : HasFiniteMulSupport fun u ↦ (fun x ↦ x - u) ^ d u
z : 𝕜
hz : z ∈ Finite.toFinset h₁
h₂ : ¬x = z
⊢ ¬(x - z) ^ d z = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case e'_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ f ^ n = f ^ ↑n

pp: case e'_3
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f x ^ n = meromorphicTrailingCoeffAt f x ^ ↑n

Tactic:
<;>

Goal state after:
case e'_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ f ^ n = f ^ ↑n

case e'_3
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f x ^ n = meromorphicTrailingCoeffAt f x ^ ↑n
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this : u₀ ∈ Finite.toFinset hd
x : 𝕜
hx : x ∈ support (update d u₀ 0)
h₁x : x = u₀
⊢ x ∈ ↑((Finite.toFinset hd).erase u₀)

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this : u₀ ∈ Finite.toFinset hd
x : 𝕜
hx : x ∈ support (update d u₀ 0)
h₁x : ¬x = u₀
⊢ x ∈ ↑((Finite.toFinset hd).erase u₀)

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this : u₀ ∈ Finite.toFinset hd
x : 𝕜
hx : x ∈ support (update d u₀ 0)
h₁x : x = u₀
⊢ x ∈ ↑((Finite.toFinset hd).erase u₀)

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this : u₀ ∈ Finite.toFinset hd
x : 𝕜
hx : x ∈ support (update d u₀ 0)
h₁x : ¬x = u₀
⊢ x ∈ ↑((Finite.toFinset hd).erase u₀)
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support.Finite
z : 𝕜
hz : z ∈ U
⊢ (MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) U) z = D z

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support.Finite
z : 𝕜
hz : z ∉ U
⊢ (MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) U) z = D z

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support.Finite
z : 𝕜
hz : z ∈ U
⊢ (MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) U) z = D z

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
D : locallyFinsuppWithin U ℤ
hD : D.support.Finite
z : 𝕜
hz : z ∉ U
⊢ (MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) U) z = D z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ meromorphicOrderAt (canonicalFactor R w) z = 0

Tactic:
(meromorphicNFOn_canonicalFactor hw (Set.mem_univ z)).meromorphicOrderAt_eq_zero_iff

Goal state after:
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ canonicalFactor R w z ≠ 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case left
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
z : ℂ
hz : z ∈ ball 0 R
a : ℂ
ha : a ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
b : ℂ
hb : b ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
⊢ a ∈ ball 0 R

pp: case right
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
z : ℂ
hz : z ∈ ball 0 R
a : ℂ
ha : a ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
b : ℂ
hb : b ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
⊢ b ∈ ball 0 R

Tactic:
<;>

Goal state after:
case left
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
z : ℂ
hz : z ∈ ball 0 R
a : ℂ
ha : a ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
b : ℂ
hb : b ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
⊢ a ∈ ball 0 R

case right
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
z : ℂ
hz : z ∈ ball 0 R
a : ℂ
ha : a ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
b : ℂ
hb : b ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
⊢ b ∈ ball 0 R
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
⊢ (fun x ↦ ↑(D u) * log ‖x - u‖) = 0 → D u = 0

pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
⊢ D u = 0 → (fun x ↦ ↑(D u) * log ‖x - u‖) = 0

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
⊢ (fun x ↦ ↑(D u) * log ‖x - u‖) = 0 → D u = 0

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
⊢ D u = 0 → (fun x ↦ ↑(D u) * log ‖x - u‖) = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ meromorphicTrailingCoeffAt f x = (∏ᶠ (u : 𝕜), (x - u) ^ update D x 0 u) • g x

Tactic:
have t₀ : MeromorphicAt (∏ᶠ u, (· - u) ^ D u) x :=
    (FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₀ : MeromorphicAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) x
⊢ meromorphicTrailingCoeffAt f x = (∏ᶠ (u : 𝕜), (x - u) ^ update D x 0 u) • g x
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ log ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) x‖ + log ‖g x‖ =
    ∑ᶠ (u : 𝕜), ↑(D u) * log ‖x - u‖ + log ‖g x‖

pp: case hx
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) x‖ ≠ 0

pp: case hy
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ ‖g x‖ ≠ 0

Tactic:
log_norm_meromorphicTrailingCoeffAt hD

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ ∑ᶠ (u : 𝕜), ↑(D u) * log ‖x - u‖ + log ‖g x‖ = ∑ᶠ (u : 𝕜), ↑(D u) * log ‖x - u‖ + log ‖g x‖

case hx
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) x‖ ≠ 0

case hy
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
x : 𝕜
f g : 𝕜 → E
D : 𝕜 → ℤ
hD : HasFiniteSupport D
h₁x : x ∈ U
h₂x : AccPt x (𝓟 U)
hf : MeromorphicAt f x
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
⊢ ‖g x‖ ≠ 0