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

State before:
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₁)
Tactic:
rw [← p.toFuncV_init, h]
State after:
no goals