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

State before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s t : Set α
ht : t ∈ ofRel r
⊢ t.Nonempty
Tactic:
obtain ⟨x, hx, rfl⟩ := ht
State after:
case intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
x : α
hx : x ∈ {x | r x x}
⊢ ((fun a => {x | r a x}) x).Nonempty

State before:
case intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
x : α
hx : x ∈ {x | r x x}
⊢ ((fun a => {x | r a x}) x).Nonempty
Tactic:
exact ⟨x, hx⟩
State after:
no goals