internlm/Lean-Github huggingface dataset:
Theorem: Graph.lifts_homotopic
Proof state before:
case hv
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₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ w✝¹ = w✝
Tactic:
rw [← edg₁.term_eq, ← edg₂.term_eq, edg_eq]
Proof state after:
no goals
Theorem: Graph.lifts_homotopic
Proof 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₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Graph.unique_Pathlift
Proof 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₂
Proof 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₂
Theorem: Graph.unique_Pathlift
Proof 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]
Proof 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₂
Theorem: Graph.unique_Pathlift
Proof 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
Proof 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₂
Theorem: Graph.unique_Pathlift
Proof 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
Proof 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₂
Theorem: Graph.unique_Pathlift
Proof 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
Proof state after:
no goals
Theorem: Graph.unique_Pathlift
Proof 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]
Proof state after:
no goals
Theorem: Graph.unique_Pathlift
Proof 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
Proof 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)
Theorem: Graph.unique_Pathlift
Proof 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
Proof state after:
no goals
Theorem: Graph.unique_Pathlift
Proof 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
Proof 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₂ }
Theorem: Graph.unique_Pathlift
Proof 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
Proof 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₂ }
Theorem: Graph.unique_Pathlift
Proof 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
Proof 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₂ }
Theorem: Graph.unique_Pathlift
Proof 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
Proof 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₂ }
Theorem: Graph.unique_Pathlift
Proof 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
Proof state after:
no goals
Theorem: Graph.unique_Pathlift
Proof 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
Proof 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₂
Theorem: Graph.unique_Pathlift
Proof 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
Proof state after:
no goals
Theorem: Graph.EdgePath.lift_append
Proof 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₂ u₂ : V₂
h : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
e' : EdgePath G₂ w₂ u₂
⊢ lift (e ++ e') p v₁ h =
    PathLift.append (lift e p v₁ h) (lift e' p (lift e p v₁ h).τ (_ : p.toFuncV (lift e p v₁ h).τ = w₂))
Tactic:
apply unique_Pathlift
Proof state after:
no goals
Theorem: Graph.EdgePath.lift_append_tail
Proof 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₂ u₂ : V₂
h : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
e' : EdgePath G₂ w₂ u₂
⊢ (lift (e ++ e') p v₁ h).τ =
    (PathLift.append (lift e p v₁ h) (lift e' p (lift e p v₁ h).τ (_ : p.toFuncV (lift e p v₁ h).τ = w₂))).τ
Tactic:
simp [lift_append]
Proof state after:
no goals
Theorem: Graph.EdgePath.lift_reverse
Proof 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 : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
⊢ lift (reverse e) p (lift e p v₁ h).τ (_ : p.toFuncV (lift e p v₁ h).τ = w₂) = PathLift.reverse p (lift e p v₁ h)
Tactic:
apply unique_Pathlift
Proof state after:
no goals