∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → LeftCancelMonoid (f i)],
  Pi.leftCancelMonoid =
    { toSemigroup := Pi.leftCancelSemigroup.toSemigroup, toOne := Pi.monoid.toOne, one_mul := ⋯, mul_one := ⋯,
      npow := Monoid.npow, npow_zero := ⋯, npow_succ := ⋯, toIsLeftCancelMul := ⋯ }