-- Mathlib/Analysis/Meromorphic/Order.lean
theorem isClopen_setOf_order_eq_top : IsClopen { u : U | (hf u.1 u.2).order = ⊤ }

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | ⋯.order = ⊤}ᶜ ∧ IsOpen (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Tactic:
constructor

Result:
case h.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | ⋯.order = ⊤}ᶜ

case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
⊢ IsOpen (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Proof state:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ¬⋯.order = ⊤

Tactic:
rwa [h₁w]

Result:
no goals

Proof state:
case left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Tactic:
rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h

Result:
case left.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z = 0
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

case left.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Proof state:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | ⋯.order = ⊤}
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, y ∈ {↑x}ᶜ → f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Tactic:
simp only [mem_setOf_eq] at hz

Result:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : ⋯.order = ⊤
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, y ∈ {↑x}ᶜ → f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Proof state:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ IsOpen {u | ⋯.order = ⊤}

Tactic:
apply isOpen_iff_forall_mem_open.mpr

Result:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ ∀ x ∈ {u | ⋯.order = ⊤}, ∃ t ⊆ {u | ⋯.order = ⊤}, IsOpen t ∧ x ∈ t