awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
hr : WellFounded (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) Set.univ (Prod.Lex s (Finsupp.Lex r s))
rw :
  Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) (Set.range fun (x : α →₀ ℕ) ↦ ((degree : (a : α →₀ ℕ) → ℕ) x, x))
    (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (α := α →₀ ℕ)
    (Function.onFun (β := ℕ × (α →₀ ℕ)) (Prod.Lex s (Finsupp.Lex r s)) fun (x : α →₀ ℕ) ↦
      ((degree : (a : α →₀ ℕ) → ℕ) x, x))

Tactic:
rw [← Set.wellFoundedOn_range]

Premises used: Set.wellFoundedOn_range
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
hr : WellFounded (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) Set.univ (Prod.Lex s (Finsupp.Lex r s))
⊢ Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) (Set.range fun (x : α →₀ ℕ) ↦ ((degree : (a : α →₀ ℕ) → ℕ) x, x))
    (Prod.Lex s (Finsupp.Lex r s))

Tactic:
Set.WellFoundedOn.mono wft (le_refl _) (fun _ _ ↦ trivial)

Premises used: le_refl, trivial, Set.WellFoundedOn.mono
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
hr : WellFounded (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) Set.univ (Prod.Lex s (Finsupp.Lex r s))
⊢ Set.WellFoundedOn (α := ℕ × (α →₀ ℕ)) (Set.range fun (x : α →₀ ℕ) ↦ ((degree : (a : α →₀ ℕ) → ℕ) x, x))
    (Prod.Lex s (Finsupp.Lex r s))

Tactic:
exact Set.WellFoundedOn.mono wft (le_refl _) (fun _ _ ↦ trivial)

Premises used: le_refl, trivial, Set.WellFoundedOn.mono
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LT α
a b : DegLex (α →₀ ℕ)
⊢ a < b ↔
    LT.lt (α := Lex (ℕ × Lex (α →₀ ℕ)))
      ((toLex : (a : ℕ × Lex (α →₀ ℕ)) → Lex (ℕ × Lex (α →₀ ℕ)))
          (((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ),
              (toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ)) :
            ℕ × Lex (α →₀ ℕ)) :
        Lex (ℕ × Lex (α →₀ ℕ)))
      ((toLex : (a : ℕ × Lex (α →₀ ℕ)) → Lex (ℕ × Lex (α →₀ ℕ)))
          (((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ),
              (toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ)) :
            ℕ × Lex (α →₀ ℕ)) :
        Lex (ℕ × Lex (α →₀ ℕ)))

Tactic:
Iff.rfl

Premises used: Lex, Iff.rfl, Finsupp.DegLex
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LT α
a b : DegLex (α →₀ ℕ)
⊢ a < b ↔
    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 : α →₀ ℕ) : ℕ) ∧
        LT.lt (α := Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) :
            Lex (α →₀ ℕ))
          ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) :
            Lex (α →₀ ℕ))

Tactic:
simp [lt_def, Prod.Lex.toLex_lt_toLex]

Premises used: Prod.Lex.toLex_lt_toLex, Finsupp.DegLex.lt_def
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a : DegLex (α →₀ ℕ)
⊢ ¬a < a

Tactic:
simp [lt_def]

Premises used: Finsupp.DegLex.lt_def
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : a < b
hbc : b < c
simp :
  ∀
    (hab :
      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 : α →₀ ℕ) : ℕ) ∧
          LT.lt (α := Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) :
              Lex (α →₀ ℕ))
            ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) :
              Lex (α →₀ ℕ)))
    (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 (α →₀ ℕ))),
    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 (α →₀ ℕ))
⊢ a < c

Tactic:
simp only [lt_iff] at hab hbc ⊢

Premises used: Finsupp.DegLex.lt_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
hbc :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)
inl :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((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 (α →₀ ℕ))

Tactic:
left
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
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 : α →₀ ℕ) : ℕ)

Tactic:
lt_trans hab hbc

Premises used: lt_trans
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
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 : α →₀ ℕ) : ℕ)

Tactic:
exact lt_trans hab hbc

Premises used: lt_trans
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
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 (α →₀ ℕ))
inl :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((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 (α →₀ ℕ))

Tactic:
left
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
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 : α →₀ ℕ) : ℕ)

Tactic:
lt_of_lt_of_eq hab hbc.1

Premises used: lt_of_lt_of_eq, And.left
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
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 : α →₀ ℕ) : ℕ)

Tactic:
exact lt_of_lt_of_eq hab hbc.1

Premises used: lt_of_lt_of_eq, And.left
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) b : α →₀ ℕ) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) c : α →₀ ℕ) : ℕ)
inr :
  LT.lt (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) a : α →₀ ℕ) : ℕ)
    ((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 (α →₀ ℕ))

Tactic:
left
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 :
  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 : α →₀ ℕ) : ℕ)

Tactic:
lt_of_eq_of_lt hab.1 hbc

Premises used: lt_of_eq_of_lt, And.left
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 :
  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 : α →₀ ℕ) : ℕ)

Tactic:
exact lt_of_eq_of_lt hab.1 hbc

Premises used: lt_of_eq_of_lt, And.left
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 (α →₀ ℕ))
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 (α →₀ ℕ))
⊢ 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:
right
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 (α →₀ ℕ))
⊢ 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:
⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩

Premises used: lt_trans, And.right, And.left, And.intro, Eq.trans
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
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 (α →₀ ℕ))
⊢ 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:
exact ⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩
-- Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex
Goal:
α : Type u_1
inst : LinearOrder α
f g : DegLex (α →₀ ℕ)
⊢ Eq.{u_1 + 1} (α := Lex (ℕ × Lex (α →₀ ℕ)))
      ((fun (f : DegLex (α →₀ ℕ)) ↦
          ((toLex : (a : ℕ × Lex (α →₀ ℕ)) → Lex (ℕ × Lex (α →₀ ℕ)))
              (((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) f : α →₀ ℕ),
                  (toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) f : α →₀ ℕ)) :
                ℕ × Lex (α →₀ ℕ)) :
            Lex (ℕ × Lex (α →₀ ℕ))))
        f)
      ((fun (f : DegLex (α →₀ ℕ)) ↦
          ((toLex : (a : ℕ × Lex (α →₀ ℕ)) → Lex (ℕ × Lex (α →₀ ℕ)))
              (((degree : (a : α →₀ ℕ) → ℕ) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) f : α →₀ ℕ),
                  (toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) ((ofDegLex : (a : DegLex (α →₀ ℕ)) → α →₀ ℕ) f : α →₀ ℕ)) :
                ℕ × Lex (α →₀ ℕ)) :
            Lex (ℕ × Lex (α →₀ ℕ))))
        g) →
    f = g

Tactic:
simp