∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {v' : V'}
  {C : G.ConnectedComponent},
  (G.connectedComponentMk (φ.symm v') = C) =
    (G'.connectedComponentMk v' = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C)