Theorem: Graph.UniversalCover.simple_connectivity_for_paths (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
vert : Vert G x₀
e₁ e₂ : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ [[e₁]] = [[e₂]]
Tactic:
apply proj_injective (proj G x₀)
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₀)]]

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

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