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₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - 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
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁)) x

Tactic:
apply AnalyticAt.zpow_nonneg (by fun_prop)
      (sub_nonneg.2 (le_of_lt (WithTop.coe_lt_coe.1 h)))

Premises used: Iff.mpr, le_of_lt, WithTop.coe_lt_coe, AnalyticAt.zpow_nonneg, Iff.mp, sub_nonneg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x ≠ 0

Tactic:
simpa [zero_zpow _ <| sub_ne_zero.mpr (WithTop.coe_lt_coe.1 h).ne']

Premises used: Iff.mpr, zero_zpow, sub_ne_zero, LT.lt.ne', WithTop.coe_lt_coe, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
h₁ :
  ∀ (a : 𝕜),
    f₁ a = (a - x) ^ n₁ • g₁ a →
      f₂ a = (a - x) ^ n₂ • g₂ a →
        Membership.mem (γ := Set 𝕜) {x}ᶜ a →
          (f₁ + f₂) a = (a - x) ^ n₁ • (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) a
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) z

Tactic:
filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin]

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₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ ∀ (a : 𝕜),
    f₁ a = (a - x) ^ n₁ • g₁ a →
      f₂ a = (a - x) ^ n₂ • g₂ a →
        Membership.mem (γ := Set 𝕜) {x}ᶜ a →
          (f₁ + f₂) a = (a - x) ^ n₁ • (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) a

Tactic:
simp_all [smul_add, ← smul_assoc, ← zpow_add', sub_ne_zero]

Premises used: smul_assoc, sub_ne_zero, zpow_add', smul_add
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x
rw : meromorphicOrderAt (f₂ + f₁) x = meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₂ + f₁) x = meromorphicOrderAt f₂ x

Tactic:
meromorphicOrderAt_add_eq_left_of_lt hf₁ h

Premises used: meromorphicOrderAt_add_eq_left_of_lt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₂ + f₁) x = meromorphicOrderAt f₂ x

Tactic:
exact meromorphicOrderAt_add_eq_left_of_lt hf₁ h

Premises used: meromorphicOrderAt_add_eq_left_of_lt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
inl :
  ∀ (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x),
    meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)
inr :
  ∀ (h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x),
    meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

Tactic:
rcases lt_or_lt_iff_ne.mpr h with h | h

Premises used: Iff.mpr, lt_or_lt_iff_ne
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h_1 : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

Tactic:
simpa [h.le] using meromorphicOrderAt_add_eq_left_of_lt hf₂ h

Premises used: meromorphicOrderAt_add_eq_left_of_lt, LT.lt.le
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h_1 : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

Tactic:
simpa [h.le] using meromorphicOrderAt_add_eq_right_of_lt hf₁ h

Premises used: LT.lt.le, meromorphicOrderAt_add_eq_right_of_lt
-- 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
hU : IsConnected U
mp :
  (∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) →
    ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
mpr :
  (∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) →
    ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ (∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) ↔
    ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
constructor
-- 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
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ PreconnectedSpace.{u_1} (↑U : Type u_1)

Tactic:
have := isPreconnected_iff_preconnectedSpace.1 hU.isPreconnected
-- 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
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
mp :
  ∀ (h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅)
    (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
mp₁ :
  ∀ (h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ)
    (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
rcases isClopen_iff.1 hf.isClopen_setOf_meromorphicOrderAt_eq_top with h | h

Premises used: MeromorphicOn.isClopen_setOf_meromorphicOrderAt_eq_top, isClopen_iff, Iff.mp
-- 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
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅
u : (↑U : Type u_1)
⊢ u ∉ ∅

Tactic:
fun a => a

Premises used: Set.Mem, Not
-- 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
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅
u : (↑U : Type u_1)
⊢ u ∉ ∅

Tactic:
exact fun a => 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
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅
u : (↑U : Type u_1)
⊢ u ∉ ∅

Tactic:
have : u ∉ (∅ : Set U) := by exact fun a => 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
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this_1 : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅
u : (↑U : Type u_1)
this : u ∉ ∅
⊢ u ∉ {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤}

Tactic:
rw [← h] at 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
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this_1 : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} ∅
u : (↑U : Type u_1)
this : u ∉ {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤}
⊢ meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤

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
hU : IsConnected U
h₂f : ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ
mp :
  ∀ (u : (↑U : Type u_1)) (hU : meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤) (u : (↑U : Type u_1)),
    meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
obtain ⟨u, hU⟩ := h₂f
-- 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
hU_1 : IsConnected U
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ
u : (↑U : Type u_1)
hU : meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ Membership.mem (γ := Set (↑U : Type u_1)) univ u

Tactic:
trivial
-- 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
hU_1 : IsConnected U
this : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ
u : (↑U : Type u_1)
hU : meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ Membership.mem (γ := Set (↑U : Type u_1)) univ u

Tactic:
have : u ∈ univ := by trivial
-- 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
hU_1 : IsConnected U
this_1 : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ
u : (↑U : Type u_1)
hU : meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : Membership.mem (γ := Set (↑U : Type u_1)) univ u
⊢ Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} u

Tactic:
rw [← h] at 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
hU_1 : IsConnected U
this_1 : PreconnectedSpace.{u_1} (↑U : Type u_1)
h : Eq.{u_1 + 1} (α := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} univ
u : (↑U : Type u_1)
hU : meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
this : Membership.mem (γ := Set (↑U : Type u_1)) {u : (↑U : Type u_1) | meromorphicOrderAt f (↑u : 𝕜) = ⊤} u
⊢ ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤

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
hU : IsConnected U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
mpr : ∀ (v : 𝕜) (hv : v ∈ U), ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
⊢ ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
obtain ⟨v, hv⟩ := hU.nonempty

Premises used: IsConnected.nonempty
-- 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
hU : IsConnected U
h₂f : ∀ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤
v : 𝕜
hv : v ∈ U
w : (↑U : Type u_1)
h : meromorphicOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) v hv) : 𝕜) ≠ ⊤
⊢ ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
use ⟨v, hv⟩, h₂f ⟨v, hv⟩

Premises used: Subtype.mk
-- 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 𝕜
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)
h : meromorphicOrderAt f (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ U) x h₁x) : 𝕜) ≠ ⊤
⊢ ∃ (u : (↑U : Type u_1)), meromorphicOrderAt f (↑u : 𝕜) ≠ ⊤

Tactic:
use ⟨x, h₁x⟩
-- 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
⊢ U \ {x} ⊆ {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
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
⊢ U \ {x} ⊆ {x}ᶜ

Tactic:
have : U \ {x} ⊆ {x}ᶜ := by 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
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : U \ {x} ⊆ {x}ᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y

Tactic:
nhdsWithin_mono _ this (h x hx).eventually_continuousAt

Premises used: Filter.Eventually, MeromorphicAt.eventually_continuousAt, nhdsWithin_mono
-- 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 : U \ {x} ⊆ {x}ᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y

Tactic:
exact nhdsWithin_mono _ this (h x hx).eventually_continuousAt

Premises used: MeromorphicAt.eventually_continuousAt, nhdsWithin_mono
-- 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
⊢ ∀ᶠ (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
-- 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 : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y
h₁ : ∀ (y : 𝕜) (hy : ContinuousAt f y) (h'y : y ∈ U \ {x}), AnalyticAt 𝕜 f y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y

Tactic:
filter_upwards [this, self_mem_nhdsWithin] with y hy h'y

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
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y
y : 𝕜
hy : ContinuousAt f y
h'y : y ∈ U \ {x}
⊢ AnalyticAt 𝕜 f y

Tactic:
(h y h'y.1).analyticAt hy

Premises used: MeromorphicAt.analyticAt, And.left
-- 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 : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y
y : 𝕜
hy : ContinuousAt f y
h'y : y ∈ U \ {x}
⊢ AnalyticAt 𝕜 f y

Tactic:
exact (h y h'y.1).analyticAt hy

Premises used: MeromorphicAt.analyticAt, And.left
-- 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
⊢ {x}ᶜ = U \ {x} ∪ Uᶜ

Tactic:
aesop (add simp Classical.em)

Premises used: Classical.em
-- 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
⊢ {x}ᶜ = U \ {x} ∪ Uᶜ

Tactic:
have : {x}ᶜ = (U \ {x}) ∪ Uᶜ := by aesop (add simp Classical.em)
-- 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ᶜ
rw : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x ⊔ 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ

Tactic:
rw [this, nhdsWithin_union]

Premises used: nhdsWithin_union
-- 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ᶜ
⊢ (∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U) ∧ ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] x, AnalyticAt 𝕜 f y ∨ y ∉ U

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- 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ᶜ
refine_1 : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U
refine_2 : ∀ᶠ (y : 𝕜) in 𝓝[Uᶜ] 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

Tactic:
refine ⟨?_, ?_⟩
-- 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ᶜ
y : 𝕜
hy : AnalyticAt 𝕜 f y
⊢ AnalyticAt 𝕜 f y ∨ y ∉ U

Tactic:
Or.inl hy

Premises used: Or.inl
-- 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 : 𝕜 |
        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
h₂ h₃ : ∀ (y : 𝕜) (hy : AnalyticAt 𝕜 f y), AnalyticAt 𝕜 f y ∨ y ∉ U
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, AnalyticAt 𝕜 f y ∨ y ∉ U

Tactic:
filter_upwards [h.eventually_analyticAt hx] with y hy using Or.inl hy

Premises used: MeromorphicOn.eventually_analyticAt
-- 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ᶜ
y : 𝕜
hy : y ∈ Uᶜ
⊢ AnalyticAt 𝕜 f y ∨ y ∉ U

Tactic:
Or.inr hy

Premises used: Or.inr