Theorem: Graph.homotopy_step_lift (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₂ w₂' u₂ : V₂
h : p.toFuncV v₁ = v₂
η₁ : EdgePath G₂ v₂ w₂
e : EdgeBetween G₂ w₂ w₂'
η₂ : EdgePath G₂ w₂ u₂
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let θ₁ := η₁.lift p v₁ h
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let w₁ := θ₁.τ
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₁ := θ₁.τ
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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₁ := θ₁.τ
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let hw : p.toFuncV w₁ = w₂ := θ₁.term_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₂ 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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let edgeLift := p.localSection w₁ e.edge (by rw [hw, e.init_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₂ 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)
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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)
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let e' : EdgeBetween G₁ w₁ (G₁.τ edgeLift) :=
        ⟨edgeLift, p.init_localSection _ _ _, 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₂ 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.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let θ₂ := η₂.lift p w₁ hw
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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) η₂))) }
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let liftCanc :=
  θ₁.append liftTailCanc
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
have splitLift :
  (η₁ ++ (cons e (cons e.bar η₂))).lift p v₁ h  =
    liftCanc := by
      apply unique_Pathlift
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
rw [splitLift]
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
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
have splitLift' :
  (η₁ ++ η₂).lift p v₁ h =
    θ₁.append θ₂ := by
      apply unique_Pathlift
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 θ₁ θ₂
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)

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 θ₁ θ₂
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
rw [splitLift']
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 θ₁ θ₂
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (PathLift.append θ₁ θ₂)

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 θ₁ θ₂
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (PathLift.append θ₁ θ₂)
Tactic:
show (⟨θ₂.τ, [[ liftCanc.path ]]⟩ : PathClassFrom G₁ v₁) =
  ⟨θ₂.τ, [[ (θ₁.append θ₂).path ]]⟩
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 θ₁ θ₂
⊢ { τ := θ₂.τ, pathClass := [[liftCanc.path]] } = { τ := θ₂.τ, pathClass := [[(PathLift.append θ₁ θ₂).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₂ 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 θ₁ θ₂
⊢ { τ := θ₂.τ, pathClass := [[liftCanc.path]] } = { τ := θ₂.τ, pathClass := [[(PathLift.append θ₁ θ₂).path]] }
Tactic:
have path1 : liftCanc.path =
  θ₁.path ++ (cons e' (cons e'.bar θ₂.path)) := by
    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₂ 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]] }

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
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]] }

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)
this : [[liftCanc.path]] = [[(PathLift.append θ₁ θ₂).path]]
⊢ { τ := θ₂.τ, pathClass := [[liftCanc.path]] } = { τ := θ₂.τ, pathClass := [[(PathLift.append θ₁ θ₂).path]] }
Tactic:
rw [this]
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₂ 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
⊢ p.toFuncV w₁ = G₂.ι e.edge
Tactic:
rw [hw, e.init_eq]
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₂ 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
⊢ List.map p.toFuncE (toList (cons e' (cons (EdgeBetween.bar e') θ₂.path))) =
    toList (cons e (cons (EdgeBetween.bar e) η₂))
Tactic:
simp [cons_toList, p.toFuncE_localSection, EdgeBetween.bar]
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
⊢ p.toFuncE (G₁.bar (Morphism.localSection p (lift η₁ p v₁ h).τ e.edge (_ : p.toFuncV w₁ = G₂.ι e.edge))) =
      G₂.bar e.edge ∧
    List.map p.toFuncE (toList (lift η₂ p (lift η₁ p v₁ h).τ (_ : p.toFuncV (lift η₁ p v₁ h).τ = w₂)).path) = toList η₂

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
⊢ p.toFuncE (G₁.bar (Morphism.localSection p (lift η₁ p v₁ h).τ e.edge (_ : p.toFuncV w₁ = G₂.ι e.edge))) =
      G₂.bar e.edge ∧
    List.map p.toFuncE (toList (lift η₂ p (lift η₁ p v₁ h).τ (_ : p.toFuncV (lift η₁ p v₁ h).τ = w₂)).path) = toList η₂
Tactic:
apply And.intro
State after:
case left
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
⊢ p.toFuncE (G₁.bar (Morphism.localSection p (lift η₁ p v₁ h).τ e.edge (_ : p.toFuncV w₁ = G₂.ι e.edge))) =
    G₂.bar e.edge

case right
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
⊢ List.map p.toFuncE (toList (lift η₂ p (lift η₁ p v₁ h).τ (_ : p.toFuncV (lift η₁ p v₁ h).τ = w₂)).path) = toList η₂

State before:
case left
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
⊢ p.toFuncE (G₁.bar (Morphism.localSection p (lift η₁ p v₁ h).τ e.edge (_ : p.toFuncV w₁ = G₂.ι e.edge))) =
    G₂.bar e.edge
Tactic:
rw [p.toFuncE_bar, p.toFuncE_localSection]
State after:
no goals

State before:
case right
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
⊢ List.map p.toFuncE (toList (lift η₂ p (lift η₁ p v₁ h).τ (_ : p.toFuncV (lift η₁ p v₁ h).τ = w₂)).path) = toList η₂
Tactic:
rw [θ₂.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₂ 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
⊢ lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h = liftCanc
Tactic:
apply unique_Pathlift
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₂ 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
⊢ lift (η₁ ++ η₂) p v₁ h = PathLift.append θ₁ θ₂
Tactic:
apply unique_Pathlift
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₂ 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 θ₁ θ₂
⊢ liftCanc.path = θ₁.path ++ cons e' (cons (EdgeBetween.bar e') θ₂.path)
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₂ 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)
⊢ [[liftCanc.path]] = [[(PathLift.append θ₁ θ₂).path]]
Tactic:
apply Quot.sound
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₂ 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)
⊢ Reduction liftCanc.path (PathLift.append θ₁ θ₂).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₂ 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)
⊢ Reduction liftCanc.path (PathLift.append θ₁ θ₂).path
Tactic:
rw [path1]
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₂ 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)
⊢ Reduction (θ₁.path ++ cons e' (cons (EdgeBetween.bar e') θ₂.path)) (PathLift.append θ₁ θ₂).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₂ 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)
⊢ Reduction (θ₁.path ++ cons e' (cons (EdgeBetween.bar e') θ₂.path)) (PathLift.append θ₁ θ₂).path
Tactic:
apply Reduction.step
State after:
no goals