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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
⊢ x ∈ P.partOf x
Tactic:
obtain ⟨_, ⟨h, -⟩⟩ := P.exists_unique_of_mem_set hx
State after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
w✝ : Set α
h : w✝ ∈ P ∧ x ∈ w✝
⊢ x ∈ P.partOf x

State before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
w✝ : Set α
h : w✝ ∈ P ∧ x ∈ w✝
⊢ x ∈ P.partOf x
Tactic:
exact mem_sUnion_of_mem h.2 h
State after:
no goals