Theorem: Graph.Morphism.reverse_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 : V₁
η : EdgePath G₁ u v
⊢ map (reverse η) f = reverse (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 : V₁
η : EdgePath G₁ u v
⊢ toList (map (reverse η) f) = toList (reverse (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 : V₁
η : EdgePath G₁ u v
⊢ toList (map (reverse η) f) = toList (reverse (map η f))
Tactic:
simp [map_toList, reverse_toList, List.map_reverse]
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 : V₁
η : EdgePath G₁ u v
⊢ List.map (f.toFuncE ∘ G₁.bar) (toList η) = List.map (G₂.bar ∘ f.toFuncE) (toList η)

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 : V₁
η : EdgePath G₁ u v
⊢ List.map (f.toFuncE ∘ G₁.bar) (toList η) = List.map (G₂.bar ∘ f.toFuncE) (toList η)
Tactic:
congr
State after:
case a.e_f
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 : V₁
η : EdgePath G₁ u v
⊢ f.toFuncE ∘ G₁.bar = G₂.bar ∘ f.toFuncE

State before:
case a.e_f
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 : V₁
η : EdgePath G₁ u v
⊢ f.toFuncE ∘ G₁.bar = G₂.bar ∘ f.toFuncE
Tactic:
funext e
State after:
case a.e_f.h
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 : V₁
η : EdgePath G₁ u v
e : E₁
⊢ (f.toFuncE ∘ G₁.bar) e = (G₂.bar ∘ f.toFuncE) e

State before:
case a.e_f.h
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 : V₁
η : EdgePath G₁ u v
e : E₁
⊢ (f.toFuncE ∘ G₁.bar) e = (G₂.bar ∘ f.toFuncE) e
Tactic:
simp only [Function.comp, f.toFuncE_bar]
State after:
no goals