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

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
e : EdgeBetween G₁ u v
η : EdgePath G₁ v w
⊢ map (cons e η) f = cons (EdgeBetween.map f e) (map η f)
Tactic:
apply eq_of_toList_eq
State after:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
e : EdgeBetween G₁ u v
η : EdgePath G₁ v w
⊢ toList (map (cons e η) f) = toList (cons (EdgeBetween.map f e) (map η f))

State before:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
e : EdgeBetween G₁ u v
η : EdgePath G₁ v w
⊢ toList (map (cons e η) f) = toList (cons (EdgeBetween.map f e) (map η f))
Tactic:
simp [map_toList, EdgeBetween.map_toList, cons_toList]
State after:
no goals