-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
inst : NeZero n
this_1 : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₁ hΔ₁) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
hff' :
  LE.le (α :=
    (fun (X : SimplexCategory) ↦ Fin (X.len + 1))
      (Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₁, property := hΔ₁ })) →
          (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
      0)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f' :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₂, property := hΔ₂ })) →
          (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
      0)
⊢ Zigzag (J := Comma (inclusion n) (Functor.fromPUnit Δ))
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) ⦋1⦌ this_1,
      right := { as := PUnit.unit },
      hom :=
        mkOfLe
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₁, property := hΔ₁ })) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
            0)
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f' :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₂, property := hΔ₂ })) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
            0)
          hff' }
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) ⦋0⦌ ⋯,
      right := { as := PUnit.unit },
      hom :=
        ⦋0⦌.const (Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} })
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f' :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₂, property := hΔ₂ })) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
            0) }

Tactic:
apply Zigzag.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 1

Premises used: SimplexCategory.Truncated.Hom.tr, CategoryTheory.CostructuredArrow.homMk, SimplexCategory.const, SimplexCategory.mk, OfNat.ofNat, CategoryTheory.Zigzag.of_inv