rw [← G.ι_bar, ← G'.ι_bar, preserve_init, preserve_bar]
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)
no goals