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

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

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

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

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

case inr.inr.inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : False
⊢ False
Tactic:
have seq := Eq.symm eq₂
Proof state after:
case inr.inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
nleq₁ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
nleq₂ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq₁ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
eq₂ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
ab : if Order.lex a b then True else False
leq : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
seq : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.lex a c then True else False

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

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

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

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

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