∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → RightCancelMonoid (f i)],
  Pi.rightCancelMonoid =
    { toSemigroup := Pi.rightCancelSemigroup.toSemigroup, toOne := Pi.monoid.toOne, one_mul := ⋯, mul_one := ⋯,
      npow := Monoid.npow, npow_zero := ⋯, npow_succ := ⋯, toIsRightCancelMul := ⋯ }