Lean4
/-- The action of the tensor product on maps coming from `SimplexCategory`. -/
def tensorHomOf {x₁ y₁ x₂ y₂ : SimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) : tensorObjOf x₁ x₂ ⟶ tensorObjOf y₁ y₂ :=
letI f₁ : Fin ((x₁.len + 1) + (x₂.len + 1)) →o Fin ((y₁.len + 1) + (y₂.len + 1)) :=
{ toFun
i :=
Fin.addCases (motive := fun _ ↦ Fin <| (y₁.len + 1) + (y₂.len + 1)) (fun i ↦ (f₁.toOrderHom i).castAdd _)
(fun i ↦ (f₂.toOrderHom i).natAdd _) i
monotone' i j
h :=
by
cases i using Fin.addCases <;> cases j using Fin.addCases <;> rw [Fin.le_def] at h ⊢ <;>
simp [Fin.coe_castAdd, Fin.coe_natAdd, Fin.addCases_left, Fin.addCases_right] at h ⊢
· case left.left i j => exact f₁.toOrderHom.monotone h
· case left.right i j => omega
· case right.left i j => omega
· case right.right i j => exact f₂.toOrderHom.monotone h }
(eqToHom (congrArg _ (Nat.succ_add _ _)).symm ≫ (SimplexCategory.mkHom f₁) ≫ eqToHom (congrArg _ (Nat.succ_add _ _)) :
_ ⟶ ⦋y₁.len + y₂.len + 1⦌)
