Theorem: Graph.UniversalCover.reduced_unique (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₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
⊢ [[p₁]] = [[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₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[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₁ : 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
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₂

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

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
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₁ : 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]
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₂).τ

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

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

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