awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∧
    LT.lt (α := Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
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 (α →₀ ℕ))
have inr : 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: right
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ 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 : α →₀ ℕ) : ℕ) ∧
        LE.le (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) :
            Lex (α →₀ ℕ))
have simp : 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: simp only [le_iff_eq_or_lt, lt_iff, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : DegLex (α →₀ ℕ)
h : a ≤ b
c : DegLex (α →₀ ℕ)
⊢ a + c ≤ b + c
have rw : ∀
  (h :
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ) ∧
        LE.le (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) :
            Lex (α →₀ ℕ)))
  (c : DegLex (α →₀ ℕ)),
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + c) : α →₀ ℕ) : ℕ)
      ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (b + c) : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + c) : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (b + c) : α →₀ ℕ) : ℕ) ∧
      LE.le (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + c) : α →₀ ℕ) :
          Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (b + c) : α →₀ ℕ) :
          Lex (α →₀ ℕ))
Tactic: rw [le_iff] at h ⊢
Cleared hypotheses: h, c
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
h : a + b ≤ a + c
⊢ b ≤ c
have rw : ∀
  (h :
    LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + b) : α →₀ ℕ) : ℕ)
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + c) : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + b) : α →₀ ℕ) : ℕ)
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + c) : α →₀ ℕ) : ℕ) ∧
        LE.le (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + b) : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) (a + c) : α →₀ ℕ) :
            Lex (α →₀ ℕ))),
  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 : α →₀ ℕ) : ℕ) ∧
      LE.le (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: rw [le_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ x ≤ y →
    LE.le (α := ℕ)
      ((fun (x : DegLex (α →₀ ℕ)) ↦
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ))
        x)
      ((fun (x : DegLex (α →₀ ℕ)) ↦
          ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ))
        y)
have rw : 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 : α →₀ ℕ) : ℕ) ∧
      LE.le (α := Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) :
          Lex (α →₀ ℕ)) →
  LE.le (α := ℕ)
    ((fun (x : DegLex (α →₀ ℕ)) ↦
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ))
      x)
    ((fun (x : DegLex (α →₀ ℕ)) ↦
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ))
      y)
Tactic: rw [le_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x : DegLex (α →₀ ℕ)
⊢ (toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) 0 ≤ x
have simp : LT.lt (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∨
  Eq (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∧
    LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: simp only [le_iff, ofDegLex_toDegLex, toLex_zero, map_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x : DegLex (α →₀ ℕ)
⊢ LT.lt (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∧
      LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))
have inl : ∀ (h : Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) (0 : ℕ)),
  LT.lt (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∧
      LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: rcases eq_zero_or_pos (ofDegLex x).degree with (h | h)
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x : DegLex (α →₀ ℕ)
inl :
  ∀
    (h :
      Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) (0 : ℕ)),
    LT.lt (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∨
      Eq (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∧
        LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) :
            Lex (α →₀ ℕ))
⊢ LT.lt (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∧
      LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))
have inr : ∀
  (h :
    LT.lt (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)),
  LT.lt (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∧
      LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: rcases eq_zero_or_pos (ofDegLex x).degree with (h | h)
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x : DegLex (α →₀ ℕ)
h : Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) (0 : ℕ)
⊢ LT.lt (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∨
    Eq (α := ℕ) (0 : ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) ∧
      LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
        ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))
have inl : LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
  ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))
Tactic: simp only [h, lt_self_iff_false, true_and, false_or]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
⊢ LE.le (α := DegLex (σ →₀ ℕ))
    ((let __Equiv : (σ →₀ ℕ) ≃ DegLex (σ →₀ ℕ) := toDegLex;
          { toEquiv := __Equiv, map_add' := ⋯ } :
          (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ))
        a :
      DegLex (σ →₀ ℕ))
    ((let __Equiv : (σ →₀ ℕ) ≃ DegLex (σ →₀ ℕ) := toDegLex;
          { toEquiv := __Equiv, map_add' := ⋯ } :
          (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ))
        b :
      DegLex (σ →₀ ℕ))
have simp : LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∨
  Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∧
    LE.le (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) a : Lex (σ →₀ ℕ))
      ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) b : Lex (σ →₀ ℕ))
Tactic: simp only [AddEquiv.coe_mk, DegLex.le_iff, ofDegLex_toDegLex]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
⊢ LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∧
      LE.le (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) a : Lex (σ →₀ ℕ))
        ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) b : Lex (σ →₀ ℕ))
have pos : ∀ (ha : LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ)),
  LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∧
      LE.le (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) a : Lex (σ →₀ ℕ))
        ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) b : Lex (σ →₀ ℕ))
Tactic: by_cases! ha : a.degree < b.degree
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
pos :
  ∀ (ha : LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ)),
    LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∨
      Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∧
        LE.le (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) a : Lex (σ →₀ ℕ))
          ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) b : Lex (σ →₀ ℕ))
⊢ LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∧
      LE.le (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) a : Lex (σ →₀ ℕ))
        ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) b : Lex (σ →₀ ℕ))
have neg : ∀ (ha : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ)),
  LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∧
      LE.le (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) a : Lex (σ →₀ ℕ))
        ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) b : Lex (σ →₀ ℕ))
Tactic: by_cases! ha : a.degree < b.degree
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ)
⊢ LT.lt (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∨
    Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ∧
      LE.le (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) a : Lex (σ →₀ ℕ))
        ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) b : Lex (σ →₀ ℕ))
have neg : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ)
Tactic: refine Or.inr ⟨le_antisymm ?_ ha, toLex_monotone h⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ)
⊢ LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ)
have neg : (degree : (a : σ →₀ ℕ) → ℕ) a ≤
  HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (b - a) : ℕ)
Tactic: rw [← add_tsub_cancel_of_le h, map_add]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ
⊢ LE.le (α := syn (σ := σ) degLex) ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (single a 1) : syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (single b 1) : syn (σ := σ) degLex) ↔
    b ≤ a
have rw : LE.le (α := DegLex (σ →₀ ℕ)) ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) (single a 1) : DegLex (σ →₀ ℕ))
    ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) (single b 1) : DegLex (σ →₀ ℕ)) ↔
  b ≤ a
Tactic: rw [MonomialOrder.degLex_le_iff, DegLex.single_le_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ
rw :
  LE.le (α := DegLex (σ →₀ ℕ)) ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) (single a 1) : DegLex (σ →₀ ℕ))
      ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) (single b 1) : DegLex (σ →₀ ℕ)) ↔
    b ≤ a
⊢ LE.le (α := syn (σ := σ) degLex) ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (single a 1) : syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (single b 1) : syn (σ := σ) degLex) ↔
    b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [MonomialOrder.degLex_le_iff, DegLex.single_le_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ
⊢ LT.lt (α := syn (σ := σ) degLex) ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (single a 1) : syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (single b 1) : syn (σ := σ) degLex) ↔
    b < a
have rw : LT.lt (α := DegLex (σ →₀ ℕ)) ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) (single a 1) : DegLex (σ →₀ ℕ))
    ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) (single b 1) : DegLex (σ →₀ ℕ)) ↔
  b < a
Tactic: rw [MonomialOrder.degLex_lt_iff, DegLex.single_lt_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ
rw :
  LT.lt (α := DegLex (σ →₀ ℕ)) ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) (single a 1) : DegLex (σ →₀ ℕ))
      ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) (single b 1) : DegLex (σ →₀ ℕ)) ↔
    b < a
⊢ LT.lt (α := syn (σ := σ) degLex) ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (single a 1) : syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (single b 1) : syn (σ := σ) degLex) ↔
    b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [MonomialOrder.degLex_lt_iff, DegLex.single_lt_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
⊢ LT.lt (α := syn (σ := Fin 2) degLex)
    ((toSyn degLex : (a : Fin 2 →₀ ℕ) → degLex.syn) (single 1 1) : syn (σ := Fin 2) degLex)
    ((toSyn degLex : (a : Fin 2 →₀ ℕ) → degLex.syn) (single 0 1) : syn (σ := Fin 2) degLex)
have rw : LT.lt (α := Fin 2) 0 1
Tactic: rw [degLex_lt_iff, single_lt_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder.DegLex (goal)
Goal:
α : Type u_1
⊢ LT.lt (α := syn (σ := Fin 2) degLex)
    ((toSyn degLex : (a : Fin 2 →₀ ℕ) → degLex.syn) (HAdd.hAdd (α := Fin 2 →₀ ℕ) (single 0 1) (single 1 1)) :
      syn (σ := Fin 2) degLex)
    ((toSyn degLex : (a : Fin 2 →₀ ℕ) → degLex.syn) (single 0 2) : syn (σ := Fin 2) degLex)
have rw : LT.lt (α := ℕ) ((degree : (a : Fin 2 →₀ ℕ) → ℕ) (HAdd.hAdd (α := Fin 2 →₀ ℕ) (single 0 1) (single 1 1)) : ℕ)
    ((degree : (a : Fin 2 →₀ ℕ) → ℕ)
        ((ofDegLex : (a : DegLex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
            ((toDegLex : (a : Fin 2 →₀ ℕ) → DegLex (Fin 2 →₀ ℕ)) (single 0 2)) :
          Fin 2 →₀ ℕ) :
      ℕ) ∨
  Eq (α := ℕ) ((degree : (a : Fin 2 →₀ ℕ) → ℕ) (HAdd.hAdd (α := Fin 2 →₀ ℕ) (single 0 1) (single 1 1)) : ℕ)
      ((degree : (a : Fin 2 →₀ ℕ) → ℕ)
          ((ofDegLex : (a : DegLex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
              ((toDegLex : (a : Fin 2 →₀ ℕ) → DegLex (Fin 2 →₀ ℕ)) (single 0 2)) :
            Fin 2 →₀ ℕ) :
        ℕ) ∧
    LT.lt (α := Lex (Fin 2 →₀ ℕ))
      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (HAdd.hAdd (α := Fin 2 →₀ ℕ) (single 0 1) (single 1 1)) :
        Lex (Fin 2 →₀ ℕ))
      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ))
          ((ofDegLex : (a : DegLex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
            ((toDegLex : (a : Fin 2 →₀ ℕ) → DegLex (Fin 2 →₀ ℕ)) (single 0 2))) :
        Lex (Fin 2 →₀ ℕ))
Tactic: rw [degLex_lt_iff, lt_iff, ofDegLex_toDegLex]