Theorem: Graph.morphism_terminal_commutes (Lectures/Graph.lean)

State before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e : EdgeBetween G v w
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₁), τ G₂ (f.toFuncE e) = f.toFuncV (τ G₁ e)
Tactic:
intro e
State after:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
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₁
⊢ τ G₂ (f.toFuncE e) = f.toFuncV (τ G₁ e)

State before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
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₁
⊢ τ G₂ (f.toFuncE e) = f.toFuncV (τ G₁ e)
Tactic:
rw [Graph.τ, Graph.τ, ←toFuncE_bar, ←toFuncV_init]
State after:
no goals