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

State before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a s : α
⊢ a ∈ ⊤ ↔ a = s ∧ a ≠ ⊥
Tactic:
change a ∈ Partition.congr _ _ ↔ _
State after:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a s : α
⊢ a ∈ (ofIndependent' ⋯).congr ⋯ ↔ a = s ∧ a ≠ ⊥

State before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a s : α
⊢ a ∈ (ofIndependent' ⋯).congr ⋯ ↔ a = s ∧ a ≠ ⊥
Tactic:
rw [mem_congr_iff, mem_ofIndependent'_iff, mem_singleton_iff]
State after:
no goals