Theorem: Graph.unique_Pathlift (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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
⊢ ∀ (p₁ : PathLift p v₁ h₁ e) (p₂ : PathLift p v₁ h₂ e), p₁ = p₂
Tactic:
intro p₁ p₂
State after:
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
⊢ p₁ = p₂

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
⊢ p₁ = p₂
Tactic:
have eq_edgepath_aux :
  p₁.path.toList.map p.toFuncE =
    p₂.path.toList.map p.toFuncE := by
  rw [p₁.list_pushdown, p₂.list_pushdown]
State after:
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
⊢ p₁ = p₂

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
⊢ p₁ = p₂
Tactic:
have eq_edgepath : p₁.path.toList = p₂.path.toList := by
  apply lifts_homotopic p p₁.path p₂.path rfl
  apply eq_edgepath_aux
State after:
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
eq_edgepath : toList p₁.path = toList p₂.path
⊢ p₁ = p₂

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
eq_edgepath : toList p₁.path = toList p₂.path
⊢ p₁ = p₂
Tactic:
have term_eq : p₁.τ = p₂.τ :=
  terminal_eq_of_toList_eq p₁.path p₂.path eq_edgepath rfl
State after:
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
eq_edgepath : toList p₁.path = toList p₂.path
term_eq : p₁.τ = p₂.τ
⊢ p₁ = p₂

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
eq_edgepath : toList p₁.path = toList p₂.path
term_eq : p₁.τ = p₂.τ
⊢ p₁ = p₂
Tactic:
match p₁, p₂ with
| ⟨τ₁, path₁, h₁, lc₁⟩, ⟨τ₂, path₂, h₂, lc₂⟩ =>
have teq : τ₁ = τ₂ := term_eq
cases teq
have peq : path₁ = path₂ := by
  apply eq_of_toList_eq
  assumption
cases peq
rfl
State after:
no goals

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
⊢ List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
Tactic:
rw [p₁.list_pushdown, p₂.list_pushdown]
State after:
no goals

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
⊢ toList p₁.path = toList p₂.path
Tactic:
apply lifts_homotopic p p₁.path p₂.path rfl
State after:
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
⊢ List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
⊢ List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
Tactic:
apply eq_edgepath_aux
State after:
no goals

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
τ₂ : V₁
path₂ : EdgePath G₁ v₁ τ₂
h₂ : p.toFuncV τ₂ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }
Tactic:
have teq : τ₁ = τ₂ := term_eq
State after:
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
τ₂ : V₁
path₂ : EdgePath G₁ v₁ τ₂
h₂ : p.toFuncV τ₂ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
teq : τ₁ = τ₂
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
τ₂ : V₁
path₂ : EdgePath G₁ v₁ τ₂
h₂ : p.toFuncV τ₂ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
teq : τ₁ = τ₂
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }
Tactic:
cases teq
State after:
case refl
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
path₂ : EdgePath G₁ v₁ τ₁
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }

State before:
case refl
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
path₂ : EdgePath G₁ v₁ τ₁
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }
Tactic:
have peq : path₁ = path₂ := by
  apply eq_of_toList_eq
  assumption
State after:
case refl
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
path₂ : EdgePath G₁ v₁ τ₁
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
peq : path₁ = path₂
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }

State before:
case refl
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
path₂ : EdgePath G₁ v₁ τ₁
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
peq : path₁ = path₂
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }
Tactic:
cases peq
State after:
case refl.refl
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₁) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₁, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₁, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₁, path := path₁, term_pushdown := h₂, list_pushdown := lc₂ }

State before:
case refl.refl
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₁) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₁, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₁, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₁, path := path₁, term_pushdown := h₂, list_pushdown := lc₂ }
Tactic:
rfl
State after:
no goals

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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
path₂ : EdgePath G₁ v₁ τ₁
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ path₁ = path₂
Tactic:
apply eq_of_toList_eq
State after:
case a
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
path₂ : EdgePath G₁ v₁ τ₁
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ toList path₁ = toList path₂

State before:
case a
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁✝ h₂✝ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁✝ e
p₂ : PathLift p v₁ h₂✝ e
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
path₂ : EdgePath G₁ v₁ τ₁
h₂ : p.toFuncV τ₁ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₁, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ toList path₁ = toList path₂
Tactic:
assumption
State after:
no goals