V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : ConnectedComponent G
⊢ ∀ (v : V), map Hom.id (connectedComponentMk G v) = connectedComponentMk G v
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : ConnectedComponent G
⊢ map Hom.id C = C
refine' C.ind _
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : ConnectedComponent G
⊢ ∀ (v : V), map Hom.id (connectedComponentMk G v) = connectedComponentMk G v
exact fun _ => rfl