internlm/Lean-Github huggingface dataset:
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ reduced (reverse p')
Tactic:
apply reverse_reduced
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ reduced p'
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ reduced p'
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.UniversalCover.rayTo_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayTo G x₀ τ p hyp)) = EdgePath.toList p
Tactic:
simp [rayTo, toList_shiftTarget, rayToRev_proj_list,
  reverse_toList, List.map_reverse]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList p
Theorem: Graph.UniversalCover.rayTo_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList p
Tactic:
have : G.bar ∘ G.bar = id := by
  funext x
  simp only [Function.comp, bar_bar, id_eq]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
this : G.bar ∘ G.bar = id
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList p
Theorem: Graph.UniversalCover.rayTo_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
this : G.bar ∘ G.bar = id
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList p
Tactic:
simp [this]
Proof state after:
no goals
Theorem: Graph.UniversalCover.rayTo_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ G.bar ∘ G.bar = id
Tactic:
funext x
Proof state after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
x : E
⊢ (G.bar ∘ G.bar) x = id x
Theorem: Graph.UniversalCover.rayTo_proj_list
Proof state before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
x : E
⊢ (G.bar ∘ G.bar) x = id x
Tactic:
simp only [Function.comp, bar_bar, id_eq]
Proof state after:
no goals
Theorem: Graph.UniversalCover.lift_of_reduced
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ lift p (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) =
    rayLift G x₀ τ p hyp
Tactic:
apply unique_Pathlift
Proof state after:
no goals
Theorem: Graph.UniversalCover.reduced_liftTerminal
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p =
    { τ := τ, p := p, is_reduced := hyp }
Tactic:
simp [liftTerminal, liftClass, lift_of_reduced p hyp, rayLift]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ (PathLift.pathClass
        { τ := { τ := τ, p := p, is_reduced := hyp }, path := rayTo G x₀ τ p hyp,
          term_pushdown :=
            (_ :
              (proj G x₀).toFuncV { τ := τ, p := p, is_reduced := hyp } =
                (proj G x₀).toFuncV { τ := τ, p := p, is_reduced := hyp }),
          list_pushdown :=
            (_ : List.map (proj G x₀).toFuncE (EdgePath.toList (rayTo G x₀ τ p hyp)) = EdgePath.toList p) }).τ =
    { τ := τ, p := p, is_reduced := hyp }
Theorem: Graph.UniversalCover.reduced_liftTerminal
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ (PathLift.pathClass
        { τ := { τ := τ, p := p, is_reduced := hyp }, path := rayTo G x₀ τ p hyp,
          term_pushdown :=
            (_ :
              (proj G x₀).toFuncV { τ := τ, p := p, is_reduced := hyp } =
                (proj G x₀).toFuncV { τ := τ, p := p, is_reduced := hyp }),
          list_pushdown :=
            (_ : List.map (proj G x₀).toFuncE (EdgePath.toList (rayTo G x₀ τ p hyp)) = EdgePath.toList p) }).τ =
    { τ := τ, p := p, is_reduced := hyp }
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.UniversalCover.reduced_unique
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
⊢ [[p₁]] = [[p₂]] → p₁ = p₂
Tactic:
intro hyp
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ p₁ = p₂
Theorem: Graph.UniversalCover.reduced_unique
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ p₁ = p₂
Tactic:
have leq :
  liftTerminal (proj G x₀) (basepoint G x₀) rfl p₁ =
  liftTerminal (proj G x₀) (basepoint G x₀) rfl p₂ := by
  simp [liftTerminal]
  apply congrArg
  apply liftClass_eq_of_homotopic
  assumption
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
leq :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
⊢ p₁ = p₂
Theorem: Graph.UniversalCover.reduced_unique
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
leq :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
⊢ p₁ = p₂
Tactic:
simp [reduced_liftTerminal p₁ hyp₁, reduced_liftTerminal p₂ hyp₂] at leq
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
leq : p₁ = p₂
⊢ p₁ = p₂
Theorem: Graph.UniversalCover.reduced_unique
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
leq : p₁ = p₂
⊢ p₁ = p₂
Tactic:
exact leq
Proof state after:
no goals
Theorem: Graph.UniversalCover.reduced_unique
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
Tactic:
simp [liftTerminal]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ (liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
        (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁).τ =
    (liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
        (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂).τ
Theorem: Graph.UniversalCover.reduced_unique
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ (liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
        (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁).τ =
    (liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
        (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂).τ
Tactic:
apply congrArg
Proof state after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
Theorem: Graph.UniversalCover.reduced_unique
Proof state before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
Tactic:
apply liftClass_eq_of_homotopic
Proof state after:
case h.red
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ [[p₁]] = [[p₂]]
Theorem: Graph.UniversalCover.reduced_unique
Proof state before:
case h.red
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ [[p₁]] = [[p₂]]
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ [[p₁]] = [[p₂]] ↔ reduction p₁ = reduction p₂
Tactic:
apply Iff.intro
Proof state after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ [[p₁]] = [[p₂]] → reduction p₁ = reduction p₂

case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ reduction p₁ = reduction p₂ → [[p₁]] = [[p₂]]
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ [[p₁]] = [[p₂]] → reduction p₁ = reduction p₂
Tactic:
intro eql
Proof state after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[p₁]] = [[p₂]]
⊢ reduction p₁ = reduction p₂
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[p₁]] = [[p₂]]
⊢ reduction p₁ = reduction p₂
Tactic:
rw [← reduction_homotopic_self p₁, ← reduction_homotopic_self p₂] at eql
Proof state after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
⊢ reduction p₁ = reduction p₂
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
⊢ reduction p₁ = reduction p₂
Tactic:
have red₁ : reduced (reduction p₁) := by
  apply reduction_reduced
Proof state after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
⊢ reduction p₁ = reduction p₂
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
⊢ reduction p₁ = reduction p₂
Tactic:
have red₂ : reduced (reduction p₂) := by
  apply reduction_reduced
Proof state after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
red₂ : reduced (reduction p₂)
⊢ reduction p₁ = reduction p₂
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
red₂ : reduced (reduction p₂)
⊢ reduction p₁ = reduction p₂
Tactic:
exact reduced_unique x₀ τ red₁ red₂ eql
Proof state after:
no goals
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
⊢ reduced (reduction p₁)
Tactic:
apply reduction_reduced
Proof state after:
no goals
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
⊢ reduced (reduction p₂)
Tactic:
apply reduction_reduced
Proof state after:
no goals
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ reduction p₁ = reduction p₂ → [[p₁]] = [[p₂]]
Tactic:
intro hyp
Proof state after:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp : reduction p₁ = reduction p₂
⊢ [[p₁]] = [[p₂]]
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp : reduction p₁ = reduction p₂
⊢ [[p₁]] = [[p₂]]
Tactic:
rw [← reduction_homotopic_self p₁, ← reduction_homotopic_self p₂]
Proof state after:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp : reduction p₁ = reduction p₂
⊢ [[reduction p₁]] = [[reduction p₂]]
Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq
Proof state before:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp : reduction p₁ = reduction p₂
⊢ [[reduction p₁]] = [[reduction p₂]]
Tactic:
rw [hyp]
Proof state after:
no goals
Theorem: Graph.UniversalCover.homotopic_of_liftTerminal_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
        (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
      liftTerminal (proj G x₀) (basepoint G x₀)
        (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂ →
    [[p₁]] = [[p₂]]
Tactic:
intro hyp
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
⊢ [[p₁]] = [[p₂]]
Theorem: Graph.UniversalCover.homotopic_of_liftTerminal_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
⊢ [[p₁]] = [[p₂]]
Tactic:
have red₁ :  [[ reduction p₁ ]] = [[ p₁ ]] := by
  apply reduction_homotopic_self
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
red₁ : [[reduction p₁]] = [[p₁]]
⊢ [[p₁]] = [[p₂]]
Theorem: Graph.UniversalCover.homotopic_of_liftTerminal_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
red₁ : [[reduction p₁]] = [[p₁]]
⊢ [[p₁]] = [[p₂]]
Tactic:
have red₂ :  [[ reduction p₂ ]] = [[ p₂ ]] := by
  apply reduction_homotopic_self
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
red₁ : [[reduction p₁]] = [[p₁]]
red₂ : [[reduction p₂]] = [[p₂]]
⊢ [[p₁]] = [[p₂]]
Theorem: Graph.UniversalCover.homotopic_of_liftTerminal_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
red₁ : [[reduction p₁]] = [[p₁]]
red₂ : [[reduction p₂]] = [[p₂]]
⊢ [[p₁]] = [[p₂]]
Tactic:
let l₁ :=
  liftTerminal_eq_of_homotopic (proj G x₀) (basepoint G x₀)  rfl red₁
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp :
  liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
red₁ : [[reduction p₁]] = [[p₁]]
red₂ : [[reduction p₂]] = [[p₂]]
l₁ : liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (reduction p₁) =
  liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ :=
  liftTerminal_eq_of_homotopic (proj G x₀) (basepoint G x₀) rfl red₁
⊢ [[p₁]] = [[p₂]]