Theorem: Graph.UniversalCover.homotopic_of_liftTerminal_eq (GroupComp/Graph/UniversalCover.lean)

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
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₂]]

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
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₂]]

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
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₂]]

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₁
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₂]]

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₂
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₂]]

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
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₂]]

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
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₂]]

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
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₂]]

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
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₂]]

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]
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₂

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals