case intro
V : Type u
G : SimpleGraph V
P : Partition G
v : V
h : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts
⊢ partOfVertex P v ∈ P.parts
V : Type u
G : SimpleGraph V
P : Partition G
v : V
⊢ partOfVertex P v ∈ P.parts
obtain ⟨h, -⟩ := (P.isPartition.2 v).choose_spec.1
no goals
case intro
V : Type u
G : SimpleGraph V
P : Partition G
v : V
h : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts
⊢ partOfVertex P v ∈ P.parts
exact h