Theorem: Graph.Morphism.comp_toFuncV (GroupComp/Graph/Covering.lean)

State before:
V₁ : Type u_5
E₁ : Type u_6
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
f : Morphism G₁ G₂
v : V₁
⊢ (comp g f).toFuncV v = g.toFuncV (f.toFuncV v)
Tactic:
rfl
State after:
no goals