∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (x x_1 : Rˣ),
  { val := star ↑(x * x_1), inv := star ↑(x * x_1)⁻¹, val_inv := ⋯, inv_val := ⋯ } =
    { val := star ↑x_1, inv := star ↑x_1⁻¹, val_inv := ⋯, inv_val := ⋯ } *
      { val := star ↑x, inv := star ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }