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

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) f) (map (p₁ ++ p₂) f)
Tactic:
simp [append_map, cons_map]
State after:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map p₁ f ++ cons (EdgeBetween.map f e) (cons (EdgeBetween.map f (EdgeBetween.bar e)) (map p₂ f)))
    (map p₁ f ++ map p₂ f)

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map p₁ f ++ cons (EdgeBetween.map f e) (cons (EdgeBetween.map f (EdgeBetween.bar e)) (map p₂ f)))
    (map p₁ f ++ map p₂ f)
Tactic:
rw [← EdgeBetween.map_bar]
State after:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map p₁ f ++ cons (EdgeBetween.map f e) (cons (EdgeBetween.bar (EdgeBetween.map f e)) (map p₂ f)))
    (map p₁ f ++ map p₂ f)

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map p₁ f ++ cons (EdgeBetween.map f e) (cons (EdgeBetween.bar (EdgeBetween.map f e)) (map p₂ f)))
    (map p₁ f ++ map p₂ f)
Tactic:
apply Reduction.step
State after:
no goals