case H.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
φ' : G' ≃g G''
x✝ : ConnectedComponent G
a✝ : V
⊢ ↑(connectedComponentEquiv (RelIso.trans φ φ')) (Quot.mk (Reachable G) a✝) =
    ↑((connectedComponentEquiv φ).trans (connectedComponentEquiv φ')) (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'
φ' : G' ≃g G''
⊢ connectedComponentEquiv (RelIso.trans φ φ') = (connectedComponentEquiv φ).trans (connectedComponentEquiv φ')
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'
φ' : G' ≃g G''
x✝ : ConnectedComponent G
a✝ : V
⊢ ↑(connectedComponentEquiv (RelIso.trans φ φ')) (Quot.mk (Reachable G) a✝) =
    ↑((connectedComponentEquiv φ).trans (connectedComponentEquiv φ')) (Quot.mk (Reachable G) a✝)
rfl