internlm/Lean-Github huggingface dataset:
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₂]]
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₂]]
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₁
_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₂]]
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₂]]
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₁
_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₂]]
Tactic:
rw [←l₁, ←_l₂] at 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₀)) (reduction p₁) =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (reduction 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₁
_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₂]]
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₀)) (reduction p₁) =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (reduction 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₁
_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₂]]
Tactic:
rw [reduced_liftTerminal (reduction p₁) (reduction_reduced p₁)] at 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 :
  { τ := τ, p := reduction p₁, is_reduced := (_ : reduced (reduction p₁)) } =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (reduction 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₁
_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₂]]
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 :
  { τ := τ, p := reduction p₁, is_reduced := (_ : reduced (reduction p₁)) } =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (reduction 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₁
_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₂]]
Tactic:
rw [reduced_liftTerminal (reduction p₂) (reduction_reduced p₂)] at 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 :
  { τ := τ, p := reduction p₁, is_reduced := (_ : reduced (reduction p₁)) } =
    { τ := τ, p := reduction p₂, is_reduced := (_ : reduced (reduction 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₁
_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₂]]
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 :
  { τ := τ, p := reduction p₁, is_reduced := (_ : reduced (reduction p₁)) } =
    { τ := τ, p := reduction p₂, is_reduced := (_ : reduced (reduction 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₁
_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₂]]
Tactic:
simp at 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₀ τ
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₁
_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₂
hyp : reduction p₁ = reduction 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₀ τ
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₁
_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₂
hyp : reduction p₁ = reduction p₂
⊢ [[p₁]] = [[p₂]]
Tactic:
rw [homotopic_iff_reduction_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₁ p₂ : EdgePath G x₀ τ
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₁
_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₂
hyp : reduction p₁ = reduction p₂
⊢ reduction p₁ = reduction 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₀ τ
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₁
_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₂
hyp : reduction p₁ = reduction p₂
⊢ reduction p₁ = reduction p₂
Tactic:
exact 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₀ τ
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₂
⊢ [[reduction p₁]] = [[p₁]]
Tactic:
apply reduction_homotopic_self
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₀ τ
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₁]]
⊢ [[reduction p₂]] = [[p₂]]
Tactic:
apply reduction_homotopic_self
Proof state after:
no goals
Theorem: Graph.UniversalCover.proj_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
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e (proj G x₀)) =
    vert
Tactic:
simp [liftTerminal, liftClass]
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
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ (PathLift.pathClass
        (lift (EdgePath.map e (proj G x₀)) (proj G x₀) (basepoint G x₀)
          (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)))).τ =
    vert
Theorem: Graph.UniversalCover.proj_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
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ (PathLift.pathClass
        (lift (EdgePath.map e (proj G x₀)) (proj G x₀) (basepoint G x₀)
          (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)))).τ =
    vert
Tactic:
simp [lift_of_proj]
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
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ (PathLift.pathClass
        { τ := vert, path := e, term_pushdown := (_ : (proj G x₀).toFuncV vert = (proj G x₀).toFuncV vert),
          list_pushdown :=
            (_ : List.map (proj G x₀).toFuncE (EdgePath.toList e) = EdgePath.toList (EdgePath.map e (proj G x₀))) }).τ =
    vert
Theorem: Graph.UniversalCover.proj_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
vert : Vert G x₀
e : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ (PathLift.pathClass
        { τ := vert, path := e, term_pushdown := (_ : (proj G x₀).toFuncV vert = (proj G x₀).toFuncV vert),
          list_pushdown :=
            (_ : List.map (proj G x₀).toFuncE (EdgePath.toList e) = EdgePath.toList (EdgePath.map e (proj G x₀))) }).τ =
    vert
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.UniversalCover.simple_connectivity_for_paths
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
vert : Vert G x₀
e₁ e₂ : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ [[e₁]] = [[e₂]]
Tactic:
apply proj_injective (proj G x₀)
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₀ : V
vert : Vert G x₀
e₁ e₂ : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ [[EdgePath.map e₁ (proj G x₀)]] = [[EdgePath.map e₂ (proj G x₀)]]
Theorem: Graph.UniversalCover.simple_connectivity_for_paths
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₀ : V
vert : Vert G x₀
e₁ e₂ : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ [[EdgePath.map e₁ (proj G x₀)]] = [[EdgePath.map e₂ (proj G x₀)]]
Tactic:
let lem :
  liftTerminal (proj G x₀) (basepoint G x₀) rfl
    (e₁.map (proj G x₀)) =
  liftTerminal (proj G x₀) (basepoint G x₀) rfl
    (e₂.map (proj G x₀)) := by
  rw [proj_liftTerminal e₁, proj_liftTerminal e₂]
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₀ : V
vert : Vert G x₀
e₁ e₂ : EdgePath (univ G x₀) (basepoint G x₀) vert
lem : liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e₁ (proj G x₀)) =
  liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e₂ (proj G x₀)) :=
  Eq.mpr
    (id
      (congrArg (fun _a => _a = liftTerminal (proj G x₀) (basepoint G x₀) rfl (EdgePath.map e₂ (proj G x₀)))
        (proj_liftTerminal e₁)))
    (Eq.mpr (id (congrArg (fun _a => vert = _a) (proj_liftTerminal e₂))) (Eq.refl vert))
⊢ [[EdgePath.map e₁ (proj G x₀)]] = [[EdgePath.map e₂ (proj G x₀)]]
Theorem: Graph.UniversalCover.simple_connectivity_for_paths
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₀ : V
vert : Vert G x₀
e₁ e₂ : EdgePath (univ G x₀) (basepoint G x₀) vert
lem : liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e₁ (proj G x₀)) =
  liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e₂ (proj G x₀)) :=
  Eq.mpr
    (id
      (congrArg (fun _a => _a = liftTerminal (proj G x₀) (basepoint G x₀) rfl (EdgePath.map e₂ (proj G x₀)))
        (proj_liftTerminal e₁)))
    (Eq.mpr (id (congrArg (fun _a => vert = _a) (proj_liftTerminal e₂))) (Eq.refl vert))
⊢ [[EdgePath.map e₁ (proj G x₀)]] = [[EdgePath.map e₂ (proj G x₀)]]
Tactic:
apply homotopic_of_liftTerminal_eq lem
Proof state after:
no goals
Theorem: Graph.UniversalCover.simple_connectivity_for_paths
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
vert : Vert G x₀
e₁ e₂ : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e₁ (proj G x₀)) =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e₂ (proj G x₀))
Tactic:
rw [proj_liftTerminal e₁, proj_liftTerminal e₂]
Proof state after:
no goals
Theorem: Graph.τ_bar
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : E
⊢ τ G (G.bar e) = G.ι e
Tactic:
aesop (add norm unfold [τ])
Proof state after:
no goals
Theorem: Graph.EdgeBetween.bar_bar
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ bar (bar e) = e
Tactic:
ext
Proof state after:
case edge
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ (bar (bar e)).edge = e.edge
Theorem: Graph.EdgeBetween.bar_bar
Proof state before:
case edge
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ (bar (bar e)).edge = e.edge
Tactic:
aesop (add norm simp [EdgeBetween.bar])
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_cons
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w u u' : V
e : EdgeBetween G v w
p : EdgePath G w u
e' : EdgeBetween G u u'
⊢ concat (cons e p) e' = cons e (concat p e')
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_nil
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v✝ w : V
e : EdgeBetween G v✝ w
v : V
⊢ reverse (nil v) = nil v
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_cons
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w u : V
e : EdgeBetween G v w
p : EdgePath G w u
⊢ reverse (cons e p) = concat (reverse p) (EdgeBetween.bar e)
Tactic:
rfl
Proof state after:
no goals