-- Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
theorem HoRel₂.mk' {V : SSet.Truncated 2} (φ : V _⦋2⦌₂) {X₀ X₁ X₂ : OneTruncation₂ V}
    (f₀₁ : X₀ ⟶ X₁) (f₁₂ : X₁ ⟶ X₂) (f₀₂ : X₀ ⟶ X₂)
    (h₀₁ : f₀₁.edge = V.map (δ₂ 2).op φ) (h₁₂ : f₁₂.edge = V.map (δ₂ 0).op φ)
    (h₀₂ : f₀₂.edge = V.map (δ₂ 1).op φ) :
    HoRel₂ _ _ (Quot.mk _ (Quiver.Hom.toPath f₀₂))
      (Quot.mk _ ((Quiver.Hom.toPath f₀₁).comp (Quiver.Hom.toPath f₁₂)))

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
X₀ X₁ X₂ : OneTruncation₂ V
f₀₁ : X₀ ⟶ X₁
f₁₂ : X₁ ⟶ X₂
f₀₂ : X₀ ⟶ X₂
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
⊢ V.map (δ₂ 1 ⋯ ⋯ ≫ δ₂ 1 ⋯ ⋯).op φ = ev0₂ φ

Tactic:
rfl

Result:
no goals

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ ev2₂ φ
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
⊢ f₁₂ = ev12₂ φ

Tactic:
ext

Result:
case a
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ ev2₂ φ
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
⊢ f₁₂.edge = (ev12₂ φ).edge

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
X₁ X₂ : OneTruncation₂ V
f₁₂ : X₁ ⟶ X₂
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
f₀₁ : ev0₂ φ ⟶ X₁
f₀₂ : ev0₂ φ ⟶ X₂
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
⊢ X₁ = ev1₂ φ

Tactic:
rw [← f₀₁.tgt_eq, h₀₁, ← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
X₁ X₂ : OneTruncation₂ V
f₁₂ : X₁ ⟶ X₂
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
f₀₁ : ev0₂ φ ⟶ X₁
f₀₂ : ev0₂ φ ⟶ X₂
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
⊢ V.map (δ₂ 0 ⋯ ⋯ ≫ δ₂ 2 ⋯ ⋯).op φ = ev1₂ φ

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₁₂ : (ev12₂ φ).edge = V.map (δ₂ 0 ⋯ ⋯).op φ
h₀₂ : (ev02₂ φ).edge = V.map (δ₂ 1 ⋯ ⋯).op φ
⊢ HoRel₂ { as := ev0₂ φ } { as := ev2₂ φ } (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) (ev02₂ φ).toPath)
    (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) ((ev01₂ φ).toPath.comp (ev12₂ φ).toPath))

Tactic:
constructor

Result:
no goals

Proof state:
case a
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₁ : ev0₂ φ ⟶ ev1₂ φ
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ ev2₂ φ
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
⊢ f₀₁.edge = (ev01₂ φ).edge

Tactic:
assumption

Result:
no goals

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
X₂ : OneTruncation₂ V
f₀₂ : ev0₂ φ ⟶ X₂
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ X₂
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
f₀₁ : ev0₂ φ ⟶ ev1₂ φ
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
⊢ X₂ = ev2₂ φ

Tactic:
rw [← f₁₂.tgt_eq, h₁₂, ← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
X₂ : OneTruncation₂ V
f₀₂ : ev0₂ φ ⟶ X₂
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ X₂
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
f₀₁ : ev0₂ φ ⟶ ev1₂ φ
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
⊢ V.map (δ₂ 0 ⋯ ⋯ ≫ δ₂ 0 ⋯ ⋯).op φ = ev2₂ φ

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
X₂ : OneTruncation₂ V
f₀₂ : ev0₂ φ ⟶ X₂
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ X₂
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
f₀₁ : ev0₂ φ ⟶ ev1₂ φ
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
⊢ V.map (δ₂ 0 ⋯ ⋯ ≫ δ₂ 0 ⋯ ⋯).op φ = ev2₂ φ

Tactic:
rfl

Result:
no goals

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₁₂ : (ev12₂ φ).edge = V.map (δ₂ 0 ⋯ ⋯).op φ
⊢ HoRel₂ { as := ev0₂ φ } { as := ev2₂ φ } (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) f₀₂.toPath)
    (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) ((ev01₂ φ).toPath.comp (ev12₂ φ).toPath))

Tactic:
obtain rfl : f₀₂ = ev02₂ φ := by ext; assumption

Result:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₁₂ : (ev12₂ φ).edge = V.map (δ₂ 0 ⋯ ⋯).op φ
h₀₂ : (ev02₂ φ).edge = V.map (δ₂ 1 ⋯ ⋯).op φ
⊢ HoRel₂ { as := ev0₂ φ } { as := ev2₂ φ } (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) (ev02₂ φ).toPath)
    (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) ((ev01₂ φ).toPath.comp (ev12₂ φ).toPath))

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₁₂ : (ev12₂ φ).edge = V.map (δ₂ 0 ⋯ ⋯).op φ
⊢ f₀₂ = ev02₂ φ

Tactic:
ext

Result:
case a
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₁₂ : (ev12₂ φ).edge = V.map (δ₂ 0 ⋯ ⋯).op φ
⊢ f₀₂.edge = (ev02₂ φ).edge

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
X₂ : OneTruncation₂ V
f₀₂ : ev0₂ φ ⟶ X₂
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ X₂
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
f₀₁ : ev0₂ φ ⟶ ev1₂ φ
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
⊢ HoRel₂ { as := ev0₂ φ } { as := X₂ } (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) f₀₂.toPath)
    (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) (f₀₁.toPath.comp f₁₂.toPath))

Tactic:
obtain rfl : X₂ = ev2₂ φ := by
  rw [← f₁₂.tgt_eq, h₁₂, ← FunctorToTypes.map_comp_apply, ← op_comp]
  rfl

Result:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₁ : ev0₂ φ ⟶ ev1₂ φ
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ ev2₂ φ
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
⊢ HoRel₂ { as := ev0₂ φ } { as := ev2₂ φ } (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) f₀₂.toPath)
    (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) (f₀₁.toPath.comp f₁₂.toPath))

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ ev2₂ φ
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
⊢ HoRel₂ { as := ev0₂ φ } { as := ev2₂ φ } (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) f₀₂.toPath)
    (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) ((ev01₂ φ).toPath.comp f₁₂.toPath))

Tactic:
obtain rfl : f₁₂ = ev12₂ φ := by ext; assumption

Result:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
h₀₁ : (ev01₂ φ).edge = V.map (δ₂ 2 ⋯ ⋯).op φ
h₁₂ : (ev12₂ φ).edge = V.map (δ₂ 0 ⋯ ⋯).op φ
⊢ HoRel₂ { as := ev0₂ φ } { as := ev2₂ φ } (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) f₀₂.toPath)
    (Quot.mk (Quotient.CompClosure Cat.FreeReflRel) ((ev01₂ φ).toPath.comp (ev12₂ φ).toPath))

Proof state:
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₁ : ev0₂ φ ⟶ ev1₂ φ
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ ev2₂ φ
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
⊢ f₀₁ = ev01₂ φ

Tactic:
ext

Result:
case a
V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ⋯ })
f₀₁ : ev0₂ φ ⟶ ev1₂ φ
h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ
f₀₂ : ev0₂ φ ⟶ ev2₂ φ
h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ
f₁₂ : ev1₂ φ ⟶ ev2₂ φ
h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ
⊢ f₀₁.edge = (ev01₂ φ).edge