Theorem: Graph.homotopy_step_lift
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₂ w₂' u₂ : V₂
h : p.toFuncV v₁ = v₂
η₁ : EdgePath G₂ v₂ w₂
e : EdgeBetween G₂ w₂ w₂'
η₂ : EdgePath G₂ w₂ u₂
θ₁ : PathLift p v₁ h η₁ := lift η₁ p v₁ h
w₁ : V₁ := θ₁.τ
hw : p.toFuncV w₁ = w₂ := θ₁.term_pushdown
edgeLift : E₁ := Morphism.localSection p w₁ e.edge (_ : p.toFuncV w₁ = G₂.ι e.edge)
e' : EdgeBetween G₁ w₁ (τ G₁ edgeLift) :=
  { edge := edgeLift, init_eq := (_ : G₁.ι (Morphism.localSection p w₁ e.edge (_ : p.toFuncV w₁ = G₂.ι e.edge)) = w₁),
    term_eq := (_ : τ G₁ edgeLift = τ G₁ edgeLift) }
θ₂ : PathLift p w₁ hw η₂ := lift η₂ p w₁ hw
liftTailCanc : PathLift p w₁ hw (cons e (cons (EdgeBetween.bar e) η₂)) :=
  { τ := θ₂.τ, path := cons e' (cons (EdgeBetween.bar e') θ₂.path), term_pushdown := (_ : p.toFuncV θ₂.τ = u₂),
    list_pushdown :=
      (_ :
        List.map p.toFuncE (toList (cons e' (cons (EdgeBetween.bar e') θ₂.path))) =
          toList (cons e (cons (EdgeBetween.bar e) η₂))) }
liftCanc : PathLift p v₁ h (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) := PathLift.append θ₁ liftTailCanc
splitLift : lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h = liftCanc
splitLift' : lift (η₁ ++ η₂) p v₁ h = PathLift.append θ₁ θ₂
path1 : liftCanc.path = θ₁.path ++ cons e' (cons (EdgeBetween.bar e') θ₂.path)
⊢ { τ := θ₂.τ, pathClass := [[liftCanc.path]] } = { τ := θ₂.τ, pathClass := [[(PathLift.append θ₁ θ₂).path]] }
Tactic:
have : [[ liftCanc.path ]] = [[ (θ₁.append θ₂).path ]] := by
  apply Quot.sound
  rw [path1]
  apply Reduction.step
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₂ w₂' u₂ : V₂
h : p.toFuncV v₁ = v₂
η₁ : EdgePath G₂ v₂ w₂
e : EdgeBetween G₂ w₂ w₂'
η₂ : EdgePath G₂ w₂ u₂
θ₁ : PathLift p v₁ h η₁ := lift η₁ p v₁ h
w₁ : V₁ := θ₁.τ
hw : p.toFuncV w₁ = w₂ := θ₁.term_pushdown
edgeLift : E₁ := Morphism.localSection p w₁ e.edge (_ : p.toFuncV w₁ = G₂.ι e.edge)
e' : EdgeBetween G₁ w₁ (τ G₁ edgeLift) :=
  { edge := edgeLift, init_eq := (_ : G₁.ι (Morphism.localSection p w₁ e.edge (_ : p.toFuncV w₁ = G₂.ι e.edge)) = w₁),
    term_eq := (_ : τ G₁ edgeLift = τ G₁ edgeLift) }
θ₂ : PathLift p w₁ hw η₂ := lift η₂ p w₁ hw
liftTailCanc : PathLift p w₁ hw (cons e (cons (EdgeBetween.bar e) η₂)) :=
  { τ := θ₂.τ, path := cons e' (cons (EdgeBetween.bar e') θ₂.path), term_pushdown := (_ : p.toFuncV θ₂.τ = u₂),
    list_pushdown :=
      (_ :
        List.map p.toFuncE (toList (cons e' (cons (EdgeBetween.bar e') θ₂.path))) =
          toList (cons e (cons (EdgeBetween.bar e) η₂))) }
liftCanc : PathLift p v₁ h (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) := PathLift.append θ₁ liftTailCanc
splitLift : lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h = liftCanc
splitLift' : lift (η₁ ++ η₂) p v₁ h = PathLift.append θ₁ θ₂
path1 : liftCanc.path = θ₁.path ++ cons e' (cons (EdgeBetween.bar e') θ₂.path)
this : [[liftCanc.path]] = [[(PathLift.append θ₁ θ₂).path]]
⊢ { τ := θ₂.τ, pathClass := [[liftCanc.path]] } = { τ := θ₂.τ, pathClass := [[(PathLift.append θ₁ θ₂).path]] }