rw [symm] at leq
case inr.inl.inl
n : ℕ
a b : Variables n order.GrLex
nleq : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
leq : Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : True
symm : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ a = b

case inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : if Order.grlex.elem_sum b = Order.grlex.elem_sum a then if Order.lex b a then True else False else False
⊢ a = b

case inr.inr
n : ℕ
a b : Variables n order.GrLex
ba :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then if Order.lex b a then True else False else False
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ a = b
case inr.inl.inl
n : ℕ
a b : Variables n order.GrLex
nleq : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
leq : Order.grlex.elem_sum a < Order.grlex.elem_sum a
ba : True
symm : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ a = b

case inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : if Order.grlex.elem_sum b = Order.grlex.elem_sum a then if Order.lex b a then True else False else False
⊢ a = b

case inr.inr
n : ℕ
a b : Variables n order.GrLex
ba :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then if Order.lex b a then True else False else False
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ a = b