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

State before:
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : Order.grlex v₁ v₂
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
simp [Order.grlex] at h
State after:
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h :
  if Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂ then True
  else if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h :
  if Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂ then True
  else if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
split at h
State after:
case inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
⊢ algebra.Order.bgrlex v₁ v₂ = true

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
⊢ algebra.Order.bgrlex v₁ v₂ = true

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
simp [algebra.Order.bgrlex]
State after:
case inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ →
    if algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂ then ¬Order.lex v₁ v₂ → False else False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ →
    if algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂ then ¬Order.lex v₁ v₂ → False else False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
split
State after:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
rename_i h
State after:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
have le := Nat.le_of_eq h
State after:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
simp [h]
State after:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
rename_i hle _
State after:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
hle : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
hle : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
rw [Order.grlex.elem_sum, Order.grlex.elem_sum] at hle
State after:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
hle : List.foldl (fun x y => x + y) 0 (toList v₁) < List.foldl (fun x y => x + y) 0 (toList v₂)
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
hle : List.foldl (fun x y => x + y) 0 (toList v₁) < List.foldl (fun x y => x + y) 0 (toList v₂)
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
rw [algebra.Order.bgrlex.elem_sum, algebra.Order.bgrlex.elem_sum] at h
State after:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
hle : List.foldl (fun x y => x + y) 0 (toList v₁) < List.foldl (fun x y => x + y) 0 (toList v₂)
h✝ : True
h : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
hle : List.foldl (fun x y => x + y) 0 (toList v₁) < List.foldl (fun x y => x + y) 0 (toList v₂)
h✝ : True
h : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
rw [h] at hle
State after:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
hle : List.foldl (fun x y => x + y) 0 (toList v₂) < List.foldl (fun x y => x + y) 0 (toList v₂)
h✝ : True
h : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
hle : List.foldl (fun x y => x + y) 0 (toList v₂) < List.foldl (fun x y => x + y) 0 (toList v₂)
h✝ : True
h : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
simp at hle
State after:
case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
rename_i le neq
State after:
case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
le : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
neq : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
le : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
neq : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
intros nleq
State after:
case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
le : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
neq : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
nleq : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁
⊢ False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
le : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
neq : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
nleq : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁
⊢ False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
have le_contr := Nat.not_lt_of_le nleq
State after:
case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
le : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
neq : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
nleq : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁
le_contr : ¬algebra.Order.bgrlex.elem_sum v₁ < algebra.Order.bgrlex.elem_sum v₂
⊢ False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
le : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
neq : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
nleq : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁
le_contr : ¬algebra.Order.bgrlex.elem_sum v₁ < algebra.Order.bgrlex.elem_sum v₂
⊢ False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
contradiction
State after:
case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
split at h
State after:
case inr.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inr.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
⊢ algebra.Order.bgrlex v₁ v₂ = true

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
simp [algebra.Order.bgrlex]
State after:
case inr.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ →
    if algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂ then ¬Order.lex v₁ v₂ → False else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inr.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ →
    if algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂ then ¬Order.lex v₁ v₂ → False else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
split
State after:
case inr.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inr.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
split at h
State after:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : Order.lex v₁ v₂
h : True
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : ¬Order.lex v₁ v₂
h : False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : Order.lex v₁ v₂
h : True
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : ¬Order.lex v₁ v₂
h : False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
intros _ hh
State after:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : Order.lex v₁ v₂
h : True
a✝ : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁
hh : ¬Order.lex v₁ v₂
⊢ False

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : ¬Order.lex v₁ v₂
h : False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true

State before:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : Order.lex v₁ v₂
h : True
a✝ : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁
hh : ¬Order.lex v₁ v₂
⊢ False

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : ¬Order.lex v₁ v₂
h : False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
repeat contradiction
State after:
no goals

State before:
case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
contradiction
State after:
no goals