Theorem: algebra.grlex_add_le_add (Diploma/Order/MonomialOrder.lean)

State before:
n : ℕ
⊢ ∀ (a b c : Variables n order.GrLex), Order.grlex a b → Order.grlex (Variables.mul a c) (Variables.mul b c)
Tactic:
intros a b c h_le
State after:
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ Order.grlex (Variables.mul a c) (Variables.mul b c)

State before:
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ Order.grlex (Variables.mul a c) (Variables.mul b c)
Tactic:
rw [Order.grlex]
State after:
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ 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 if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False

State before:
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ 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 if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False
Tactic:
rw [Order.grlex] at h_le
State after:
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
⊢ 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 if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False

State before:
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
⊢ 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 if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False
Tactic:
split
State after:
case inl
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 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

State before:
case inl
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 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:
split at h_le
State after:
case inl.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
⊢ 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 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

State before:
case inl.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
⊢ 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 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:
intros sum₁ sum₂
State after:
case inl.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)
⊢ if sum₁ < sum₂ then True else if sum₁ = sum₂ then True else 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

State before:
case inl.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)
⊢ if sum₁ < sum₂ then True else if sum₁ = sum₂ then True else 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:
repeat (split; simp)
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

State before:
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 at *
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 :
  if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
⊢ 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

State before:
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 :
  if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
⊢ 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:
split at h_le
State after:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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

State before:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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:
rename_i h₁ h₂ h₃
State after:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h₂ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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

State before:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h₂ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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 [elem_sum_is_hom] at *
State after:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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

State before:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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:
have h₄ := Nat.le_of_lt h₃
State after:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₄ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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

State before:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₄ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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:
have h₅ := Eq.symm (Nat.le_antisymm h₂ h₄)
State after:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₄ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
h₅ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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

State before:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₄ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
h₅ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False

case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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:
contradiction
State after:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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

State before:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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:
rename_i h₁ h₂ h₃
State after:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h₂ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h₃ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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

State before:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum (Variables.mul a c) = Order.grlex.elem_sum (Variables.mul b c)
h₂ : Order.grlex.elem_sum (Variables.mul b c) ≤ Order.grlex.elem_sum (Variables.mul a c)
h₃ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
⊢ 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 [elem_sum_is_hom] at *
State after:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₃ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
⊢ 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

State before:
case inl.inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h_le : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₃ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
⊢ 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:
split at h_le
State after:
case inl.inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₃ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₃ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h_le : False
⊢ 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

State before:
case inl.inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₃ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₃ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h_le : False
⊢ 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:
contradiction
State after:
case inl.inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₃ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h_le : False
⊢ 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

State before:
case inl.inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₃ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h_le : False
⊢ 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:
exact h_le
State after:
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

State before:
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:
intros sum₁ sum₂
State after:
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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
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

State before:
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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
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:
repeat (split; simp)
State after:
case inl.inr.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 False 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 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

State before:
case inl.inr.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 False 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 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 [elem_sum_is_hom] at *
State after:
case inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h_le : if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True else False
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ 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

State before:
case inl.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h_le : if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True else False
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ 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:
split at h_le
State after:
case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ 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

State before:
case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ 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:
rename_i h₁ h₂ h₃
State after:
case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ 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

State before:
case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ 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:
exact Nat.le_lt_antisymm h₁ h₃
State after:
case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ 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

State before:
case inl.inr.inr.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
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ 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:
exact h_le
State after:
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

State before:
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:
intros sum₁ sum₂
State after:
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)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
⊢ if sum₁ < sum₂ then True else if sum₁ = sum₂ then False else False

State before:
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)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
⊢ if sum₁ < sum₂ then True else if sum₁ = sum₂ then False else False
Tactic:
split
State after:
case inr.inl
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)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : sum₁ < sum₂
⊢ True

case inr.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)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : ¬sum₁ < sum₂
⊢ if sum₁ = sum₂ then False else False

State before:
case inr.inl
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)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : sum₁ < sum₂
⊢ True

case inr.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)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : ¬sum₁ < sum₂
⊢ if sum₁ = sum₂ then False else False
Tactic:
simp
State after:
case inr.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)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : ¬sum₁ < sum₂
⊢ if sum₁ = sum₂ then False else False

State before:
case inr.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)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : ¬sum₁ < sum₂
⊢ if sum₁ = sum₂ then False else False
Tactic:
split
State after:
case inr.inr.inl
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)
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 inr.inr.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)
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

State before:
case inr.inr.inl
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)
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 inr.inr.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)
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
Tactic:
simp [elem_sum_is_hom] at *
State after:
case inr.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h_le :
  if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
h✝² : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False

case inr.inr.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)
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

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

case inr.inr.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)
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
Tactic:
split at h_le
State after:
case inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

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

case inr.inr.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)
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

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

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

case inr.inr.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)
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
Tactic:
rename_i h₁ h₂ h₃
State after:
case inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

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

case inr.inr.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)
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

State before:
case inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

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

case inr.inr.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)
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
Tactic:
exact Nat.le_lt_antisymm h₁ h₃
State after:
case inr.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : if Order.lex a b then True else False
⊢ False

case inr.inr.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)
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

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

case inr.inr.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)
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
Tactic:
simp at *
State after:
case inr.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h_le : if Order.lex a b then True else False
h✝ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
⊢ False

case inr.inr.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)
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

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

case inr.inr.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)
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
Tactic:
split at h_le
State after:
case inr.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.lex a b
h_le : True
⊢ False

case inr.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.lex a b
h_le : False
⊢ False

case inr.inr.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)
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

State before:
case inr.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.lex a b
h_le : True
⊢ False

case inr.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.lex a b
h_le : False
⊢ False

case inr.inr.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)
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
Tactic:
rename_i h_lex₁ _ _ _ h_lex₂
State after:
case inr.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h_lex₁ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h_lex₂ : Order.lex a b
h_le : True
⊢ False

case inr.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.lex a b
h_le : False
⊢ False

case inr.inr.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)
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

State before:
case inr.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h_lex₁ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h_lex₂ : Order.lex a b
h_le : True
⊢ False

case inr.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.lex a b
h_le : False
⊢ False

case inr.inr.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)
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
Tactic:
have hr := lex_add_le_add a b c h_lex₂
State after:
case inr.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h_lex₁ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h_lex₂ : Order.lex a b
h_le : True
hr : Order.lex (Variables.mul a c) (Variables.mul b c)
⊢ False

case inr.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.lex a b
h_le : False
⊢ False

case inr.inr.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)
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

State before:
case inr.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h_lex₁ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h_lex₂ : Order.lex a b
h_le : True
hr : Order.lex (Variables.mul a c) (Variables.mul b c)
⊢ False

case inr.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.lex a b
h_le : False
⊢ False

case inr.inr.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)
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
Tactic:
contradiction
State after:
case inr.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.lex a b
h_le : False
⊢ False

case inr.inr.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)
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

State before:
case inr.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝³ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.lex a b
h_le : False
⊢ False

case inr.inr.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)
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
Tactic:
exact h_le
State after:
case inr.inr.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)
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

State before:
case inr.inr.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)
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
Tactic:
simp [elem_sum_is_hom] at *
State after:
case inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h_le :
  if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
h✝² : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False

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

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

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ False
Tactic:
rename_i h₁ h₂ h₃
State after:
case inr.inr.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h✝ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

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

State before:
case inr.inr.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h✝ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : True
⊢ False

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ False
Tactic:
exact Nat.le_lt_antisymm h₁ h₃
State after:
case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ False

State before:
case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.lex (Variables.mul a c) (Variables.mul b c)
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝² : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h_le : False
⊢ False
Tactic:
exact h_le
State after:
no goals

State before:
case inl.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 True else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : ¬sum₁ < sum₂
⊢ if sum₁ = sum₂ then True else 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:
(split; simp)
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

State before:
case inl.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 True else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : ¬sum₁ < sum₂
⊢ if sum₁ = sum₂ then True else 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:
split
State after:
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

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
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

State before:
case 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 False else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : ¬sum₁ < sum₂
⊢ 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:
(split; simp)
State after:
case inl.inr.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 False 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 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

State before:
case 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 False else False
sum₁ : ℕ := Order.grlex.elem_sum (Variables.mul a c)
sum₂ : ℕ := Order.grlex.elem_sum (Variables.mul b c)
h✝ : ¬sum₁ < sum₂
⊢ 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:
split
State after:
case inl.inr.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 False 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.inr.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 False 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 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

State before:
case inl.inr.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 False 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.inr.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 False 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 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
State after:
case inl.inr.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 False 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 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