-- 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} }
pos :
  ∀
    (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
      { 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) }
      { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
        right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f' : Comma (inclusion n) (Functor.fromPUnit Δ) }
neg :
  ∀
    (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
      { 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) }
      { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
        right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f' : Comma (inclusion n) (Functor.fromPUnit Δ) }
⊢ Zigzag
    { 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) }
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
      right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f' : Comma (inclusion n) (Functor.fromPUnit Δ) }

Tactic:
by_cases hff' : f 0 ≤ f' 0

Premises used: CategoryTheory.ConcreteCategory.hom, OfNat.ofNat, DFunLike.coe