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

State before:
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
⊢ Order.grlex v₁ v₂
Tactic:
simp [Order.grlex]
State after:
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
⊢ 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

State before:
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
⊢ 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
Tactic:
split
State after:
case inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
⊢ True

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

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

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

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

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

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

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
simp [algebra.Order.bgrlex] 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 :
  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
⊢ if Order.lex v₁ v₂ then True else False

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

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 :
  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
⊢ if Order.lex v₁ v₂ then True else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
split at h
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✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

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✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
simp at *
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✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False
h✝ : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

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✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False
h✝ : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

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

State before:
case inr.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False
h✝ : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

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

State before:
case inr.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² h✝¹ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
h : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁) → ¬Order.lex v₁ v₂ → False
h✝ : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
rename_i hh
State after:
case inr.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ h✝ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
h : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁) → ¬Order.lex v₁ v₂ → False
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

State before:
case inr.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ h✝ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
h : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁) → ¬Order.lex v₁ v₂ → False
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

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

State before:
case inr.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ h✝ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
h : ¬Order.lex v₁ v₂ → False
⊢ if Order.lex v₁ v₂ then True else 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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
split
State after:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² h✝¹ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
h : ¬Order.lex v₁ v₂ → False
h✝ : Order.lex v₁ v₂
⊢ True

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² h✝¹ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
h : ¬Order.lex v₁ v₂ → False
h✝ : ¬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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

State before:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² h✝¹ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
h : ¬Order.lex v₁ v₂ → False
h✝ : Order.lex v₁ v₂
⊢ True

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² h✝¹ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
h : ¬Order.lex v₁ v₂ → False
h✝ : ¬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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
simp
State after:
case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² h✝¹ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
h : ¬Order.lex v₁ v₂ → False
h✝ : ¬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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

State before:
case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² h✝¹ : List.foldl (fun x y => x + y) 0 (toList v₁) = List.foldl (fun x y => x + y) 0 (toList v₂)
hh : List.foldl (fun x y => x + y) 0 (toList v₂) ≤ List.foldl (fun x y => x + y) 0 (toList v₁)
h : ¬Order.lex v₁ v₂ → False
h✝ : ¬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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
contradiction
State after:
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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

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

State before:
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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ if Order.lex v₁ v₂ then True else False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
split
State after:
case inr.inl.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✝¹ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝ : Order.lex v₁ v₂
⊢ True

case inr.inl.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✝¹ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝ : ¬Order.lex v₁ v₂
⊢ False

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

State before:
case inr.inl.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✝¹ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝ : Order.lex v₁ v₂
⊢ True

case inr.inl.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✝¹ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝ : ¬Order.lex v₁ v₂
⊢ False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
simp
State after:
case inr.inl.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✝¹ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝ : ¬Order.lex v₁ v₂
⊢ False

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

State before:
case inr.inl.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✝¹ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝ : ¬Order.lex v₁ v₂
⊢ False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
simp at *
State after:
case inr.inl.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
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 : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝¹ : ¬Order.lex v₁ v₂
h✝ : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ False

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

State before:
case inr.inl.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
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 : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝¹ : ¬Order.lex v₁ v₂
h✝ : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
rename_i h₁
State after:
case inr.inl.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
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 : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝ : ¬Order.lex v₁ v₂
h₁ : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ False

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

State before:
case inr.inl.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
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 : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
h✝ : ¬Order.lex v₁ v₂
h₁ : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ False

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

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

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

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

State before:
case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
⊢ False
Tactic:
simp [Order.bgrlex] at h
State after:
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 :
  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
⊢ False

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 :
  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
⊢ False
Tactic:
split at h
State after:
case inr.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✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False
⊢ False

case inr.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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ False

State before:
case inr.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✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False
⊢ False

case inr.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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ False
Tactic:
contradiction
State after:
case inr.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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ False

State before:
case inr.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✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ False
Tactic:
rename_i nleq neq₁ neq₂
State after:
case inr.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
nleq : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
neq₁ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
neq₂ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ False

State before:
case inr.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
nleq : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
neq₁ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
neq₂ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ False
Tactic:
have leq := Nat.le_of_not_lt nleq
State after:
case inr.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
nleq : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
neq₁ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
neq₂ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
leq : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ False

State before:
case inr.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
nleq : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
neq₁ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
neq₂ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
leq : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ False
Tactic:
exact h leq
State after:
no goals