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 (↑(Iso.symm φ) v') = connectedComponentMk G u ↔
    connectedComponentMk G' v' = map (RelEmbedding.toRelHom (RelIso.toRelEmbedding φ)) (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 (↑(Iso.symm φ) v') = C ↔
    connectedComponentMk G' v' = map (RelEmbedding.toRelHom (RelIso.toRelEmbedding φ)) 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 (↑(Iso.symm φ) v') = connectedComponentMk G u ↔
    connectedComponentMk G' v' = map (RelEmbedding.toRelHom (RelIso.toRelEmbedding φ)) (connectedComponentMk G u)
simp only [Iso.symm_apply_reachable, ConnectedComponent.eq, ConnectedComponent.map_mk,
  RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding]