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

Goal state before:
pp: case h.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | f =ᶠ[𝓝[≠] x] g}

pp: case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ U ⊆ {x | f =ᶠ[𝓝[≠] x] g}

Tactic:
·

Goal state after:
case h.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | f =ᶠ[𝓝[≠] x] g}
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ U ⊆ {x | f =ᶠ[𝓝[≠] x] g}

Tactic:
·

Goal state after:
case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ U ⊆ {x | f =ᶠ[𝓝[≠] x] g}
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ 0 < dist z c

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ 0 < dist z c

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ 0 < dist z c
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
hacc : AccPt x (𝓟 U)
⊢ {x | deriv f x = deriv g x} ∪ Uᶜ ∈ 𝓝[≠] x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
hacc : ¬AccPt x (𝓟 U)
⊢ {x | deriv f x = deriv g x} ∪ Uᶜ ∈ 𝓝[≠] x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
hacc : AccPt x (𝓟 U)
⊢ {x | deriv f x = deriv g x} ∪ Uᶜ ∈ 𝓝[≠] x
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
hacc : ¬AccPt x (𝓟 U)
⊢ {x | deriv f x = deriv g x} ∪ Uᶜ ∈ 𝓝[≠] x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
hacc : ¬AccPt x (𝓟 U)
⊢ {x | deriv f x = deriv g x} ∪ Uᶜ ∈ 𝓝[≠] x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case e'_2
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
this :
  ∀ (n : ℕ),
    ∃ 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
hN :
  ∃ g',
    ContinuousOn g' (Set.Icc 0 1 ×ˢ N) ∧
      p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x✝ : ↑I × A → E
a✝ : ↑I
⊢ x✝ (a✝, a) = g (a✝, a) ↔ a✝ ≤ 1 → x✝ (a✝, a) = g (a✝, a)

Tactic:
·

Goal state after:
case e'_2
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
this :
  ∀ (n : ℕ),
    ∃ 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
hN :
  ∃ g',
    ContinuousOn g' (Set.Icc 0 1 ×ˢ N) ∧
      p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x✝ : ↑I × A → E
a✝ : ↑I
⊢ x✝ (a✝, a) = g (a✝, a) ↔ a✝ ≤ 1 → x✝ (a✝, a) = g (a✝, a)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
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
⊢ ContinuousOn g (Set.Icc 0 (t Nat.zero) ×ˢ Set.univ)

pp: case refine_2
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)
⊢ ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n.succ) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n.succ, g' (t', a) = g (t', a)

Tactic:
·

Goal state after:
case refine_1
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
⊢ ContinuousOn g (Set.Icc 0 (t Nat.zero) ×ˢ Set.univ)
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U✝ : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ (fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) =ᶠ[codiscreteWithin U] 0

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U✝ : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : ¬MeromorphicOn f U
⊢ (fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) =ᶠ[codiscreteWithin U] 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U✝ : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ (fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) =ᶠ[codiscreteWithin U] 0
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U✝ : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : ¬MeromorphicOn f U
⊢ (fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) =ᶠ[codiscreteWithin U] 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U✝ : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : ¬MeromorphicOn f U
⊢ (fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0) =ᶠ[codiscreteWithin U] 0
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∉ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x
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
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∉ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∉ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∉ U
⊢ (divisor f₁ U) z = (divisor f₂ U) z

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : ¬z ∉ U
⊢ (divisor f₁ U) z = (divisor f₂ U) z

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∉ U
⊢ (divisor f₁ U) z = (divisor f₂ U) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : ¬MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∉ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x
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
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∉ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∉ U
⊢ (divisor f₁ U) x = (divisor f₂ U) x
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
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : ¬MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : ¬MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
⊢ 0 x ≤ (divisor f U) x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∉ U
⊢ 0 x ≤ (divisor f U) x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
⊢ 0 x ≤ (divisor f U) x
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∉ U
⊢ min ((divisor f₁ U) z) ((divisor f₂ U) z) ≤ (divisor (f₁ + f₂) U) z

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
⊢ min ((divisor f₁ U) z) ((divisor f₂ U) z) ≤ (divisor (f₁ + 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₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∉ U
⊢ min ((divisor f₁ U) z) ((divisor f₂ U) z) ≤ (divisor (f₁ + f₂) U) z
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 : 𝕜
⊢ MeromorphicNFAt f x → AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0 → MeromorphicNFAt 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 : 𝕜
⊢ MeromorphicNFAt f x → AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[𝓝 x] 0
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

pp: case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
·

Goal state after:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[𝓝 x] 0
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

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

Tactic:
·

Goal state after:
case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀