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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ IsOpen s
Tactic:
convert isOpen_image_coe ((↑) ⁻¹' s)
State after:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ s = Nat.cast '' (Nat.cast ⁻¹' s)

State before:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ s = Nat.cast '' (Nat.cast ⁻¹' s)
Tactic:
simp_rw [eq_comm (a := s), image_preimage_eq_iff, range_coe', Iio, lt_top_iff_ne_top,
  ← compl_singleton_eq, subset_compl_singleton_iff]
State after:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ ⊤ ∉ s

State before:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ ⊤ ∉ s
Tactic:
assumption
State after:
no goals