Theorem: algebra.grlex_add_le_add
Proof state before:
case inl.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h✝³ : Order.lex (Variables.mul a c) (Variables.mul b c)
h✝² : Order.lex a b
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then True else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : ¬sum₁ < sum₂
h✝ : sum₁ = sum₂
⊢ True

case inl.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : Order.lex (Variables.mul a c) (Variables.mul b c)
h✝² : Order.lex a b
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then True else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : ¬sum₁ < sum₂
h✝ : ¬sum₁ = sum₂
⊢ False

case inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝¹ : Order.lex (Variables.mul a c) (Variables.mul b c)
h✝ : ¬Order.lex a b
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then False else False
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then True else False

case inr
n : ℕ
a b c : Variables n order.GrLex
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then if Order.lex a b then True else False else False
h✝ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then False else False
Tactic:
simp
Proof state after:
case inl.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : Order.lex (Variables.mul a c) (Variables.mul b c)
h✝² : Order.lex a b
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then True else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : ¬sum₁ < sum₂
h✝ : ¬sum₁ = sum₂
⊢ False

case inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝¹ : Order.lex (Variables.mul a c) (Variables.mul b c)
h✝ : ¬Order.lex a b
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then False else False
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then True else False

case inr
n : ℕ
a b c : Variables n order.GrLex
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then if Order.lex a b then True else False else False
h✝ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then False else False