Theorem: polynomial.erase_reducer (Diploma/Polynomials/Division.lean)

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
⊢ divisible = p - reducer + (quotient + reducer) + remainder
Tactic:
have h: -reducer + (quotient + reducer) = (quotient + reducer) + -reducer := 
  add_comm (-reducer) (quotient + reducer)
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : -reducer + (quotient + reducer) = quotient + reducer + -reducer
⊢ divisible = p - reducer + (quotient + reducer) + remainder

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : -reducer + (quotient + reducer) = quotient + reducer + -reducer
⊢ divisible = p - reducer + (quotient + reducer) + remainder
Tactic:
rw [sub_eq_add_neg, ←add_assoc, add_comm, add_assoc,
    add_assoc, h, add_assoc, add_right_neg, add_zero, add_comm]
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : -reducer + (quotient + reducer) = quotient + reducer + -reducer
⊢ divisible = p + quotient + remainder

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : -reducer + (quotient + reducer) = quotient + reducer + -reducer
⊢ divisible = p + quotient + remainder
Tactic:
exact sum_eq
State after:
no goals