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

Goal state before:
pp: case mp.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : D u = 0
⊢ D u = 0

pp: case mp.inr.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : y = 0
⊢ D u = 0

pp: case mp.inr.inr.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = 1
⊢ D u = 0

pp: case mp.inr.inr.inr
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = -1
⊢ D u = 0

Tactic:
·

Goal state after:
case mp.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : D u = 0
⊢ D u = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case mp.inr.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : y = 0
⊢ D u = 0

pp: case mp.inr.inr.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = 1
⊢ D u = 0

pp: case mp.inr.inr.inr
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = -1
⊢ D u = 0

Tactic:
·

Goal state after:
case mp.inr.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : y = 0
⊢ D u = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case mp.inr.inr.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = 1
⊢ D u = 0

pp: case mp.inr.inr.inr
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = -1
⊢ D u = 0

Tactic:
·

Goal state after:
case mp.inr.inr.inl
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = 1
⊢ D u = 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
⊢ (Γ t) 1 = (Γ 0) 1

pp: case refine_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ (p ∘ fun st ↦ (Γ st.2) st.1) = ⇑((↑γ).comp ContinuousMap.prodSwap)

pp: case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ (0, x).2) (0, x).1

pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1

Tactic:
·

Goal state after:
case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
⊢ (Γ t) 1 = (Γ 0) 1
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case mp.inr.inr.inr
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = -1
⊢ D u = 0

Tactic:
·

Goal state after:
case mp.inr.inr.inr
𝕜 : 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
y : 𝕜
hy : 1 < ‖y‖
h : ‖y‖ = -1
⊢ D u = 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
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 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
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : R ≤ 0
⊢ ∃ g, CanonicalDecomp f g R

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : ¬R ≤ 0
⊢ ∃ g, CanonicalDecomp f g R

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : R ≤ 0
⊢ ∃ g, CanonicalDecomp f g R
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₂f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₂f₂ : ¬meromorphicOrderAt f₂ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₂f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ (p ∘ fun st ↦ (Γ st.2) st.1) = ⇑((↑γ).comp ContinuousMap.prodSwap)

pp: case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ (0, x).2) (0, x).1

pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ (p ∘ fun st ↦ (Γ st.2) st.1) = ⇑((↑γ).comp ContinuousMap.prodSwap)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := ⋯
g : 𝕜 → E := ⋯
⊢ AnalyticAt 𝕜 ((fun z ↦ (z - x) ^ (n₁ - n)) • g₁) x

pp: case hg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := ⋯
g : 𝕜 → E := ⋯
⊢ AnalyticAt 𝕜 ((fun z ↦ (z - x) ^ (n₂ - n)) • g₂) x

Tactic:
·

Goal state after:
case hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := ⋯
g : 𝕜 → E := ⋯
⊢ AnalyticAt 𝕜 ((fun z ↦ (z - x) ^ (n₁ - n)) • g₁) x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ (0, x).2) (0, x).1

pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ (0, x).2) (0, x).1
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1

Tactic:
·

Goal state after:
case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1
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)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
z : ℂ
hz : z ∈ closedBall 0 R
⊢ meromorphicOrderAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) z + meromorphicOrderAt f z ≠ ⊤

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
z : ℂ
hz : z ∈ closedBall 0 R
⊢ MeromorphicAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) 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)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
z : ℂ
hz : z ∈ closedBall 0 R
⊢ meromorphicOrderAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) z + meromorphicOrderAt f z ≠ ⊤
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)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
z : ℂ
hz : z ∈ closedBall 0 R
⊢ MeromorphicAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) 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)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
z : ℂ
hz : z ∈ closedBall 0 R
⊢ MeromorphicAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
⊢ ∃ g, CanonicalDecomp f g R

Tactic:
use g

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := ⋯
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := ⋯
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
⊢ CanonicalDecomp f g R