Theorem: Graph.cover_π₁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₁ : V₁
v₂ : V₂
hyp : p.toFuncV v₁ = v₂
⊢ Function.Injective ⇑(Morphism.π₁map v₁ v₂ p hyp)
Tactic:
cases hyp
State after:
case refl
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₁ : V₁
⊢ Function.Injective ⇑(Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁))

State before:
case refl
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₁ : V₁
⊢ Function.Injective ⇑(Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁))
Tactic:
apply Quot.ind
State after:
case refl.mk
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₁ : V₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁) ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction a = a₂

State before:
case refl.mk
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₁ : V₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁) ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction a = a₂
Tactic:
intro η₁
State after:
case refl.mk
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₁ : V₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction η₁ = a₂

State before:
case refl.mk
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₁ : V₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction η₁ = a₂
Tactic:
apply Quot.ind
State after:
case refl.mk.mk
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₁ : V₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁),
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) →
      Quot.mk Reduction η₁ = Quot.mk Reduction a

State before:
case refl.mk.mk
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₁ : V₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁),
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) →
      Quot.mk Reduction η₁ = Quot.mk Reduction a
Tactic:
intro η₂
State after:
case refl.mk.mk
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₁ : V₁
η₁ η₂ : EdgePath G₁ v₁ v₁
⊢ (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
      (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₂) →
    Quot.mk Reduction η₁ = Quot.mk Reduction η₂

State before:
case refl.mk.mk
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₁ : V₁
η₁ η₂ : EdgePath G₁ v₁ v₁
⊢ (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
      (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₂) →
    Quot.mk Reduction η₁ = Quot.mk Reduction η₂
Tactic:
simp [Morphism.π₁map]
State after:
case refl.mk.mk
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₁ : V₁
η₁ η₂ : EdgePath G₁ v₁ v₁
⊢ PathClass.map p (Quot.mk Reduction η₁) = PathClass.map p (Quot.mk Reduction η₂) →
    Quot.mk Reduction η₁ = Quot.mk Reduction η₂

State before:
case refl.mk.mk
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₁ : V₁
η₁ η₂ : EdgePath G₁ v₁ v₁
⊢ PathClass.map p (Quot.mk Reduction η₁) = PathClass.map p (Quot.mk Reduction η₂) →
    Quot.mk Reduction η₁ = Quot.mk Reduction η₂
Tactic:
apply proj_injective
State after:
no goals