awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Order
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
h₂ h₃ : ∀ (y : 𝕜) (hy : y ∈ Uᶜ), AnalyticAt 𝕜 f y ∨ y ∉ U
⊢ ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∉ U

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy using Or.inr hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Order
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
rw : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ {x : 𝕜 | AnalyticAt 𝕜 f x}))
⊢ {x : 𝕜 | AnalyticAt 𝕜 f x} ∈ codiscreteWithin U

Tactic:
rw [mem_codiscreteWithin]

Premises used: mem_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.Order
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
rw : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, x ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ
⊢ Disjoint (𝓝[≠] x) (𝓟 (U \ {x : 𝕜 | AnalyticAt 𝕜 f x}))

Tactic:
rw [Filter.disjoint_principal_right, ← Filter.eventually_mem_set]

Premises used: Filter.eventually_mem_set, Filter.disjoint_principal_right
-- Module: Mathlib.Analysis.Meromorphic.Order
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 : ∀ (y : 𝕜) (hy : AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ), y ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, x ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ

Tactic:
filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with y hy

Premises used: MeromorphicOn.eventually_analyticAt_or_mem_compl
-- Module: Mathlib.Analysis.Meromorphic.Order
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 → AnalyticAt 𝕜 f y
⊢ y ∈ (U \ {x : 𝕜 | AnalyticAt 𝕜 f x})ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Order
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
h₁ : y ∈ U → ∀ (hy : y ∈ Uᶜ), AnalyticAt 𝕜 f y
h₂ h₃ : y ∈ U → ∀ (hy : AnalyticAt 𝕜 f y), AnalyticAt 𝕜 f y
⊢ y ∈ U → AnalyticAt 𝕜 f y

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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 : 𝕜) = ⊤}))
⊢ Membership.mem (γ := Filter (↑U : Type u_1)) (codiscrete (↑U : Type u_1))
    {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤}

Tactic:
rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin]

Premises used: mem_codiscreteWithin, mem_codiscrete_subtype_iff_mem_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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
⊢ 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 [Filter.disjoint_principal_right]

Premises used: Filter.disjoint_principal_right
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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
⊢ (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

Premises used: MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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 : 𝕜) = ⊤})ᶜ
⊢ (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:
filter_upwards [eventually_eventually_nhdsWithin.2 h₁f] with a h₁a

Premises used: Iff.mpr, eventually_eventually_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Order
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
this : ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 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:
simp +contextual [meromorphicOrderAt_eq_top_iff, this]

Premises used: meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
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 : ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 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:
suffices ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0 by
      simp +contextual [meromorphicOrderAt_eq_top_iff, this]
-- Module: Mathlib.Analysis.Meromorphic.Order
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
h₁ : ∀ (hax : a ≠ x), ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0

Tactic:
obtain rfl | hax := eq_or_ne a x

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Meromorphic.Order
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
a : 𝕜
hx : a ∈ U
h₁f h₁a : ∀ᶠ (x : 𝕜) in 𝓝[≠] a, f x = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0

Tactic:
h₁a
-- Module: Mathlib.Analysis.Meromorphic.Order
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
a : 𝕜
hx : a ∈ U
h₁f h₁a : ∀ᶠ (x : 𝕜) in 𝓝[≠] a, f x = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0

Tactic:
exact h₁a
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0

Tactic:
rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h₁a ⊢

Premises used: eventually_nhds_iff, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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
⊢ ∃ (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
-- Module: Mathlib.Analysis.Meromorphic.Order
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
right : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t \ {x}) ∧ a ∈ t \ {x}
⊢ ∃ (t : Set 𝕜),
    (∀ y ∈ t, Membership.mem (γ := Set 𝕜) {a}ᶜ y → f y = 0) ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ a ∈ t

Tactic:
use t \ {x}, fun y h₁y _ ↦ h₁t y h₁y.1 h₁y.2
-- Module: Mathlib.Analysis.Meromorphic.Order
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
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t \ {x}) ∧ a ∈ t \ {x}

Tactic:
⟨h₂t.sdiff isClosed_singleton, Set.mem_diff_of_mem h₃t hax⟩

Premises used: IsOpen.sdiff, And.intro, Set.mem_diff_of_mem, isClosed_singleton
-- Module: Mathlib.Analysis.Meromorphic.Order
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
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t \ {x}) ∧ a ∈ t \ {x}

Tactic:
exact ⟨h₂t.sdiff isClosed_singleton, Set.mem_diff_of_mem h₃t hax⟩
-- Module: Mathlib.Analysis.Meromorphic.Order
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
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 : 𝕜) = ⊤})ᶜ
⊢ (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:
filter_upwards [hf.eventually_analyticAt_or_mem_compl hx, h₁f] with a h₁a h'₁a

Premises used: MeromorphicOn.eventually_analyticAt_or_mem_compl
-- Module: Mathlib.Analysis.Meromorphic.Order
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 : a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
⊢ 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:
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]

Premises used: Set.mem_image, Subtype.exists, not_exists, exists_eq_right, Set.mem_setOf_eq, exists_and_right, not_or, Set.mem_diff, Decidable.not_not, not_and, Classical.not_forall, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
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 = ⊤
h₁ : ∀ (h' : a ∈ Uᶜ), a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤

Tactic:
rcases h₁a with h' | h'
-- Module: Mathlib.Analysis.Meromorphic.Order
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 : f a ≠ 0
h' : AnalyticAt 𝕜 f a
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤

Tactic:
simp +contextual [h'.meromorphicOrderAt_eq, h'.analyticOrderAt_eq_zero.2, h'₁a]

Premises used: Iff.mpr, AnalyticAt.meromorphicOrderAt_eq, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
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 : f a ≠ 0
h' : a ∈ Uᶜ
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤

Tactic:
fun ha ↦ (h' ha).elim

Premises used: False.elim
-- Module: Mathlib.Analysis.Meromorphic.Order
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 : f a ≠ 0
h' : a ∈ Uᶜ
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤

Tactic:
exact fun ha ↦ (h' ha).elim

Premises used: False.elim
-- Module: Mathlib.Analysis.Meromorphic.Order
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 ≠ ⊤
⊢ image (α := (↑U : Type u_1)) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ U))
      {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = 0 ∨ meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∈
    codiscreteWithin U

Tactic:
mem_codiscrete_subtype_iff_mem_codiscreteWithin.1
      h₁f.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top

Premises used: MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top, Iff.mp, mem_codiscrete_subtype_iff_mem_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.Order
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 ≠ ⊤
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 : 𝕜) = ⊤})
⊢ {u : 𝕜 | u ∈ U ∧ (meromorphicOrderAt f u = 0 ∨ meromorphicOrderAt f u = ⊤)} ∈ codiscreteWithin U

Tactic:
convert!
    mem_codiscrete_subtype_iff_mem_codiscreteWithin.1
      h₁f.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top

Premises used: MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top, Iff.mp, mem_codiscrete_subtype_iff_mem_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.Order
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 ≠ ⊤
⊢ 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:
aesop
-- Module: Mathlib.Analysis.Meromorphic.Order
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)
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)
⊢ 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'

Premises used: meromorphicOrderAt, eq_or_ne, Top.top
-- Module: Mathlib.Analysis.Meromorphic.Order
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 = ⊤
inl₁ : Ne (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)) 0
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)

Tactic:
rw [hf', WithTop.top_mul]

Premises used: WithTop.top_mul
-- Module: Mathlib.Analysis.Meromorphic.Order
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 : ∀ (hf' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ∘ g) z = 0
⊢ meromorphicOrderAt (f ∘ g) x = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff] at hf' ⊢

Premises used: meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
inl : ∀ᶠ (b : 𝕜) in map g (𝓝[≠] x), f b = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ∘ g) z = 0

Tactic:
rw [Function.comp_def, ← eventually_map (P := (f · = 0))]

Premises used: Filter.eventually_map, Function.comp_def
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
⊢ ∀ᶠ (b : 𝕜) in map g (𝓝[≠] x), f b = 0

Tactic:
EventuallyEq.filter_mono hf' (hg.map_nhdsNE hg_nc)

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq, AnalyticAt.map_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
⊢ ∀ᶠ (b : 𝕜) in map g (𝓝[≠] x), f b = 0

Tactic:
exact EventuallyEq.filter_mono hf' (hg.map_nhdsNE hg_nc)

Premises used: Filter.EventuallyEq.filter_mono, AnalyticAt.map_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.Order
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) = ⊤
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
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) = ⊤
⊢ Ne (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)) 0

Tactic:
simp [(show AnalyticAt 𝕜 (g · - g x) x by fun_prop).analyticOrderAt_eq_zero]

Premises used: AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
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)).untop₀ : WithTop ℤ)

Tactic:
have hr := (WithTop.coe_untop₀_of_ne_top hf').symm