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