Theorem: Graph.toFuncV_init (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:
exact f.toFuncV_init e
State after:
no goals