awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
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 (α →₀ ℕ)))
⊢ 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 (α →₀ ℕ))

Tactic:
simp only [le_iff_eq_or_lt, lt_iff, EmbeddingLike.apply_eq_iff_eq]

Premises used: le_iff_eq_or_lt, EmbeddingLike.apply_eq_iff_eq, Finsupp.DegLex.lt_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : x = 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:
simp [h]
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
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:
simp [k]
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
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:
simp only [h, k, false_or]

Premises used: false_or
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b : DegLex (α →₀ ℕ)
h : a ≤ b
c : DegLex (α →₀ ℕ)
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 (α →₀ ℕ))
⊢ a + c ≤ b + c

Tactic:
rw [le_iff] at h ⊢

Premises used: Finsupp.DegLex.le_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b : DegLex (α →₀ ℕ)
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:
simpa [ofDegLex_add, map_add] using h

Premises used: map_add, ofDegLex_add
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
h : a + b ≤ a + c
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 (α →₀ ℕ))
⊢ b ≤ c

Tactic:
rw [le_iff] at h ⊢

Premises used: Finsupp.DegLex.le_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
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:
simpa only [ofDegLex_add, map_add, add_lt_add_iff_left, add_right_inj, toLex_add,
      add_le_add_iff_left] using h

Premises used: add_le_add_iff_left, toLex_add, map_add, ofDegLex_add, add_right_inj, add_lt_add_iff_left
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a : α
_ :
  ∀ ⦃b : α⦄,
    a < b →
      LT.lt.{u_1} (α := DegLex (α →₀ ℕ))
        ((fun (a : α) ↦ ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1) : DegLex (α →₀ ℕ))) b)
        ((fun (a : α) ↦ ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1) : DegLex (α →₀ ℕ))) a)
⊢ ∀ ⦃b : α⦄,
    a < b →
      LT.lt.{u_1} (α := DegLex (α →₀ ℕ))
        ((fun (a : α) ↦ ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1) : DegLex (α →₀ ℕ))) b)
        ((fun (a : α) ↦ ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1) : DegLex (α →₀ ℕ))) a)

Tactic:
_
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ LT.lt.{u_1} (α := DegLex (α →₀ ℕ))
    ((fun (a : α) ↦ ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1) : DegLex (α →₀ ℕ))) b)
    ((fun (a : α) ↦ ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1) : DegLex (α →₀ ℕ))) a)

Tactic:
simp only [lt_iff, ofDegLex_toDegLex, degree_single, lt_self_iff_false, Lex.single_lt_iff, h,
    and_self, or_true]

Premises used: and_self, Finsupp.Lex.single_lt_iff, ofDegLex_toDegLex, Finsupp.DegLex.lt_iff, lt_self_iff_false, Finsupp.degree_single, or_true
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
⊢ Antitone (β := DegLex (α →₀ ℕ)) fun (a : α) ↦ (toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1)

Tactic:
single_strictAnti.antitone

Premises used: Finsupp.DegLex.single_strictAnti, StrictAnti.antitone
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ LT.lt (α := DegLex (α →₀ ℕ)) ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single b 1) : DegLex (α →₀ ℕ))
      ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1) : DegLex (α →₀ ℕ)) ↔
    a < b

Tactic:
single_strictAnti.lt_iff_gt

Premises used: StrictAnti.lt_iff_gt, Finsupp.DegLex.single_strictAnti
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ LE.le (α := DegLex (α →₀ ℕ)) ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single b 1) : DegLex (α →₀ ℕ))
      ((toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) (single a 1) : DegLex (α →₀ ℕ)) ↔
    a ≤ b

Tactic:
single_strictAnti.le_iff_ge

Premises used: StrictAnti.le_iff_ge, Finsupp.DegLex.single_strictAnti
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
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)
⊢ x ≤ y →
    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]

Premises used: Finsupp.DegLex.le_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
h :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) y : α →₀ ℕ) : ℕ)
⊢ LE.le (α := ℕ)
    ((fun (x : DegLex (α →₀ ℕ)) ↦
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ))
      x)
    ((fun (x : DegLex (α →₀ ℕ)) ↦
        ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ))
      y)

Tactic:
apply le_of_lt h

Premises used: le_of_lt
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x y : DegLex (α →₀ ℕ)
h :
  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:
apply le_of_eq h.1

Premises used: And.left, le_of_eq
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x : DegLex (α →₀ ℕ)
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 (α →₀ ℕ))
⊢ (toDegLex : (a : α →₀ ℕ) → DegLex (α →₀ ℕ)) 0 ≤ x

Tactic:
simp only [le_iff, ofDegLex_toDegLex, toLex_zero, map_zero]

Premises used: map_zero, toLex_zero, ofDegLex_toDegLex, Finsupp.DegLex.le_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 (α →₀ ℕ))
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 (α →₀ ℕ))
⊢ 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)

Premises used: ofDegLex, Finsupp.degree, eq_zero_or_pos, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x : DegLex (α →₀ ℕ)
h : Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) (0 : ℕ)
inl :
  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 (α →₀ ℕ))

Tactic:
simp only [h, lt_self_iff_false, true_and, false_or]

Premises used: false_or, lt_self_iff_false, true_and
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x : DegLex (α →₀ ℕ)
h : Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : ℕ) (0 : ℕ)
⊢ LE.le (α := Lex (α →₀ ℕ)) (0 : Lex (α →₀ ℕ))
    ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) x : α →₀ ℕ) : Lex (α →₀ ℕ))

Tactic:
bot_le

Premises used: bot_le