Lean4
instance nonAssocRing [NonAssocRing R] : NonAssocRing (ULift R) :=
{ zero := (0 : ULift R), one := (1 : ULift R), add := (· + ·), mul := (· * ·), sub := Sub.sub, neg := Neg.neg,
nsmul := AddMonoid.nsmul, natCast := fun n => ULift.up n, intCast := fun n => ULift.up n,
zsmul := SubNegMonoid.zsmul, intCast_ofNat := addGroupWithOne.intCast_ofNat, add_assoc, zero_add, add_zero,
neg_add_cancel, add_comm, left_distrib, right_distrib, zero_mul, mul_zero, one_mul, mul_one, sub_eq_add_neg,
nsmul_zero := fun _ => AddMonoid.nsmul_zero _, nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _,
zsmul_zero' := SubNegMonoid.zsmul_zero', zsmul_succ' := SubNegMonoid.zsmul_succ',
zsmul_neg' := SubNegMonoid.zsmul_neg', natCast_zero := AddMonoidWithOne.natCast_zero,
natCast_succ := AddMonoidWithOne.natCast_succ, intCast_negSucc := AddGroupWithOne.intCast_negSucc }
