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

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

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

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

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