awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
y : 𝕜
hU : IsPreconnected U
h₁x : x ∈ U
hy : y ∈ U
h₂x : meromorphicOrderAt f x ≠ ⊤
w : (↑U : Type u_1)
⊢ ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
have h : meromorphicOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) x h₁x) : 𝕜) ≠ ⊤
Tactic: use ⟨x, h₁x⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y
have this : U \ {x} ⊆ {x}ᶜ
Tactic: have : U \ {x} ⊆ {x}ᶜ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y
have this : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y
Tactic: have : ∀ᶠ y in 𝓝[U \ {x}] x, ContinuousAt f y := by
    have : U \ {x} ⊆ {x}ᶜ := by simp
    exact nhdsWithin_mono _ this (h x hx).eventually_continuousAt
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y
have h₁ : ∀ (y : 𝕜) (hy : ContinuousAt f y) (h'y : y ∈ U \ {x}), AnalyticAt 𝕜 f y
Tactic: filter_upwards [this, self_mem_nhdsWithin] with y hy h'y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
have this : {x}ᶜ = U \ {x} ∪ Uᶜ
Tactic: have : {x}ᶜ = (U \ {x}) ∪ Uᶜ := by aesop (add simp Classical.em)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
have rw : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x ⊔ 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
Tactic: rw [this, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
⊢ (∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U) ∧ ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∉ U
have refine_1 : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
refine_1 : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U
⊢ (∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U) ∧ ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∉ U
have refine_2 : ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∉ U
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U
have h₁ : ∀ (a : 𝕜),
  Membership.mem (γ := Set 𝕜)
    {x : 𝕜 |
      Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y) x} x →
        Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y ∨ y ∉ U) x} x}
    a
Tactic: filter_upwards [h.eventually_analyticAt hx] with y hy using Or.inl hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
h₁ :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y) x} x →
          Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y ∨ y ∉ U) x} x}
      a
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U
have h₂ : ∀ (a : 𝕜), AnalyticAt 𝕜 f a → AnalyticAt 𝕜 f a ∨ a ∉ U
Tactic: filter_upwards [h.eventually_analyticAt hx] with y hy using Or.inl hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∉ U
have h₁ : ∀ (a : 𝕜),
  Membership.mem (γ := Set 𝕜)
    {x : 𝕜 | x ∈ Uᶜ → Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y ∨ y ∉ U) x} x} a
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy using Or.inr hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
h₁ :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 | x ∈ Uᶜ → Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (y : 𝕜) ↦ AnalyticAt 𝕜 f y ∨ y ∉ U) x} x} a
⊢ ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∉ U
have h₂ : ∀ a ∈ Uᶜ, AnalyticAt 𝕜 f a ∨ a ∉ U
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy using Or.inr hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ {x : 𝕜 | AnalyticAt 𝕜 f x} ∈ codiscreteWithin U
have rw : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ {x : 𝕜 | AnalyticAt 𝕜 f x}))
Tactic: rw [mem_codiscreteWithin]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
⊢ Disjoint (𝓝[≠] x) (𝓟 (U \ {x : 𝕜 | AnalyticAt 𝕜 f x}))
have rw : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, x ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ
Tactic: rw [Filter.disjoint_principal_right, ← Filter.eventually_mem_set]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, x ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ
have h : ∀ (y : 𝕜) (hy : AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ), y ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ
Tactic: filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
y : 𝕜
hy : AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
⊢ y ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ
have h : y ∈ U → AnalyticAt 𝕜 f y
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
y : 𝕜
hy : AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
⊢ y ∈ U → AnalyticAt 𝕜 f y
have h : y ∈ U → ∀ (hy : AnalyticAt 𝕜 f y), AnalyticAt 𝕜 f y
Tactic: tauto
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
y : 𝕜
hy : AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
h : y ∈ U → ∀ (hy : AnalyticAt 𝕜 f y), AnalyticAt 𝕜 f y
⊢ y ∈ U → AnalyticAt 𝕜 f y
have h₁ : y ∈ U → ∀ (hy : y ∈ Uᶜ), AnalyticAt 𝕜 f y
Tactic: tauto
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ Membership.mem (γ := Filter (↑U : Type u_1)) (codiscrete (↑U : Type u_1))
    {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤}
have rw : ∀ x ∈ U,
  Disjoint (𝓝[≠] x)
    (𝓟
      (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤}))
Tactic: rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
⊢ Disjoint (𝓝[≠] x)
    (𝓟
      (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤}))
have rw : (U \
      image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
        {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
  𝓝[≠] x
Tactic: rw [Filter.disjoint_principal_right]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
⊢ (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x
have inl : ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0),
  (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x
Tactic: rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
inl :
  ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0),
    (U \
          image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
            {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
      𝓝[≠] x
⊢ (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x
have inr : ∀ (h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0),
  (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x
Tactic: rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x
have h : ∀ (a : 𝕜) (h₁a : ∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0),
  a ∈
    (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ
Tactic: filter_upwards [eventually_eventually_nhdsWithin.2 h₁f] with a h₁a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
h₁a : ∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0
⊢ a ∈
    (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ
have h : ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
Tactic: suffices ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0 by
      simp +contextual [meromorphicOrderAt_eq_top_iff, this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
h₁a : ∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
have h : ∀ (hx : a ∈ U) (h₁f h₁a : ∀ᶠ (x : 𝕜) in 𝓝[≠] a, f x = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
Tactic: obtain rfl | hax := eq_or_ne a x
Cleared hypotheses: x, hx, h₁f, h₁a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
h₁a : ∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0
h : ∀ (hx : a ∈ U) (h₁f h₁a : ∀ᶠ (x : 𝕜) in 𝓝[≠] a, f x = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
have h₁ : ∀ (hax : a ≠ x), ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
Tactic: obtain rfl | hax := eq_or_ne a x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
h₁a : ∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0
hax : a ≠ x
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
have h : ∀
  (h₁a :
    ∃ (t : Set 𝕜),
      (∀ y ∈ t, Membership.mem (γ := Set 𝕜) {x}ᶜ y → f y = 0) ∧
        IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ a ∈ t)
  (hax : a ≠ x),
  ∃ (t : Set 𝕜),
    (∀ y ∈ t, Membership.mem (γ := Set 𝕜) {a}ᶜ y → f y = 0) ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ a ∈ t
Tactic: rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h₁a ⊢
Cleared hypotheses: h₁a, hax
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
h₁a :
  ∃ (t : Set 𝕜),
    (∀ y ∈ t, Membership.mem (γ := Set 𝕜) {x}ᶜ y → f y = 0) ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ a ∈ t
hax : a ≠ x
⊢ ∃ (t : Set 𝕜),
    (∀ y ∈ t, Membership.mem (γ := Set 𝕜) {a}ᶜ y → f y = 0) ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ a ∈ t
have h : ∀ (t : Set 𝕜) (h₁t : ∀ y ∈ t, Membership.mem (γ := Set 𝕜) {x}ᶜ y → f y = 0)
  (h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) (h₃t : a ∈ t),
  ∃ (t : Set 𝕜),
    (∀ y ∈ t, Membership.mem (γ := Set 𝕜) {a}ᶜ y → f y = 0) ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ a ∈ t
Tactic: obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₁a
Cleared hypotheses: h₁a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
hax : a ≠ x
t : Set 𝕜
h₁t : ∀ y ∈ t, Membership.mem (γ := Set 𝕜) {x}ᶜ y → f y = 0
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : a ∈ t
⊢ ∃ (t : Set 𝕜),
    (∀ y ∈ t, Membership.mem (γ := Set 𝕜) {a}ᶜ y → f y = 0) ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ a ∈ t
have right : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t \ {x}) ∧ a ∈ t \ {x}
Tactic: use t \ {x}, fun y h₁y _ ↦ h₁t y h₁y.1 h₁y.2
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
⊢ (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ ∈
    𝓝[≠] x
have h : ∀ (a : 𝕜) (h₁a : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ) (h'₁a : f a ≠ 0),
  a ∈
    (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ
Tactic: filter_upwards [hf.eventually_analyticAt_or_mem_compl hx, h₁f] with a h₁a h'₁a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h₁a : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
h'₁a : f a ≠ 0
⊢ a ∈
    (U \
        image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
          {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})ᶜ
have h : a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
Tactic: simp only [mem_compl_iff, mem_diff, mem_image, mem_setOf_eq, Subtype.exists, exists_and_right,
      exists_eq_right, not_exists, not_or, not_and, not_forall, Decidable.not_not]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h₁a : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
h'₁a : f a ≠ 0
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
have h : ∀ (h' : AnalyticAt 𝕜 f a), a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
Tactic: rcases h₁a with h' | h'
Cleared hypotheses: h₁a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h₁a : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
h'₁a : f a ≠ 0
h : ∀ (h' : AnalyticAt 𝕜 f a), a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
have h₁ : ∀ (h' : a ∈ Uᶜ), a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
Tactic: rcases h₁a with h' | h'
Cleared hypotheses: h₁a
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
⊢ {u : 𝕜 | u ∈ U ∧ (meromorphicOrderAt f u = 0 ∨ meromorphicOrderAt f u = ⊤)} ∈ codiscreteWithin U
have h : Eq.{u_1 + 1} (α := Set 𝕜) {u : 𝕜 | u ∈ U ∧ (meromorphicOrderAt f u = 0 ∨ meromorphicOrderAt f u = ⊤)}
  (image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
    {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤})
Tactic: convert!
    mem_codiscrete_subtype_iff_mem_codiscreteWithin.1
      h₁f.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have inl : ∀ (hf' : meromorphicOrderAt f (g x) = ⊤),
  meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
Tactic: rcases eq_or_ne (meromorphicOrderAt f (g x)) ⊤ with hf' | hf'
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
inl :
  ∀ (hf' : meromorphicOrderAt f (g x) = ⊤),
    meromorphicOrderAt (f ∘ g) x =
      meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have inr : ∀ (hf' : meromorphicOrderAt f (g x) ≠ ⊤),
  meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
Tactic: rcases eq_or_ne (meromorphicOrderAt f (g x)) ⊤ with hf' | hf'
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have inl : meromorphicOrderAt (f ∘ g) x = ⊤
Tactic: rw [hf', WithTop.top_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
inl : meromorphicOrderAt (f ∘ g) x = ⊤
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
have inl₁ : Ne (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)) 0
Tactic: rw [hf', WithTop.top_mul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x = ⊤
have inl : ∀ (hf' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ∘ g) z = 0
Tactic: rw [meromorphicOrderAt_eq_top_iff] at hf' ⊢
Cleared hypotheses: hf'