-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Truncated (goal)
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
    { 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 Δ) }
have trans : Zigzag (J := Comma (inclusion n) (Functor.fromPUnit Δ))
  { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) ⦋0⦌ sorry,
    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) ⦋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)
        sorry }
Tactic: trans ⟨⦋1⦌ₙ, ⟨⟨⟩⟩, mkOfLe (n := Δ.len) (f' 0) (f 0) (le_of_not_ge hff')⟩