Theorem: Matroid.top_ne_bot (Matroid/Extension.lean)

State before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
⊢ ⊤ ≠ ⊥
Tactic:
rw [Ne, eq_comm, ModularCut.eq_top_iff]
State after:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
⊢ M.cl ∅ ∉ ⊥

State before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
⊢ M.cl ∅ ∉ ⊥
Tactic:
simp
State after:
no goals