case intro.intro
V : Type u
G : SimpleGraph V
P : Partition G
v : V
_h3 : ∀ (y : Set V), (fun b => ∃! x, v ∈ b) y → y = Exists.choose (_ : ∃! b x, v ∈ b)
h1 : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts
h2 :
  (fun x => v ∈ Exists.choose (_ : ∃! b x, v ∈ b)) h1 ∧
    ∀ (y : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts), (fun x => v ∈ Exists.choose (_ : ∃! b x, v ∈ b)) y → y = h1
⊢ v ∈ partOfVertex P v
V : Type u
G : SimpleGraph V
P : Partition G
v : V
⊢ v ∈ partOfVertex P v
obtain ⟨⟨h1, h2⟩, _h3⟩ := (P.isPartition.2 v).choose_spec
no goals
case intro.intro
V : Type u
G : SimpleGraph V
P : Partition G
v : V
_h3 : ∀ (y : Set V), (fun b => ∃! x, v ∈ b) y → y = Exists.choose (_ : ∃! b x, v ∈ b)
h1 : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts
h2 :
  (fun x => v ∈ Exists.choose (_ : ∃! b x, v ∈ b)) h1 ∧
    ∀ (y : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts), (fun x => v ∈ Exists.choose (_ : ∃! b x, v ∈ b)) y → y = h1
⊢ v ∈ partOfVertex P v
exact h2.1