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

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
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
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑w → f y = 0) ∧ IsOpen t ∧ ↑w ∈ t

Tactic:
rw [h₁w]

Result:
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
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
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑z → f y = 0) ∧ IsOpen t ∧ ↑z ∈ t

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
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'
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑w → f y = 0) ∧ IsOpen t ∧ ↑w ∈ t

Tactic:
by_cases h₁w : w = z

Result:
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
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
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑w → f y = 0) ∧ IsOpen t ∧ ↑w ∈ t

case neg
𝕜 : 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
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
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑w → f y = 0) ∧ IsOpen t ∧ ↑w ∈ t

Proof state:
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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
⊢ w ∈ {u | ⋯.order = ⊤}ᶜ

Tactic:
simp only [mem_compl_iff, mem_setOf_eq]

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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
⊢ ¬⋯.order = ⊤

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
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
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑z → f y = 0) ∧ IsOpen t ∧ ↑z ∈ t

Tactic:
tauto

Result:
no goals

Proof state:
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'

Tactic:
exact ⟨isOpen_induced h₂t', h₃t'⟩

Result:
no goals

Proof state:
case right.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
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
⊢ w ∈ (fun ⦃w⦄ => t' ↑w) \ fun ⦃w⦄ => {↑z} ↑w

Tactic:
exact ⟨hw, mem_singleton_iff.not.1 (Subtype.coe_ne_coe.2 h₁w)⟩

Result:
no goals

Proof state:
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 = ⊤}ᶜ

Tactic:
intro w hw

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'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
⊢ w ∈ {u | ⋯.order = ⊤}ᶜ

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 : ⋯.order = ⊤
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, y ∈ {↑x}ᶜ → f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Tactic:
rw [MeromorphicAt.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] 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 : ∃ t, (∀ y ∈ t, y ∈ {↑z}ᶜ → f y = 0) ∧ IsOpen t ∧ ↑z ∈ t
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, y ∈ {↑x}ᶜ → f y = 0) ∧ IsOpen t ∧ ↑x ∈ t}, IsOpen x ∧ z ∈ x

Proof state:
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 : ⋯.order = ⊤
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Tactic:
tauto

Result:
no goals

Proof state:
case neg
𝕜 : 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
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
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑w → f y = 0) ∧ IsOpen t ∧ ↑w ∈ t

Tactic:
use t' \ {z.1}, fun y h₁y _ ↦ h₁t' y (mem_of_mem_diff h₁y) (mem_of_mem_inter_right h₁y)

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
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
⊢ IsOpen (t' \ {↑z}) ∧ ↑w ∈ t' \ {↑z}

Proof state:
case left.inr.intro.intro.intro
𝕜 : 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'
⊢ ∃ t ⊆ {u | ⋯.order = ⊤}ᶜ, IsOpen t ∧ z ∈ t

Tactic:
use Subtype.val ⁻¹' t'

Result:
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'