simp only [mul_path_path, map_on_quotient, Morphism.append_map]
case mk.mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
a : EdgePath G₁ v w
b : EdgePath G₁ w u
⊢ map f (Quot.mk Reduction a * Quot.mk Reduction b) = map f (Quot.mk Reduction a) * map f (Quot.mk Reduction b)
no goals