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

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

State before:
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ Order.grlex a c
Tactic:
simp [Order.grlex]
State after:
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False

State before:
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Tactic:
simp [Order.grlex] at ab bc
State after:
n : ℕ
a b c : 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
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False

State before:
n : ℕ
a b c : 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
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Tactic:
split <;> simp
State after:
case inr
n : ℕ
a b c : 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
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
⊢ if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
nleq : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
leq₁ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
leq₂ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
⊢ False

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

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

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

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

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

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

State before:
case inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
nleq : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
leq₁ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
leq₂ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
contr : Order.grlex.elem_sum a < Order.grlex.elem_sum c
⊢ False

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
nleq₁ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
nleq₂ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
have seq := Eq.symm eq₂
State after:
case inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
nleq₁ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
nleq₂ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
seq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
nleq₁ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
nleq₂ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
seq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
rw [seq] at leq
State after:
case inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
nleq₁ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
nleq₂ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
seq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
nleq₁ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
nleq₂ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
seq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
⊢ if Order.lex a c then True else False

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
rename_i nleq₁ nleq₂ eq₁ eq₂ neq₁ eq₃
State after:
case inr.inr.inl.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
nleq₁ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
nleq₂ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
neq₁ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
nleq₁ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
nleq₂ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
neq₁ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
simp at *
State after:
case inr.inr.inl.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
⊢ if Order.lex a c then True else False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
split
State after:
case inr.inr.inl.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝ : Order.lex a c
⊢ True

case inr.inr.inl.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝ : ¬Order.lex a c
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝ : Order.lex a c
⊢ True

case inr.inr.inl.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝ : ¬Order.lex a c
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
simp [lex_le_trans]
State after:
case inr.inr.inl.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝ : ¬Order.lex a c
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝ : ¬Order.lex a c
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
split at ab
State after:
case inr.inr.inl.inl.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : Order.lex a b
ab : True
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : Order.lex a b
ab : True
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
split at bc
State after:
case inr.inr.inl.inl.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝² : ¬Order.lex a c
h✝¹ : Order.lex a b
ab : True
h✝ : Order.lex b c
bc : True
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝² : ¬Order.lex a c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b c
bc : False
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝² : ¬Order.lex a c
h✝¹ : Order.lex a b
ab : True
h✝ : Order.lex b c
bc : True
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝² : ¬Order.lex a c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b c
bc : False
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
rename_i h₁ h₂ h₃
State after:
case inr.inr.inl.inl.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h₁ : ¬Order.lex a c
h₂ : Order.lex a b
ab : True
h₃ : Order.lex b c
bc : True
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝² : ¬Order.lex a c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b c
bc : False
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h₁ : ¬Order.lex a c
h₂ : Order.lex a b
ab : True
h₃ : Order.lex b c
bc : True
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝² : ¬Order.lex a c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b c
bc : False
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
have contr := lex_le_trans a b c h₂ h₃
State after:
case inr.inr.inl.inl.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h₁ : ¬Order.lex a c
h₂ : Order.lex a b
ab : True
h₃ : Order.lex b c
bc : True
contr : Order.lex a c
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝² : ¬Order.lex a c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b c
bc : False
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

State before:
case inr.inr.inl.inl.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h₁ : ¬Order.lex a c
h₂ : Order.lex a b
ab : True
h₃ : Order.lex b c
bc : True
contr : Order.lex a c
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝² : ¬Order.lex a c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.lex b c
bc : False
⊢ False

case inr.inr.inl.inl.inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq₃ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
nleq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
neq₁ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a c
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

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

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

State before:
case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
split at ab
State after:
case inr.inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : Order.lex a b
ab : True
⊢ False

case inr.inr.inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

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

case inr.inr.inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
rename_i h₁ h₂ h₃ h₄
State after:
case inr.inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h₄ : Order.lex a b
ab : True
⊢ False

case inr.inr.inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

State before:
case inr.inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h₄ : Order.lex a b
ab : True
⊢ False

case inr.inr.inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
rw [← h₂] at h₃
State after:
case inr.inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum c
bc : True
h₄ : Order.lex a b
ab : True
⊢ False

case inr.inr.inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

State before:
case inr.inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.grlex.elem_sum a < Order.grlex.elem_sum c
bc : True
h₄ : Order.lex a b
ab : True
⊢ False

case inr.inr.inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : ¬Order.lex a b
ab : False
⊢ False

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

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

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

State before:
case inr.inr.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
⊢ False

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
split at ab
State after:
case inr.inr.inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝ : Order.lex a b
ab : True
⊢ False

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

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

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

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
split at bc
State after:
case inr.inr.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
⊢ False

case inr.inr.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : False
⊢ False

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

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

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

case inr.inr.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : False
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
simp at *
State after:
case inr.inr.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝⁵ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝⁴ : Order.lex a b
ab : True
h✝³ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
h✝² : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
⊢ False

case inr.inr.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : False
⊢ False

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

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

State before:
case inr.inr.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝⁵ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝⁴ : Order.lex a b
ab : True
h✝³ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
h✝² : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
⊢ False

case inr.inr.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : False
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
rename_i h₁ h₂ h₃ _ _ _ _
State after:
case inr.inr.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.lex a b
ab : True
h✝³ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
h✝² : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
⊢ False

case inr.inr.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : False
⊢ False

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

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

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

case inr.inr.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : False
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
rw [h₂] at h₁
State after:
case inr.inr.inr.inl.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h₁ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
h₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₃ : Order.lex a b
ab : True
h✝³ : Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : if Order.lex b c then True else False
h✝² : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum c ≤ Order.grlex.elem_sum b
⊢ False

case inr.inr.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : False
⊢ False

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

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

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

case inr.inr.inr.inl.inr.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝⁶ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝⁵ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
h✝¹ : Order.lex a b
ab : True
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum c
bc : False
⊢ False

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
repeat contradiction
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

case inr.inr.inr.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
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 c
bc : True
⊢ False

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

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

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

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

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

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

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

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

State before:
case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
contradiction
State after:
no goals