-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hbc :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
inl :
  ∀
    (hbc :
      LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)),
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
        LT.lt (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) :
            Lex (α →₀ ℕ))
inl₁ :
  ∀
    (hbc :
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
        LT.lt (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) :
            Lex (α →₀ ℕ))),
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
        LT.lt (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) :
            Lex (α →₀ ℕ))
⊢ LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ) ∧
      LT.lt (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))

Tactic:
rcases hbc with (hbc | hbc)