α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)
α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'
simp [h₁.symm, h₂.symm, termg, add_zsmul]
no goals
α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)
exact add_add_add_comm (n₁ • x) a₁ (n₂ • x) a₂