∀ (G : Type u) [inst : Group G] (x : ℕ),
  Action.diagonalSuccIsoTensorTrivial G x =
    match x with
    | 0 =>
      Action.diagonalOneIsoLeftRegular G ≪≫
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Action.leftRegular G)).symm ≪≫
          CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
            (Action.tensorUnitIso (Equiv.ofUnique PUnit.{u + 1} (Fin 0 → G)).toIso)
    | n.succ =>
      Action.diagonalSuccIsoTensorDiagonal G (n + 1) ≪≫
        CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
            (Action.diagonalSuccIsoTensorTrivial G n) ≪≫
          Action.leftRegularTensorIso G
              (CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) (Action.trivial G (Fin n → G))) ≪≫
            CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
              (Action.mkIso (Fin.insertNthEquiv (fun x => G) 0).toIso ⋯)