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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ n = ⊤ ↔ ∀ (m : ℕ), ↑m < n
Tactic:
refine ⟨fun h m ↦ h ▸ coe_lt_top m ,fun h ↦ ?_⟩
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ n = ⊤

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ n = ⊤
Tactic:
rw [← not_not (a := (n = ⊤)), ← Ne, ne_top_iff_exists]
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ ¬∃ a, ↑a = n

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ ¬∃ a, ↑a = n
Tactic:
rintro ⟨a, rfl⟩
State after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
a : ℕ
h : ∀ (m : ℕ), ↑m < ↑a
⊢ False

State before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
a : ℕ
h : ∀ (m : ℕ), ↑m < ↑a
⊢ False
Tactic:
exact (h a).ne rfl
State after:
no goals