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

State before:
n : ℕ
⊢ ∀ (a b : Variables n order.GrLex), Order.grlex a b → Order.grlex b a → a = b
Tactic:
intros a b ab ba
State after:
n : ℕ
a b : Variables n order.GrLex
ab : Order.grlex a b
ba : Order.grlex b a
⊢ a = b

State before:
n : ℕ
a b : Variables n order.GrLex
ab : Order.grlex a b
ba : Order.grlex b a
⊢ a = b
Tactic:
simp [Order.grlex] at ab ba
State after:
n : ℕ
a b : Variables n order.GrLex
ab :
  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
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
⊢ a = b

State before:
n : ℕ
a b : Variables n order.GrLex
ab :
  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
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
⊢ a = b
Tactic:
split at ab
State after:
case inl
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
ab : True
⊢ a = b

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

State before:
case inl
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
ab : True
⊢ a = b

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
split at ba
State after:
case inl.inl
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
h✝ : Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : True
⊢ a = b

case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
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
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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

State before:
case inl.inl
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
h✝ : Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : True
⊢ a = b

case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
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
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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
rename_i leq₁ leq₂
State after:
case inl.inl
n : ℕ
a b : Variables n order.GrLex
leq₁ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
leq₂ : Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : True
⊢ a = b

case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
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
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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

State before:
case inl.inl
n : ℕ
a b : Variables n order.GrLex
leq₁ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
leq₂ : Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : True
⊢ a = b

case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
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
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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
have asymm_leq₁ := Nat.lt_asymm leq₁
State after:
case inl.inl
n : ℕ
a b : Variables n order.GrLex
leq₁ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
leq₂ : Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : True
asymm_leq₁ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ a = b

case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
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
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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

State before:
case inl.inl
n : ℕ
a b : Variables n order.GrLex
leq₁ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
leq₂ : Order.grlex.elem_sum b < Order.grlex.elem_sum a
ba : True
asymm_leq₁ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ a = b

case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
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
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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
contradiction
State after:
case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
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
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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

State before:
case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
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
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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
split at ba
State after:
case inl.inr.inl
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ a = b

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

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

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

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

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
rename_i leq nleq eq
State after:
case inl.inr.inl
n : ℕ
a b : Variables n order.GrLex
leq : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
nleq : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
eq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ a = b

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

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

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

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

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
rw [eq] at leq
State after:
case inl.inr.inl
n : ℕ
a b : Variables n order.GrLex
leq : Order.grlex.elem_sum a < Order.grlex.elem_sum a
ab : True
nleq : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
eq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ a = b

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

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

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

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

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
simp at leq
State after:
case inl.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : False
⊢ a = b

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

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

case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
contradiction
State after:
case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b

State before:
case 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
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ a = b
Tactic:
split at ab
State after:
case inr.inl
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 : if Order.lex a b then True 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

State before:
case inr.inl
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 : if Order.lex a b then True 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
Tactic:
split at ba
State after:
case inr.inl.inl
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 : True
⊢ 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

State before:
case inr.inl.inl
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 : True
⊢ 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
Tactic:
rename_i nleq eq leq
State after:
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
⊢ 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

State before:
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
⊢ 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
Tactic:
have symm := Eq.symm eq
State after:
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

State before:
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
Tactic:
rw [symm] at leq
State after:
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

State before:
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
Tactic:
simp at leq
State after:
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

State before:
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
Tactic:
split at ba
State after:
case inr.inl.inr.inl
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ a = b

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ a = b

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
apply lex_le_antisymm
State after:
case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
split at ab
State after:
case inr.inl.inr.inl.a.inl
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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : Order.lex a b
ab : True
⊢ Order.lex a b

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.inl
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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : Order.lex a b
ab : True
⊢ Order.lex a b

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
split at ba
State after:
case inr.inl.inr.inl.a.inl.inl
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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : Order.lex b a
ba : True
⊢ Order.lex a b

case inr.inl.inr.inl.a.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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex a b

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.inl.inl
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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : Order.lex b a
ba : True
⊢ Order.lex a b

case inr.inl.inr.inl.a.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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex a b

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
repeat (
  rename_i h₁ _
  exact h₁
)
State after:
case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
contradiction
State after:
case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
split at ab
State after:
case inr.inl.inr.inl.a.inl
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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : Order.lex a b
ab : True
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.inl
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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : Order.lex a b
ab : True
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
split at ba
State after:
case inr.inl.inr.inl.a.inl.inl
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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : Order.lex b a
ba : True
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.inl.inl
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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : Order.lex b a
ba : True
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
rename_i h
State after:
case inr.inl.inr.inl.a.inl.inl
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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : Order.lex a b
ab : True
h : Order.lex b a
ba : True
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.inl.inl
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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : Order.lex a b
ab : True
h : Order.lex b a
ba : True
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
exact h
State after:
case inr.inl.inr.inl.a.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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.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
h✝³ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝² : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex b a

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
repeat contradiction
State after:
no goals

State before:
case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
(
rename_i h₁ _
exact h₁
)
State after:
case inr.inl.inr.inl.a.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
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h₁ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
rename_i h₁ _
State after:
case inr.inl.inr.inl.a.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
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h₁ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h₁ : Order.lex a b
ab : True
h✝ : ¬Order.lex b a
ba : False
⊢ Order.lex a b

case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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
Tactic:
exact h₁
State after:
case inr.inl.inr.inl.a.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
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
h✝ : ¬Order.lex a b
ab : False
⊢ Order.lex a b

case inr.inl.inr.inl.a
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
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : if Order.lex b a then True else False
⊢ Order.lex b a

case inr.inl.inr.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
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
ba : 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

State before:
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
Tactic:
contradiction
State after:
no goals