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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z ≠ ⊤

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
hd : ¬(support d).Finite
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z ≠ ⊤

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z ≠ ⊤
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x c : 𝕜
h : ¬MeromorphicAt f (x + c)
⊢ meromorphicTrailingCoeffAt (f ∘ fun x ↦ x + c) x = meromorphicTrailingCoeffAt f (x + c)

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x c : 𝕜
h : ¬¬MeromorphicAt f (x + c)
⊢ meromorphicTrailingCoeffAt (f ∘ fun x ↦ x + c) x = meromorphicTrailingCoeffAt f (x + c)

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x c : 𝕜
h : ¬MeromorphicAt f (x + c)
⊢ meromorphicTrailingCoeffAt (f ∘ fun x ↦ x + c) x = meromorphicTrailingCoeffAt f (x + c)
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
hd : ¬(support d).Finite
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z ≠ ⊤

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
hd : ¬(support d).Finite
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z ≠ ⊤
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
nneg : 0 ≤ meromorphicOrderAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g

pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g
g : 𝕜 → E
hg₁ : AnalyticAt 𝕜 g x
hg₂ : f =ᶠ[𝓝[≠] x] g
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
nneg : 0 ≤ meromorphicOrderAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : ¬u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : ¬u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : ¬u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g
g : 𝕜 → E
hg₁ : AnalyticAt 𝕜 g x
hg₂ : f =ᶠ[𝓝[≠] x] g
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[𝓝[≠] x] g
g : 𝕜 → E
hg₁ : AnalyticAt 𝕜 g x
hg₂ : f =ᶠ[𝓝[≠] x] g
⊢ 0 ≤ meromorphicOrderAt f x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inl
w x : ℂ
hx : x ∈ {w}ᶜ
⊢ AnalyticAt ℂ (fun z ↦ (↑0 ^ 2 - (starRingEnd ℂ) w * z) / (↑0 * (z - w))) x

pp: case inr
R : ℝ
w x : ℂ
hx : x ∈ {w}ᶜ
h : R ≠ 0
⊢ AnalyticAt ℂ (fun z ↦ (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))) x

Tactic:
·

Goal state after:
case inl
w x : ℂ
hx : x ∈ {w}ᶜ
⊢ AnalyticAt ℂ (fun z ↦ (↑0 ^ 2 - (starRingEnd ℂ) w * z) / (↑0 * (z - w))) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case refine_1
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ MeromorphicNFAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w

pp: case refine_2
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ ↑R ^ 2 - (starRingEnd ℂ) w * w ≠ 0

Tactic:
·

Goal state after:
case refine_1
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ MeromorphicNFAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case refine_2
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ ↑R ^ 2 - (starRingEnd ℂ) w * w ≠ 0

Tactic:
·

Goal state after:
case refine_2
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ ↑R ^ 2 - (starRingEnd ℂ) w * w ≠ 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset h)
y : 𝕜
hy : y ∈ Finite.toFinset h
hxy : x = y
⊢ meromorphicTrailingCoeffAt (fun x ↦ x - y) x ^ d y = (x - y) ^ update d x 0 y

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset h)
y : 𝕜
hy : y ∈ Finite.toFinset h
hxy : ¬x = y
⊢ meromorphicTrailingCoeffAt (fun x ↦ x - y) x ^ d y = (x - y) ^ update d x 0 y

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset h)
y : 𝕜
hy : y ∈ Finite.toFinset h
hxy : x = y
⊢ meromorphicTrailingCoeffAt (fun x ↦ x - y) x ^ d y = (x - y) ^ update d x 0 y
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inl
R : ℝ
z : ℂ
hz : z ∈ univ
h : z ∈ ball 0 R
⊢ MeromorphicNFAt (canonicalFactor R z) z

pp: case inr
R : ℝ
w : ℂ
h : w ∈ ball 0 R
z : ℂ
hz : z ∈ univ
h₁ : z ≠ w
⊢ MeromorphicNFAt (canonicalFactor R w) z

Tactic:
·

Goal state after:
case inl
R : ℝ
z : ℂ
hz : z ∈ univ
h : z ∈ ball 0 R
⊢ MeromorphicNFAt (canonicalFactor R z) z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset h)
y : 𝕜
hy : y ∈ Finite.toFinset h
hxy : ¬x = y
⊢ meromorphicTrailingCoeffAt (fun x ↦ x - y) x ^ d y = (x - y) ^ update d x 0 y

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset h)
y : 𝕜
hy : y ∈ Finite.toFinset h
hxy : ¬x = y
⊢ meromorphicTrailingCoeffAt (fun x ↦ x - y) x ^ d y = (x - y) ^ update d x 0 y
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
z : ℂ
hz : z ∈ univ
h : z ∈ ball 0 R
⊢ -1 < 0

Tactic:
by lia

Goal state after:
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
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = ⊤

pp: case neg
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : ¬e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : e = 0
⊢ meromorphicOrderAt (fun x ↦ e) 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
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : ¬e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst✝ : Decidable (e = 0)
he : ¬e = 0
⊢ meromorphicOrderAt (fun x ↦ e) z₀ = 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2.refine_8
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
⊢ (fun ta ↦ if ta.1 ≤ t n then g' ta else if f ta ∈ (q e).target then ↑(q e).symm (f ta) else g ta) (t0, a) = g (t0, a)

Tactic:
·

Goal state after:
case refine_2.refine_8
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
⊢ (fun ta ↦ if ta.1 ≤ t n then g' ta else if f ta ∈ (q e).target then ↑(q e).symm (f ta) else g ta) (t0, a) = g (t0, a)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case mp
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ ball 0 R
⊢ canonicalFactor R w z = 0 → z = w

pp: case mpr
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ ball 0 R
⊢ z = w → canonicalFactor R w z = 0

Tactic:
·

Goal state after:
case mp
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ ball 0 R
⊢ canonicalFactor R w z = 0 → z = w
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case mpr
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ ball 0 R
⊢ z = w → canonicalFactor R w z = 0

Tactic:
·

Goal state after:
case mpr
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ ball 0 R
⊢ z = w → canonicalFactor R w z = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
y : 𝕜
a✝ : y ∈ Finite.toFinset h✝
h : x = y
⊢ ‖(x - y) ^ update d x 0 y‖ ≠ 0

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
y : 𝕜
a✝ : y ∈ Finite.toFinset h✝
h : ¬x = y
⊢ ‖(x - y) ^ update d x 0 y‖ ≠ 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
y : 𝕜
a✝ : y ∈ Finite.toFinset h✝
h : x = y
⊢ ‖(x - y) ^ update d x 0 y‖ ≠ 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
y : 𝕜
a✝ : y ∈ Finite.toFinset h✝
h : ¬x = y
⊢ ‖(x - y) ^ update d x 0 y‖ ≠ 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
y : 𝕜
a✝ : y ∈ Finite.toFinset h✝
h : ¬x = y
⊢ ‖(x - y) ^ update d x 0 y‖ ≠ 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
x : 𝕜
f : 𝕜 → E
h₁ : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬¬MeromorphicAt f x
⊢ meromorphicOrderAt 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
x : 𝕜
f : 𝕜 → E
h₁ : ¬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 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt 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
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : w = 0
⊢ meromorphicOrderAt (canonicalFactor R w) 0 ≠ ⊤

pp: case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ meromorphicOrderAt (canonicalFactor R w) 0 ≠ ⊤

Tactic:
·

Goal state after:
case pos
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : w = 0
⊢ meromorphicOrderAt (canonicalFactor R w) 0 ≠ ⊤
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ canonicalFactor R w 0 ≠ 0

pp: case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ MeromorphicNFAt (canonicalFactor R w) 0

Tactic:
·

Goal state after:
case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ canonicalFactor R w 0 ≠ 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ MeromorphicNFAt (canonicalFactor R w) 0

Tactic:
·

Goal state after:
case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ MeromorphicNFAt (canonicalFactor R w) 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

pp: case neg
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∉ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
·

Goal state after:
case pos
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos.inl
R : ℝ
z : ℂ
hz hw : z ∈ ball 0 R
⊢ (meromorphicOrderAt (canonicalFactor R z) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single z 1) ⋯) z

pp: case pos.inr
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ (meromorphicOrderAt (canonicalFactor R w) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
·

Goal state after:
case pos.inl
R : ℝ
z : ℂ
hz hw : z ∈ ball 0 R
⊢ (meromorphicOrderAt (canonicalFactor R z) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single z 1) ⋯) z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos.inr
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ (meromorphicOrderAt (canonicalFactor R w) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
·

Goal state after:
case pos.inr
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ (meromorphicOrderAt (canonicalFactor R w) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
this✝ : ∀ y ∈ Finite.toFinset h✝, ‖(x - y) ^ update d x 0 y‖ ≠ 0
this : (support fun u ↦ ↑(d u) * log ‖x - u‖) ⊆ ↑(Finite.toFinset h✝)
y : 𝕜
hy : y ∈ Finite.toFinset h✝
h : x = y
⊢ ↑(update d x 0 y) * log ‖x - y‖ = ↑(d y) * log ‖x - y‖

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
this✝ : ∀ y ∈ Finite.toFinset h✝, ‖(x - y) ^ update d x 0 y‖ ≠ 0
this : (support fun u ↦ ↑(d u) * log ‖x - u‖) ⊆ ↑(Finite.toFinset h✝)
y : 𝕜
hy : y ∈ Finite.toFinset h✝
h : ¬x = y
⊢ ↑(update d x 0 y) * log ‖x - y‖ = ↑(d y) * log ‖x - y‖

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
this✝ : ∀ y ∈ Finite.toFinset h✝, ‖(x - y) ^ update d x 0 y‖ ≠ 0
this : (support fun u ↦ ↑(d u) * log ‖x - u‖) ⊆ ↑(Finite.toFinset h✝)
y : 𝕜
hy : y ∈ Finite.toFinset h✝
h : x = y
⊢ ↑(update d x 0 y) * log ‖x - y‖ = ↑(d y) * log ‖x - y‖
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
this✝ : ∀ y ∈ Finite.toFinset h✝, ‖(x - y) ^ update d x 0 y‖ ≠ 0
this : (support fun u ↦ ↑(d u) * log ‖x - u‖) ⊆ ↑(Finite.toFinset h✝)
y : 𝕜
hy : y ∈ Finite.toFinset h✝
h : ¬x = y
⊢ ↑(update d x 0 y) * log ‖x - y‖ = ↑(d y) * log ‖x - y‖

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h✝ : HasFiniteSupport d
this✝ : ∀ y ∈ Finite.toFinset h✝, ‖(x - y) ^ update d x 0 y‖ ≠ 0
this : (support fun u ↦ ↑(d u) * log ‖x - u‖) ⊆ ↑(Finite.toFinset h✝)
y : 𝕜
hy : y ∈ Finite.toFinset h✝
h : ¬x = y
⊢ ↑(update d x 0 y) * log ‖x - y‖ = ↑(d y) * log ‖x - y‖
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∉ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
·

Goal state after:
case neg
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∉ ball 0 R
⊢ (divisor (canonicalFactor R w) (ball 0 R)) z = (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z
Module: Mathlib.Analysis.Meromorphic.Order

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

pp: case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ MeromorphicAt 1 x

Tactic:
·

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

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ MeromorphicAt 1 x

Tactic:
·

Goal state after:
case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ ∅, MeromorphicAt (f i) x
⊢ MeromorphicAt 1 x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

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

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_1
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
w : ℂ
⊢ MeromorphicNFOn (canonicalFactor R w ^ F w) (ball 0 R)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

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

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 pos
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.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_5
F : ι → 𝕜 → 𝕜
h₁ : ∀ (c : ι), MeromorphicAt (F c) x
h₂ : ∀ (c : ι), meromorphicOrderAt (F c) x ≠ ⊤
hF : Function.HasFiniteMulSupport F
⊢ meromorphicOrderAt (∏ᶠ (c : ι), F c) x ≠ ⊤

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_5
F : ι → 𝕜 → 𝕜
h₁ : ∀ (c : ι), MeromorphicAt (F c) x
h₂ : ∀ (c : ι), meromorphicOrderAt (F c) x ≠ ⊤
hF : ¬Function.HasFiniteMulSupport F
⊢ meromorphicOrderAt (∏ᶠ (c : ι), F c) x ≠ ⊤

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_5
F : ι → 𝕜 → 𝕜
h₁ : ∀ (c : ι), MeromorphicAt (F c) x
h₂ : ∀ (c : ι), meromorphicOrderAt (F c) x ≠ ⊤
hF : Function.HasFiniteMulSupport F
⊢ meromorphicOrderAt (∏ᶠ (c : ι), F c) x ≠ ⊤