Theorem: Graph.EdgeBetween.map_bar (GroupComp/Graph/Covering.lean)

State before:
V : Type u
E : Type v
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₂
v₁ w₁ : V₁
e : EdgeBetween G₁ v₁ w₁
⊢ bar (map f e) = map f (bar e)
Tactic:
ext
State after:
case edge
V : Type u
E : Type v
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₂
v₁ w₁ : V₁
e : EdgeBetween G₁ v₁ w₁
⊢ (bar (map f e)).edge = (map f (bar e)).edge

State before:
case edge
V : Type u
E : Type v
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₂
v₁ w₁ : V₁
e : EdgeBetween G₁ v₁ w₁
⊢ (bar (map f e)).edge = (map f (bar e)).edge
Tactic:
simp [f.toFuncE_bar, EdgeBetween.map]
State after:
no goals