V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
v : V
v' : V'
C : ConnectedComponent G
u : V
⊢ connectedComponentMk G' (↑φ v) = map (RelEmbedding.toRelHom (RelIso.toRelEmbedding φ)) (connectedComponentMk G u) ↔
    connectedComponentMk G v = connectedComponentMk G u
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
v : V
v' : V'
C : ConnectedComponent G
⊢ connectedComponentMk G' (↑φ v) = map (RelEmbedding.toRelHom (RelIso.toRelEmbedding φ)) C ↔
    connectedComponentMk G v = C
refine' C.ind fun u => _
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
v : V
v' : V'
C : ConnectedComponent G
u : V
⊢ connectedComponentMk G' (↑φ v) = map (RelEmbedding.toRelHom (RelIso.toRelEmbedding φ)) (connectedComponentMk G u) ↔
    connectedComponentMk G v = connectedComponentMk G u
simp only [Iso.reachable_iff, ConnectedComponent.map_mk, RelEmbedding.coe_toRelHom,
  RelIso.coe_toRelEmbedding, ConnectedComponent.eq]