u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ a₂ b₂ : R
⊢ a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ c₁ a₂ b₂ c₂ : R
x✝¹ : a₁ + b₁ = c₁
x✝ : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂
subst_vars
no goals
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ a₂ b₂ : R
⊢ a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
simp [add_assoc, add_left_comm]