-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
pos :
  ∀
    (k :
      LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ)),
    x = y ∨
        LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
            ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∨
          Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
              ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∧
            LT.lt (α := Lex (α →₀ ℕ))
              ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) :
                Lex (α →₀ ℕ))
              ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) :
                Lex (α →₀ ℕ)) ↔
      LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∨
        Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
            ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∧
          (x = y ∨
            LT.lt (α := Lex (α →₀ ℕ))
              ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) :
                Lex (α →₀ ℕ))
              ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) :
                Lex (α →₀ ℕ)))
⊢ x = y ∨
      LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∨
        Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
            ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∧
          LT.lt (α := Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) :
              Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) :
              Lex (α →₀ ℕ)) ↔
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∧
        (x = y ∨
          LT.lt (α := Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) :
              Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) :
              Lex (α →₀ ℕ)))
have neg : ∀
  (k :
    ¬LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ)),
  x = y ∨
      LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∨
        Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
            ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∧
          LT.lt (α := Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) :
              Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) :
              Lex (α →₀ ℕ)) ↔
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ) ∧
        (x = y ∨
          LT.lt (α := Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) :
              Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) :
              Lex (α →₀ ℕ)))
Tactic: by_cases k : (ofDegLex x).degree < (ofDegLex y).degree