Theorem: Partition.Rel.mem_left (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 : Set α
P : Partition s
h : P.Rel x y
⊢ x ∈ s
Tactic:
obtain ⟨t, htP, hxt, -⟩ := h
State after:
case intro.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 α
P : Partition s
t : Set α
htP : t ∈ P
hxt : x ∈ t
⊢ x ∈ s

State before:
case intro.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 α
P : Partition s
t : Set α
htP : t ∈ P
hxt : x ∈ t
⊢ x ∈ s
Tactic:
exact subset_of_mem htP hxt
State after:
no goals