internlm/Lean-Github huggingface dataset:
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.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let θ₁ := η₁.lift p v₁ h
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let w₁ := θ₁.τ
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₁ := θ₁.τ
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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₁ := θ₁.τ
⊢ 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
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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
⊢ 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])
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)
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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)
⊢ 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⟩
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.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let θ₂ := η₂.lift p w₁ hw
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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) η₂))) }
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
let liftCanc :=
  θ₁.append liftTailCanc
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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
⊢ 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
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
rw [splitLift]
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
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
have splitLift' :
  (η₁ ++ η₂).lift p v₁ h =
    θ₁.append θ₂ := by
      apply unique_Pathlift
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 θ₁ θ₂
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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 θ₁ θ₂
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
Tactic:
rw [splitLift']
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 θ₁ θ₂
⊢ PathLift.pathClass liftCanc = PathLift.pathClass (PathLift.append θ₁ θ₂)