∀ {G : Type u} [inst : Mul G] [inst_1 : Inv G] [inst_2 : One G] (assoc : ∀ (a b c : G), a * b * c = a * (b * c))
  (mul_one : ∀ (a : G), a * 1 = a) (mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1),
  Group.ofRightAxioms assoc mul_one mul_inv_cancel =
    { toMul := inst, mul_assoc := assoc, toOne := inst_2, one_mul := ⋯, mul_one := mul_one, npow := npowRecAuto,
      npow_zero := ⋯, npow_succ := ⋯, toInv := inst_1, div := DivInvMonoid.div', div_eq_mul_inv := ⋯, zpow := zpowRec,
      zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }