Theorem: Partition.not_mem_empty (Matroid/ForMathlib/SetPartition.lean)

State before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α
⊢ a ∉ Partition.empty α
Tactic:
rw [← SetLike.mem_coe, empty_coe_eq]
State after:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α
⊢ a ∉ ∅

State before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α
⊢ a ∉ ∅
Tactic:
simp
State after:
no goals