-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X : Truncated 2
C : Type u
inst : Category.{u, u} C
F G : X ⟶ obj (truncation 2) (nerve C)
h : map F = map G
f :
  X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌ ⋯))
obtain :
  ∀
    (x₀ x₁ :
      X.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Truncated.Edge._proof_1)))
    (f : Truncated.Edge x₀ x₁),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.app
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1)
                    ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })))
          f.edge :
        (fun (X : Type u) ↦ X)
          (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (G.app
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1)
                    ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })))
          f.edge :
        (fun (X : Type u) ↦ X)
          (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                ⋯))))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        f :
      (fun (X : Type u) ↦ X)
        (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (G.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        f :
      (fun (X : Type u) ↦ X)
        (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))

Tactic:
obtain ⟨x₀, x₁, f, rfl⟩ := Truncated.Edge.exists_of_simplex f

Premises used: SSet.Truncated.Edge.exists_of_simplex, rfl