-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i : Fin (x₂.len + 1)
h : Fin.natAdd (x₁.len + 1) i ≤ j
right :
  ∀ (i_1 : Fin (x₁.len + 1)) (h : Fin.natAdd (x₁.len + 1) i ≤ Fin.castAdd (x₂.len + 1) i_1),
    LE.le (α := Fin (y₁.len + 1 + (y₂.len + 1)))
      ((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
          (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
              (fun (i : Fin (x₁.len + 1)) ↦
                Fin.castAdd (y₂.len + 1)
                  ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
              (fun (i : Fin (x₂.len + 1)) ↦
                Fin.natAdd (y₁.len + 1)
                  ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
              i :
            Fin (y₁.len + 1 + (y₂.len + 1))))
        (Fin.natAdd (x₁.len + 1) i))
      ((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
          (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
              (fun (i : Fin (x₁.len + 1)) ↦
                Fin.castAdd (y₂.len + 1)
                  ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
              (fun (i : Fin (x₂.len + 1)) ↦
                Fin.natAdd (y₁.len + 1)
                  ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
              i :
            Fin (y₁.len + 1 + (y₂.len + 1))))
        (Fin.castAdd (x₂.len + 1) i_1))
right₁ :
  ∀ (i_1 : Fin (x₂.len + 1))
    (h : LE.le (α := Fin (x₁.len + 1 + (x₂.len + 1))) (Fin.natAdd (x₁.len + 1) i) (Fin.natAdd (x₁.len + 1) i_1)),
    LE.le (α := Fin (y₁.len + 1 + (y₂.len + 1)))
      ((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
          (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
              (fun (i : Fin (x₁.len + 1)) ↦
                Fin.castAdd (y₂.len + 1)
                  ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
              (fun (i : Fin (x₂.len + 1)) ↦
                Fin.natAdd (y₁.len + 1)
                  ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
              i :
            Fin (y₁.len + 1 + (y₂.len + 1))))
        (Fin.natAdd (x₁.len + 1) i))
      ((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
          (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
              (fun (i : Fin (x₁.len + 1)) ↦
                Fin.castAdd (y₂.len + 1)
                  ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
              (fun (i : Fin (x₂.len + 1)) ↦
                Fin.natAdd (y₁.len + 1)
                  ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
              i :
            Fin (y₁.len + 1 + (y₂.len + 1))))
        (Fin.natAdd (x₁.len + 1) i_1))
⊢ LE.le (α := Fin (y₁.len + 1 + (y₂.len + 1)))
    ((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
        (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
            (fun (i : Fin (x₁.len + 1)) ↦
              Fin.castAdd (y₂.len + 1)
                ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
            (fun (i : Fin (x₂.len + 1)) ↦
              Fin.natAdd (y₁.len + 1)
                ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.natAdd (x₁.len + 1) i))
    ((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
        (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
            (fun (i : Fin (x₁.len + 1)) ↦
              Fin.castAdd (y₂.len + 1)
                ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
            (fun (i : Fin (x₂.len + 1)) ↦
              Fin.natAdd (y₁.len + 1)
                ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      j)

Tactic:
cases j using Fin.addCases