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