[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
k : α
n : ℕ
x a a' : α
h : k + a = a'
⊢ k + term n x a = term n x a'
[PROOFSTEP]
simp [h.symm, term, add_comm, add_assoc]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
k : α
n : ℤ
x a a' : α
h : k + a = a'
⊢ k + termg n x a = termg n x a'
[PROOFSTEP]
simp [h.symm, termg, add_comm, add_assoc]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
x a k a' : α
h : a + k = a'
⊢ term n x a + k = term n x a'
[PROOFSTEP]
simp [h.symm, term, add_assoc]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a k a' : α
h : a + k = a'
⊢ termg n x a + k = termg n x a'
[PROOFSTEP]
simp [h.symm, termg, add_assoc]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
n₁ : ℕ
x a₁ : α
n₂ : ℕ
a₂ : α
n' : ℕ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ term n₁ x a₁ + term n₂ x a₂ = term n' x a'
[PROOFSTEP]
simp [h₁.symm, h₂.symm, term, add_nsmul, add_assoc, add_left_comm]
[GOAL]
α : 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'
[PROOFSTEP]
simp [h₁.symm, h₂.symm, termg, add_zsmul]
[GOAL]
α : 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₂)
[PROOFSTEP]
exact add_add_add_comm (n₁ • x) a₁ (n₂ • x) a₂
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
x a : α
⊢ term 0 x a = a
[PROOFSTEP]
simp [term, zero_nsmul, one_nsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
x a : α
⊢ termg 0 x a = a
[PROOFSTEP]
simp [termg, zero_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -termg n x a = termg n' x a'
[PROOFSTEP]
simp [h₂.symm, h₁.symm, termg]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -a + -(n • x) = -(n • x) + -a
[PROOFSTEP]
exact add_comm _ _
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
c : ℕ
⊢ smul c 0 = 0
[PROOFSTEP]
simp [smul, nsmul_zero]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
c : ℤ
⊢ smulg c 0 = 0
[PROOFSTEP]
simp [smulg, zsmul_zero]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
c n : ℕ
x a : α
n' : ℕ
a' : α
h₁ : c * n = n'
h₂ : smul c a = a'
⊢ smul c (term n x a) = term n' x a'
[PROOFSTEP]
simp [h₂.symm, h₁.symm, term, smul, nsmul_add, mul_nsmul']
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
c n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : c * n = n'
h₂ : smulg c a = a'
⊢ smulg c (termg n x a) = termg n' x a'
[PROOFSTEP]
simp [h₂.symm, h₁.symm, termg, smulg, zsmul_add, mul_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
x : α
⊢ x = term 1 x 0
[PROOFSTEP]
simp [term]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
x : α
⊢ x = termg 1 x 0
[PROOFSTEP]
simp [termg]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
x x' : α
h : x = x'
⊢ x = term 1 x' 0
[PROOFSTEP]
simp [term, h]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
x x' : α
h : x = x'
⊢ x = termg 1 x' 0
[PROOFSTEP]
simp [termg, h]
[GOAL]
α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ a - b = c
[PROOFSTEP]
rw [sub_eq_add_neg, h]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
l : ℕ
r : α
tl : ℕ
tr t : α
prl : l = tl
prr : r = tr
prt : smul tl tr = t
⊢ smul l r = t
[PROOFSTEP]
simp [prl, prr, prt]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
l : ℤ
r : α
tl : ℤ
tr t : α
prl : l = tl
prr : r = tr
prt : smulg tl tr = t
⊢ smulg l r = t
[PROOFSTEP]
simp [prl, prr, prt]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
l : ℕ
r : α
tl : ℕ
zl : ℤ
tr t : α
prl₁ : l = tl
prl₂ : ↑tl = zl
prr : r = tr
prt : smulg zl tr = t
⊢ smul l r = t
[PROOFSTEP]
simp [← prt, prl₁, ← prl₂, prr, smul, smulg, coe_nat_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t
[PROOFSTEP]
rw [prl, prr, prt]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t
[PROOFSTEP]
rw [prl, prr, prt]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
a ta t : α
pra : a = ta
prt : -ta = t
⊢ -a = t
[PROOFSTEP]
simp [pra, prt]
