mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
w : ℂ
hw : w ∉ ball 0 R
⊢ MeromorphicNFOn (canonicalFactor R w ^ F w) (ball 0 R)

Tactic:
·

Goal state after:
case neg
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
w : ℂ
hw : w ∉ ball 0 R
⊢ MeromorphicNFOn (canonicalFactor R w ^ F w) (ball 0 R)
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ AnalyticOnNhd 𝕜 g U

pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∀ (u : ↑U), g ↑u ≠ 0

pp: case refine_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ AnalyticOnNhd 𝕜 g U
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = (z - x) ^ 0 • g z

pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ MeromorphicAt 1 x

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = (z - x) ^ 0 • g z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case refine_2
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 = b

Tactic:
·

Goal state after:
case refine_2
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 = b
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ MeromorphicAt 1 x

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
⊢ MeromorphicAt 1 x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
⊢ ↑n * ⊤ + ⊤ = (↑n + 1) * ⊤

pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
a✝ : ℤ
⊢ ↑n * ↑a✝ + ↑a✝ = (↑n + 1) * ↑a✝

Tactic:
·

Goal state after:
case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
⊢ ↑n * ⊤ + ⊤ = (↑n + 1) * ⊤
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
a✝ : ℤ
⊢ ↑n * ↑a✝ + ↑a✝ = (↑n + 1) * ↑a✝

Tactic:
·

Goal state after:
case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
a✝ : ℤ
⊢ ↑n * ↑a✝ + ↑a✝ = (↑n + 1) * ↑a✝
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
⊢ meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = (z - x) ^ 0 • g z

pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ MeromorphicAt 1 x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = (z - x) ^ 0 • g z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∀ (u : ↑U), g ↑u ≠ 0

pp: case refine_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∀ (u : ↑U), g ↑u ≠ 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ MeromorphicAt 1 x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : n = 0
⊢ MeromorphicAt 1 x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz : z ∉ U
⊢ (∑ x ∈ h.toFinset, F x • locallyFinsuppWithin.restrict (single x 1) ⋯) z = F z

pp: case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz : ¬z ∉ U
⊢ (∑ x ∈ h.toFinset, F x • locallyFinsuppWithin.restrict (single x 1) ⋯) z = F z

Tactic:
·

Goal state after:
case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz : z ∉ U
⊢ (∑ x ∈ h.toFinset, F x • locallyFinsuppWithin.restrict (single x 1) ⋯) z = F z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case right.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ (g ^ n) x ≠ 0

pp: case right.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z

Tactic:
·

Goal state after:
case right.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ (g ^ n) x ≠ 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case right.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z

Tactic:
·

Goal state after:
case right.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ^ n) z = (z - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z

pp: case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z

Tactic:
·

Goal state after:
case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case refine_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g

Tactic:
·

Goal state after:
case refine_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case neg
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
t0 : ↑I
htn1 : t0 ≤ t n.succ
htn : ¬t0 ≤ t n
hf : f (t0, a) ∉ (q e).target
⊢ g (t0, a) = g (t0, a)

Tactic:
·

Goal state after:
case neg
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
t0 : ↑I
htn1 : t0 ≤ t n.succ
htn : ¬t0 ≤ t n
hf : f (t0, a) ∉ (q e).target
⊢ g (t0, a) = g (t0, a)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z

Tactic:
·

Goal state after:
case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∑ i ∈ η₀.toFinset, divisor (canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R) = -divisor f (ball 0 R)

pp: case h₁f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ i ∈ η₀.toFinset, MeromorphicOn (canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R)

pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ i ∈ η₀.toFinset, ∀ z ∈ ball 0 R, meromorphicOrderAt (canonicalFactor R i ^ (divisor f (ball 0 R)) i) z ≠ ⊤

Tactic:
·

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∑ i ∈ η₀.toFinset, divisor (canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R) = -divisor f (ball 0 R)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case h₁f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ i ∈ η₀.toFinset, MeromorphicOn (canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R)

pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ i ∈ η₀.toFinset, ∀ z ∈ ball 0 R, meromorphicOrderAt (canonicalFactor R i ^ (divisor f (ball 0 R)) i) z ≠ ⊤

Tactic:
·

Goal state after:
case h₁f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ i ∈ η₀.toFinset, MeromorphicOn (canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ i ∈ η₀.toFinset, ∀ z ∈ ball 0 R, meromorphicOrderAt (canonicalFactor R i ^ (divisor f (ball 0 R)) i) z ≠ ⊤

Tactic:
·

Goal state after:
case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∀ i ∈ η₀.toFinset, ∀ z ∈ ball 0 R, meromorphicOrderAt (canonicalFactor R i ^ (divisor f (ball 0 R)) i) z ≠ ⊤
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 : 𝕜
hx : (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 : 𝕜
hx : 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 : 𝕜
hx : (fun x ↦ ↑(D u) * log ‖x - u‖) = 0
⊢ D u = 0