internlm/Lean-Github huggingface dataset:
Theorem: Graph.homotopy_step_lift
Proof state before:
case a
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ 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]
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 (θ₁.path ++ cons e' (cons (EdgeBetween.bar e') θ₂.path)) (PathLift.append θ₁ θ₂).path
Theorem: Graph.homotopy_step_lift
Proof state before:
case a
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ 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
Proof state after:
no goals
Theorem: Graph.homotopyLift_of_path
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
⊢ homotopyLift p v₁ h [[e]] = PathLift.pathClass (lift e p v₁ h)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.liftClass_eq_of_homotopic
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ liftClass p v₁ v₂ w₂ h e₁ = liftClass p v₁ v₂ w₂ h e₂
Tactic:
simp [liftClass, ← homotopyLift_of_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₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ homotopyLift p v₁ h [[e₁]] = homotopyLift p v₁ h [[e₂]]
Theorem: Graph.liftClass_eq_of_homotopic
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ homotopyLift p v₁ h [[e₁]] = homotopyLift p v₁ h [[e₂]]
Tactic:
congr
Proof state after:
no goals
Theorem: Graph.liftTerminal_eq_of_homotopic
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ liftTerminal p v₁ h e₁ = liftTerminal p v₁ h e₂
Tactic:
simp [liftTerminal]
Proof state after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ (liftClass p v₁ v₂ w₂ h e₁).τ = (liftClass p v₁ v₂ w₂ h e₂).τ
Theorem: Graph.liftTerminal_eq_of_homotopic
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ (liftClass p v₁ v₂ w₂ h e₁).τ = (liftClass p v₁ v₂ w₂ h e₂).τ
Tactic:
rw [liftClass_eq_of_homotopic _ _ _ red]
Proof state after:
no goals
Theorem: Graph.lift_of_proj
Proof state before:
V : Type u
E : Type v
V₁ : Type ?u.140325
E₁ : Type ?u.140324
V₂ : Type ?u.140329
E₂ : Type ?u.140328
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e : EdgePath G₁ v₁ w₁
⊢ List.map p.toFuncE (toList e) = toList (EdgePath.map e p)
Tactic:
simp [map_toList]
Proof state after:
no goals
Theorem: Graph.lift_of_proj
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₁ w₁ : V₁
e : EdgePath G₁ v₁ w₁
⊢ lift (EdgePath.map e p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁) =
    { τ := w₁, path := e, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
      list_pushdown := (_ : List.map p.toFuncE (toList e) = toList (EdgePath.map e p)) }
Tactic:
apply unique_Pathlift
Proof state after:
no goals
Theorem: Graph.liftTerminal_of_proj
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₁ w₁ : V₁
e : EdgePath G₁ v₁ w₁
⊢ liftTerminal p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e p) = w₁
Tactic:
simp only [liftTerminal, liftClass, lift_of_proj]
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₁ w₁ : V₁
e : EdgePath G₁ v₁ w₁
⊢ (PathLift.pathClass
        { τ := w₁, path := e, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e) = toList (EdgePath.map e p)) }).τ =
    w₁
Theorem: Graph.liftTerminal_of_proj
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₁ w₁ : V₁
e : EdgePath G₁ v₁ w₁
⊢ (PathLift.pathClass
        { τ := w₁, path := e, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e) = toList (EdgePath.map e p)) }).τ =
    w₁
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.proj_injective
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
⊢ [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]] → [[e₁]] = [[e₂]]
Tactic:
intro hyp
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
⊢ [[e₁]] = [[e₂]]
Theorem: Graph.proj_injective
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
⊢ [[e₁]] = [[e₂]]
Tactic:
let lem :=
  liftClass_eq_of_homotopic p v₁ rfl hyp
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : liftClass p v₁ (p.toFuncV v₁) (p.toFuncV w₁) (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e₁ p) =
  liftClass p v₁ (p.toFuncV v₁) (p.toFuncV w₁) (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e₂ p) :=
  liftClass_eq_of_homotopic p v₁ rfl hyp
⊢ [[e₁]] = [[e₂]]
Theorem: Graph.proj_injective
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : liftClass p v₁ (p.toFuncV v₁) (p.toFuncV w₁) (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e₁ p) =
  liftClass p v₁ (p.toFuncV v₁) (p.toFuncV w₁) (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e₂ p) :=
  liftClass_eq_of_homotopic p v₁ rfl hyp
⊢ [[e₁]] = [[e₂]]
Tactic:
simp [liftClass, PathLift.pathClass] at lem
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  (lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq [[(lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]
Theorem: Graph.proj_injective
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  (lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq [[(lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]
Tactic:
rw [lift_of_proj] at lem
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]
Theorem: Graph.proj_injective
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]
Tactic:
rw [lift_of_proj] at lem
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      { τ := w₁, path := e₂, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₂) = toList (EdgePath.map e₂ p)) }.τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[{ τ := w₁, path := e₂, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₂) = toList (EdgePath.map e₂ p)) }.path]]
⊢ [[e₁]] = [[e₂]]
Theorem: Graph.proj_injective
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      { τ := w₁, path := e₂, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₂) = toList (EdgePath.map e₂ p)) }.τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[{ τ := w₁, path := e₂, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₂) = toList (EdgePath.map e₂ p)) }.path]]
⊢ [[e₁]] = [[e₂]]
Tactic:
simp at lem
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : [[e₁]] = [[e₂]]
⊢ [[e₁]] = [[e₂]]
Theorem: Graph.proj_injective
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : [[e₁]] = [[e₂]]
⊢ [[e₁]] = [[e₂]]
Tactic:
exact lem
Proof state after:
no goals
Theorem: Graph.cover_π₁injective
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₂ : V₂
hyp : p.toFuncV v₁ = v₂
⊢ Function.Injective ⇑(Morphism.π₁map v₁ v₂ p hyp)
Tactic:
cases hyp
Proof state after:
case refl
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst : CoveringMap p
v₁ : V₁
⊢ Function.Injective ⇑(Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁))
Theorem: Graph.cover_π₁injective
Proof state before:
case refl
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst : CoveringMap p
v₁ : V₁
⊢ Function.Injective ⇑(Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁))
Tactic:
apply Quot.ind
Proof state after:
case refl.mk
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₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁) ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction a = a₂
Theorem: Graph.cover_π₁injective
Proof state before:
case refl.mk
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₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁) ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction a = a₂
Tactic:
intro η₁
Proof state after:
case refl.mk
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₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction η₁ = a₂
Theorem: Graph.cover_π₁injective
Proof state before:
case refl.mk
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₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction η₁ = a₂
Tactic:
apply Quot.ind
Proof state after:
case refl.mk.mk
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₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁),
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) →
      Quot.mk Reduction η₁ = Quot.mk Reduction a
Theorem: Graph.cover_π₁injective
Proof state before:
case refl.mk.mk
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₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁),
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) →
      Quot.mk Reduction η₁ = Quot.mk Reduction a
Tactic:
intro η₂
Proof state after:
case refl.mk.mk
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₁
η₁ η₂ : EdgePath G₁ v₁ v₁
⊢ (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
      (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₂) →
    Quot.mk Reduction η₁ = Quot.mk Reduction η₂
Theorem: Graph.cover_π₁injective
Proof state before:
case refl.mk.mk
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₁
η₁ η₂ : EdgePath G₁ v₁ v₁
⊢ (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
      (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₂) →
    Quot.mk Reduction η₁ = Quot.mk Reduction η₂
Tactic:
simp [Morphism.π₁map]
Proof state after:
case refl.mk.mk
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₁
η₁ η₂ : EdgePath G₁ v₁ v₁
⊢ PathClass.map p (Quot.mk Reduction η₁) = PathClass.map p (Quot.mk Reduction η₂) →
    Quot.mk Reduction η₁ = Quot.mk Reduction η₂
Theorem: Graph.cover_π₁injective
Proof state before:
case refl.mk.mk
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₁
η₁ η₂ : EdgePath G₁ v₁ v₁
⊢ PathClass.map p (Quot.mk Reduction η₁) = PathClass.map p (Quot.mk Reduction η₂) →
    Quot.mk Reduction η₁ = Quot.mk Reduction η₂
Tactic:
apply proj_injective
Proof state after:
no goals
Theorem: sq2_pow_twice
Proof state before:
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Tactic:
have two_nonneg : (2 : ℝ) ≥ 0 := by norm_cast
Proof state after:
two_nonneg : 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Tactic:
have sq2_pos : (Real.sqrt 2) > 0 := by simp [Real.sqrt_pos]
Proof state after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Tactic:
have sq2_nonneg : (Real.sqrt 2) ≥ 0 := by
  apply Real.sqrt_nonneg
Proof state after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Tactic:
rw [← Real.rpow_mul sq2_nonneg, Real.mul_self_sqrt two_nonneg]
Proof state after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ Real.sqrt 2 ^ 2 = 2