Theorem: ENat.isOpen_singleton (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n x : ℕ∞
hx : x ≠ ⊤
⊢ IsOpen {x}
Tactic:
lift x to ℕ using hx
State after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
x : ℕ
⊢ IsOpen {↑x}

State before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
x : ℕ
⊢ IsOpen {↑x}
Tactic:
rw [← image_singleton, ← openEmbedding_coe.open_iff_image_open]
State after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
x : ℕ
⊢ IsOpen {x}

State before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
x : ℕ
⊢ IsOpen {x}
Tactic:
exact trivial
State after:
no goals