Theorem: Graph.proj_injective (GroupComp/Graph/Covering.lean)

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
⊢ [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]] → [[e₁]] = [[e₂]]
Tactic:
intro hyp
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
⊢ [[e₁]] = [[e₂]]

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
⊢ [[e₁]] = [[e₂]]
Tactic:
let lem :=
  liftClass_eq_of_homotopic p v₁ rfl hyp
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : liftClass p v₁ (p.toFuncV v₁) (p.toFuncV w₁) (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e₁ p) =
  liftClass p v₁ (p.toFuncV v₁) (p.toFuncV w₁) (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e₂ p) :=
  liftClass_eq_of_homotopic p v₁ rfl hyp
⊢ [[e₁]] = [[e₂]]

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : liftClass p v₁ (p.toFuncV v₁) (p.toFuncV w₁) (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e₁ p) =
  liftClass p v₁ (p.toFuncV v₁) (p.toFuncV w₁) (_ : p.toFuncV v₁ = p.toFuncV v₁) (EdgePath.map e₂ p) :=
  liftClass_eq_of_homotopic p v₁ rfl hyp
⊢ [[e₁]] = [[e₂]]
Tactic:
simp [liftClass, PathLift.pathClass] at lem
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  (lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq [[(lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  (lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq [[(lift (EdgePath.map e₁ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]
Tactic:
rw [lift_of_proj] at lem
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      (lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[(lift (EdgePath.map e₂ p) p v₁ (_ : p.toFuncV v₁ = p.toFuncV v₁)).path]]
⊢ [[e₁]] = [[e₂]]
Tactic:
rw [lift_of_proj] at lem
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      { τ := w₁, path := e₂, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₂) = toList (EdgePath.map e₂ p)) }.τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[{ τ := w₁, path := e₂, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₂) = toList (EdgePath.map e₂ p)) }.path]]
⊢ [[e₁]] = [[e₂]]

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem :
  { τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.τ =
      { τ := w₁, path := e₂, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
          list_pushdown := (_ : List.map p.toFuncE (toList e₂) = toList (EdgePath.map e₂ p)) }.τ ∧
    HEq
      [[{ τ := w₁, path := e₁, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₁) = toList (EdgePath.map e₁ p)) }.path]]
      [[{ τ := w₁, path := e₂, term_pushdown := (_ : p.toFuncV w₁ = p.toFuncV w₁),
            list_pushdown := (_ : List.map p.toFuncE (toList e₂) = toList (EdgePath.map e₂ p)) }.path]]
⊢ [[e₁]] = [[e₂]]
Tactic:
simp at lem
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : [[e₁]] = [[e₂]]
⊢ [[e₁]] = [[e₂]]

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : [[e₁]] = [[e₂]]
⊢ [[e₁]] = [[e₂]]
Tactic:
exact lem
State after:
no goals