rw [← p.toFuncV_init, h]
V : Type u
E : Type v
V₁ : Type ?u.89747
E₁ : Type ?u.89746
V₂ : Type ?u.89751
E₂ : Type ?u.89750
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
e₁ : E₁
h : v₁ = G₁.ι e₁
⊢ p.toFuncV v₁ = G₂.ι (p.toFuncE e₁)
no goals