Theorem: Graph.Graph.hom.preserve_terminal (GroupComp/Subgraph.lean)

State before:
V : Type u_2
E : Type u_3
V' : Type u_1
E' : Type u_4
G : Graph V E
G' : Graph V' E'
φ : hom G G'
e : E
⊢ φ.toFuncV (τ G e) = τ G' (φ.toFuncE e)
Tactic:
rw [← G.ι_bar, ← G'.ι_bar, preserve_init, preserve_bar]
State after:
no goals