u : Lean.Level
R✝ : Type ?u.213656
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂
u : Lean.Level
R✝ : Type ?u.213656
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ a₂ b₁ b₂ : R
x✝¹ : -a₁ = b₁
x✝ : -a₂ = b₂
⊢ -(a₁ + a₂) = b₁ + b₂
subst_vars
no goals
u : Lean.Level
R✝ : Type ?u.213656
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂
simp [add_comm]