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

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

State before:
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
have contr := lex_le_total a b
State after:
n : ℕ
a b : Variables n order.GrLex
contr : Order.lex a b ∨ Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

State before:
n : ℕ
a b : Variables n order.GrLex
contr : Order.lex a b ∨ Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
cases contr
State after:
case inl
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex a b
⊢ Order.grlex a b ∨ Order.grlex b a

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

State before:
case inl
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex a b
⊢ Order.grlex a b ∨ Order.grlex b a

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
split <;> simp
State after:
case inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝¹ : Order.lex a b
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
⊢ (if Order.grlex.elem_sum a = Order.grlex.elem_sum b then True else False) ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then if Order.lex b a then True else False else False

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
split <;> repeat (first | split | simp)
State after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
simp at *
State after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝² : ¬Order.lex b a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ False

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
rename_i neq₁ eq nle _ _
State after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex a b
neq₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
nle : ¬Order.lex b a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ False

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

State before:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex a b
neq₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
nle : ¬Order.lex b a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ False

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
have contr := Eq.symm eq
State after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex a b
neq₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
nle : ¬Order.lex b a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

State before:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex a b
neq₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
eq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
nle : ¬Order.lex b a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
contradiction
State after:
case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
simp
State after:
case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
simp at *
State after:
case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ False

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
rename_i neq₁ neq₂ nleq₁ nleq₂
State after:
case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex a b
neq₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
neq₂ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
nleq₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ False

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
have contr := Nat.le_antisymm nleq₁ nleq₂
State after:
case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex a b
neq₁ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
neq₂ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
nleq₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
nleq₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

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

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
contradiction
State after:
case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a

State before:
case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
Tactic:
simp [Order.grlex]
State after:
case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ (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) ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then if Order.lex b a then True else False else False

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

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

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

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

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

State before:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
neq : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
rw [eq] at neq
State after:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
neq : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum b
⊢ False

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

State before:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
neq : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum b
⊢ False

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

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

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

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

case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
simp at *
State after:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False

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

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

State before:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
have contr := Nat.le_antisymm h₁ h₂
State after:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False

State before:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
rw [contr] at neq
State after:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum a
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False

State before:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum a
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
simp at *
State after:
no goals

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

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Tactic:
(first | split | simp)
State after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False

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

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

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Tactic:
first | split | simp
State after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False

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

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

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

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

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

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

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Tactic:
simp
State after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False

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

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

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
(first | split | simp)
State after:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

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

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

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

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

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

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

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

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

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

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

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