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 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 ]]⟩
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 θ₁ θ₂
⊢ { τ := θ₂.τ, pathClass := [[liftCanc.path]] } = { τ := θ₂.τ, pathClass := [[(PathLift.append θ₁ θ₂).path]] }
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 θ₁ θ₂
⊢ { τ := θ₂.τ, pathClass := [[liftCanc.path]] } = { τ := θ₂.τ, pathClass := [[(PathLift.append θ₁ θ₂).path]] }
Tactic:
have path1 : liftCanc.path =
  θ₁.path ++ (cons e' (cons e'.bar θ₂.path)) := by
    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 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]] }
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)
this : [[liftCanc.path]] = [[(PathLift.append θ₁ θ₂).path]]
⊢ { τ := θ₂.τ, pathClass := [[liftCanc.path]] } = { τ := θ₂.τ, pathClass := [[(PathLift.append θ₁ θ₂).path]] }
Tactic:
rw [this]
Proof state after:
no goals
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
⊢ p.toFuncV w₁ = G₂.ι e.edge
Tactic:
rw [hw, e.init_eq]
Proof state after:
no goals
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
⊢ 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]
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
⊢ 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 η₂
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
⊢ 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
Proof 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 η₂
Theorem: Graph.homotopy_step_lift
Proof 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]
Proof state after:
no goals
Theorem: Graph.homotopy_step_lift
Proof 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]
Proof state after:
no goals
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
⊢ lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h = liftCanc
Tactic:
apply unique_Pathlift
Proof state after:
no goals
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
⊢ lift (η₁ ++ η₂) p v₁ h = PathLift.append θ₁ θ₂
Tactic:
apply unique_Pathlift
Proof state after:
no goals
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 θ₁ θ₂
⊢ liftCanc.path = θ₁.path ++ cons e' (cons (EdgeBetween.bar e') θ₂.path)
Tactic:
rfl
Proof state after:
no goals
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)
⊢ [[liftCanc.path]] = [[(PathLift.append θ₁ θ₂).path]]
Tactic:
apply Quot.sound
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₂ 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