Theorem: Graph.toFuncV_term (GroupComp/Graph/Covering.lean)

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
⊢ ∀ (e : E₁), f.toFuncV (τ G₁ e) = τ G₂ (f.toFuncE e)
Tactic:
intro e
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncV (τ G₁ e) = τ G₂ (f.toFuncE e)

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncV (τ G₁ e) = τ G₂ (f.toFuncE e)
Tactic:
rw [Graph.τ, Graph.τ, ←toFuncE_bar, ←toFuncV_init]
State after:
no goals