awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
x : DegLex (α →₀ ℕ)
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:
simp [h]
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedGT α
⊢ WellFoundedLT.{u_1} (DegLex (α →₀ ℕ))

Tactic:
⟨wellFounded wellFounded_gt wellFounded_lt fun _ ↦ not_lt_zero⟩

Premises used: IsWellFounded.mk, wellFounded_lt, not_lt_zero, wellFounded_gt, Finsupp.DegLex.wellFounded
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
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 (σ →₀ ℕ))
⊢ 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 (σ →₀ ℕ))

Tactic:
simp only [AddEquiv.coe_mk, DegLex.le_iff, ofDegLex_toDegLex]

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

Premises used: Finsupp.degree, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
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:
Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
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:
exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 (σ →₀ ℕ))

Tactic:
Or.inr ⟨le_antisymm ?_ ha, toLex_monotone h⟩

Premises used: le_antisymm, And.intro, Finsupp.toLex_monotone, Or.inr
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 : ℕ)
neg : LE.le (α := ℕ) ((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:
refine Or.inr ⟨le_antisymm ?_ ha, toLex_monotone h⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 : ℕ)
neg :
  (degree : (a : σ →₀ ℕ) → ℕ) a ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (b - a) : ℕ)
⊢ LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) b : ℕ)

Tactic:
rw [← add_tsub_cancel_of_le h, map_add]

Premises used: map_add, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 : ℕ)
⊢ (degree : (a : σ →₀ ℕ) → ℕ) a ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (b - a) : ℕ)

Tactic:
Nat.le_add_right a.degree (b - a).degree

Premises used: Nat.le_add_right, HSub.hSub, Finsupp.degree, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 : ℕ)
⊢ (degree : (a : σ →₀ ℕ) → ℕ) a ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) a : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (b - a) : ℕ)

Tactic:
exact Nat.le_add_right a.degree (b - a).degree

Premises used: Nat.le_add_right, HSub.hSub, Finsupp.degree, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
⊢ LE.le (α := syn (σ := σ) degLex) ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) a : syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) b : syn (σ := σ) degLex) ↔
    LE.le (α := DegLex (σ →₀ ℕ)) ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) a : DegLex (σ →₀ ℕ))
      ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) b : DegLex (σ →₀ ℕ))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
σ : Type u_2
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
a b : σ →₀ ℕ
⊢ LT.lt (α := syn (σ := σ) degLex) ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) a : syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) b : syn (σ := σ) degLex) ↔
    LT.lt (α := DegLex (σ →₀ ℕ)) ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) a : DegLex (σ →₀ ℕ))
      ((toDegLex : (a : σ →₀ ℕ) → DegLex (σ →₀ ℕ)) b : DegLex (σ →₀ ℕ))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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
rw₁ rw₂ : b ≤ a ↔ 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

Tactic:
rw [MonomialOrder.degLex_le_iff, DegLex.single_le_iff]

Premises used: MonomialOrder.degLex_le_iff, Finsupp.DegLex.single_le_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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
rw₁ rw₂ : b < a ↔ 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

Tactic:
rw [MonomialOrder.degLex_lt_iff, DegLex.single_lt_iff]

Premises used: Finsupp.DegLex.single_lt_iff, MonomialOrder.degLex_lt_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
rw : LT.lt (α := Fin 2) 0 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)

Tactic:
rw [degLex_lt_iff, single_lt_iff]

Premises used: Finsupp.DegLex.single_lt_iff, MonomialOrder.degLex_lt_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
⊢ LT.lt (α := Fin 2) 0 1

Tactic:
Nat.one_pos

Premises used: Nat.one_pos
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
⊢ LT.lt (α := Fin 2) 0 1

Tactic:
exact Nat.one_pos

Premises used: Nat.one_pos
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
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 →₀ ℕ))
⊢ 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)

Tactic:
rw [degLex_lt_iff, lt_iff, ofDegLex_toDegLex]

Premises used: ofDegLex_toDegLex, Finsupp.DegLex.lt_iff, MonomialOrder.degLex_lt_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
simp :
  HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ)) <
    (toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)
⊢ 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:
simp only [Fin.isValue, map_add, degree_single, Nat.reduceAdd, ofDegLex_toDegLex,
    lt_self_iff_false, toLex_add, true_and, false_or]

Premises used: toLex_add, map_add, Nat.reduceAdd, false_or, ofDegLex_toDegLex, Fin.isValue, lt_self_iff_false, Finsupp.degree_single, true_and
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
h :
  (∀ (j : Fin 2),
      (fun (x1 x2 : Fin 2) ↦ x1 < x2) j 0 →
        Eq (α := (@fun {i : Fin 2} ↦ ℕ) j)
          ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
                    (HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
                      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
                      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ))) :
                  Fin 2 →₀ ℕ) :
                (a : Fin 2) → ℕ)
              j :
            ℕ)
          ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
                    ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)) :
                  Fin 2 →₀ ℕ) :
                (a : Fin 2) → ℕ)
              j :
            ℕ)) ∧
    (@fun {i : Fin 2} (x1 x2 : ℕ) ↦ x1 < x2) 0
      ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
              (HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
                ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
                ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ))) :
            Fin 2 →₀ ℕ) :
          (a : Fin 2) → ℕ)
        0)
      ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ) ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)) :
            Fin 2 →₀ ℕ) :
          (a : Fin 2) → ℕ)
        0)
⊢ HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ)) <
    (toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)

Tactic:
use 0
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
⊢ (∀ (j : Fin 2),
      (fun (x1 x2 : Fin 2) ↦ x1 < x2) j 0 →
        Eq (α := (@fun {i : Fin 2} ↦ ℕ) j)
          ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
                    (HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
                      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
                      ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ))) :
                  Fin 2 →₀ ℕ) :
                (a : Fin 2) → ℕ)
              j :
            ℕ)
          ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
                    ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)) :
                  Fin 2 →₀ ℕ) :
                (a : Fin 2) → ℕ)
              j :
            ℕ)) ∧
    (@fun {i : Fin 2} (x1 x2 : ℕ) ↦ x1 < x2) 0
      ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ)
              (HAdd.hAdd (α := Lex (Fin 2 →₀ ℕ)) (β := Lex (Fin 2 →₀ ℕ))
                ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 1) : Lex (Fin 2 →₀ ℕ))
                ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 1 1) : Lex (Fin 2 →₀ ℕ))) :
            Fin 2 →₀ ℕ) :
          (a : Fin 2) → ℕ)
        0)
      ((((ofLex : (a : Lex (Fin 2 →₀ ℕ)) → Fin 2 →₀ ℕ) ((toLex : (a : Fin 2 →₀ ℕ) → Lex (Fin 2 →₀ ℕ)) (single 0 2)) :
            Fin 2 →₀ ℕ) :
          (a : Fin 2) → ℕ)
        0)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
⊢ LT.lt (α := syn (σ := Fin 2) degLex)
    ((toSyn degLex : (a : Fin 2 →₀ ℕ) → degLex.syn) (single 0 1) : syn (σ := Fin 2) degLex)
    ((toSyn degLex : (a : Fin 2 →₀ ℕ) → degLex.syn) (single 1 2) : syn (σ := Fin 2) degLex)

Tactic:
simp [degLex_lt_iff, lt_iff]

Premises used: Finsupp.DegLex.lt_iff, MonomialOrder.degLex_lt_iff
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, List.foldr, Finset.sum, rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
m n : α →₀ ℕ
⊢ (toMultiset : (a : α →₀ ℕ) → Multiset α) (m + n) =
    HAdd.hAdd (α := Multiset α) (β := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) m : Multiset α)
      ((toMultiset : (a : α →₀ ℕ) → Multiset α) n : Multiset α)

Tactic:
toMultiset.map_add m n

Premises used: Finsupp.toMultiset, AddMonoidHom.map_add
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
f : α →₀ ℕ
⊢ Eq (α := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α)
    (f.sum fun (a : α) (n : ℕ) ↦ HSMul.hSMul (β := Multiset α) n {a} : Multiset α)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
a : α
n : ℕ
rw : HSMul.hSMul (α := ℕ) (β := Multiset α) 0 {a} = 0
⊢ (toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n) = HSMul.hSMul (β := Multiset α) n {a}

Tactic:
rw [toMultiset_apply, sum_single_index]

Premises used: Finsupp.sum_single_index, Finsupp.toMultiset_apply
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
a : α
n : ℕ
⊢ HSMul.hSMul (α := ℕ) (β := Multiset α) 0 {a} = 0

Tactic:
apply zero_nsmul

Premises used: zero_nsmul
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
ι : Type u_3
f : ι → α →₀ ℕ
s : Finset ι
⊢ Eq.{u_1 + 1} (α := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) (∑ i ∈ s, f i))
    (∑ i ∈ s, (toMultiset : (a : α →₀ ℕ) → Multiset α) (f i))

Tactic:
map_sum Finsupp.toMultiset _ _

Premises used: Finsupp.toMultiset, map_sum
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
s : Finset ι
n : ℕ
simp_rw : ∑ i ∈ s, (toMultiset : (a : ι →₀ ℕ) → Multiset ι) (single i n) = n • s.val
simp_rw₁ : ∑ x ∈ s, HSMul.hSMul (β := Multiset ι) n {x} = n • s.val
simp_rw₂ : HSMul.hSMul (β := Multiset ι) n (∑ x ∈ s, {x}) = n • s.val
⊢ (toMultiset : (a : ι →₀ ℕ) → Multiset ι) (∑ i ∈ s, single i n) = n • s.val

Tactic:
simp_rw [toMultiset_sum, Finsupp.toMultiset_single, Finset.sum_nsmul, sum_multiset_singleton]

Premises used: Finset.sum_nsmul, Finsupp.toMultiset_sum, Finset.sum_multiset_singleton, Finsupp.toMultiset_single
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
f : α →₀ ℕ
⊢ Multiset.card.{u_1} (α := α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.sum fun (x : α) ↦ id

Tactic:
simp [toMultiset_apply, Function.id_def]

Premises used: Function.id_def, Finsupp.toMultiset_apply
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f)

Tactic:
f.induction ?_ ?_

Premises used: Finsupp.induction
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
refine_1 :
  Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
refine_2 :
  ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) =
            (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) →
          Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a b + f)) =
            (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g (single a b + f))
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f)

Tactic:
refine f.induction ?_ ?_
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
refine_1 : Multiset.map g 0 = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)
refine_1₁ :
  Eq (α := Multiset β) (0 : Multiset β) ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0) : Multiset β)
refine_1₂ : Eq.{u_2 + 1} (α := Multiset β) 0 ((toMultiset : (a : β →₀ ℕ) → Multiset β) 0)
refine_1₃ refine_1₄ : Eq.{u_2 + 1} (α := Multiset β) 0 0
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g 0)

Tactic:
rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]

Premises used: Finsupp.toMultiset_zero, Multiset.map_zero, Finsupp.mapDomain_zero
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
f_1 : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
refine_2 :
  a ∉ f.support →
    n ≠ 0 →
      Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) =
          (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) →
        Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)) =
          (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g (single a n + f))
⊢ a ∉ f.support →
    n ≠ 0 →
      Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) =
          (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) →
        Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)) =
          (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g (single a n + f))

Tactic:
_