-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i j : Fin (x₁.len + 1 + (x₂.len + 1))
h : i ≤ j
left :
  ∀ (i : Fin (x₁.len + 1)) (h : Fin.castAdd (x₂.len + 1) i ≤ j),
    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.castAdd (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)
right :
  ∀ (i : Fin (x₂.len + 1)) (h : Fin.natAdd (x₁.len + 1) i ≤ j),
    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)
⊢ 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))))
      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 i using Fin.addCases