u : Lean.Level
R✝ : Type ?u.203351
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a : R
⊢ -a = Int.rawCast (Int.negOfNat 1) * a
u : Lean.Level
R✝ : Type ?u.203351
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b : R
x✝ : Int.rawCast (Int.negOfNat 1) * a = b
⊢ -a = b
subst_vars
no goals
u : Lean.Level
R✝ : Type ?u.203351
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a : R
⊢ -a = Int.rawCast (Int.negOfNat 1) * a
simp [Int.negOfNat]