case H.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
x✝ : ConnectedComponent G'
a✝ : V'
⊢ ↑(connectedComponentEquiv (symm φ)) (Quot.mk (Reachable G') a✝) =
    ↑(connectedComponentEquiv φ).symm (Quot.mk (Reachable G') a✝)
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
⊢ connectedComponentEquiv (symm φ) = (connectedComponentEquiv φ).symm
ext ⟨_⟩
no goals
case H.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
x✝ : ConnectedComponent G'
a✝ : V'
⊢ ↑(connectedComponentEquiv (symm φ)) (Quot.mk (Reachable G') a✝) =
    ↑(connectedComponentEquiv φ).symm (Quot.mk (Reachable G') a✝)
rfl