awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : Unique ι
inst_3 : (i : ι) → PartialOrder (α i)
x y : Lex (Π₀ (i : ι), α i)
⊢ x ≤ y ↔
    LE.le (α := α default)
      ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) default)
      ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) y : Π₀ (i : ι), α i) : (a : ι) → α a) default)

Tactic:
Pi.lex_le_iff_of_unique

Premises used: Pi.lex_le_iff_of_unique, Lex, DFinsupp.Lex
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : Unique ι
inst_3 : (i : ι) → PartialOrder (α i)
x y : Colex (Π₀ (i : ι), α i)
⊢ x ≤ y ↔
    LE.le (α := α default)
      ((((ofColex : (a : Colex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) default)
      ((((ofColex : (a : Colex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) y : Π₀ (i : ι), α i) : (a : ι) → α a) default)

Tactic:
Lex.le_iff_of_unique (ι := ιᵒᵈ)

Premises used: DFinsupp.Lex.le_iff_of_unique, OrderDual
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_eq :
  {f g : Π₀ (i : ι), α i} →
    Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_gt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus (N := α) g).min = (↑wit : WithTop ι)
h₁ :
  (f : (a : ι) → α a) wit < (g : (a : ι) → α a) wit →
    P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
      ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h₂ :
  (g : (a : ι) → α a) wit < (f : (a : ι) → α a) wit →
    P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
      ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
⊢ P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)

Tactic:
apply (mem_neLocus.mp <| Finset.mem_of_min h).lt_or_gt.by_cases

Premises used: DFinsupp.mem_neLocus, Finset.mem_of_min, Or.by_cases, Iff.mp, Ne.lt_or_gt
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_eq :
  {f g : Π₀ (i : ι), α i} →
    Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_gt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus (N := α) g).min = (↑wit : WithTop ι)
hwit : (f : (a : ι) → α a) wit < (g : (a : ι) → α a) wit
⊢ P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)

Tactic:
exact h_lt ⟨wit, fun j hj ↦ notMem_neLocus.mp (Finset.notMem_of_lt_min hj h), hwit⟩

Premises used: Finset.notMem_of_lt_min, DFinsupp.notMem_neLocus, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_eq :
  {f g : Π₀ (i : ι), α i} →
    Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_gt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus (N := α) g).min = (↑wit : WithTop ι)
hwit : (g : (a : ι) → α a) wit < (f : (a : ι) → α a) wit
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j wit
rwa rwa₁ rwa₂ rwa₃ :
  Finset.min
      (neLocus (N := α)
        ((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
          ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f))
        ((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
          ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g))) =
    (↑wit : WithTop ι)
⊢ Finset.min
      (neLocus (N := α)
        ((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
          ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g))
        ((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
          ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f))) =
    (↑wit : WithTop ι)

Tactic:
rwa [neLocus_comm]

Premises used: DFinsupp.neLocus_comm
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_eq :
  {f g : Π₀ (i : ι), α i} →
    Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_gt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus (N := α) g).min = (↑wit : WithTop ι)
hwit : (g : (a : ι) → α a) wit < (f : (a : ι) → α a) wit
⊢ P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)

Tactic:
exact h_gt ⟨wit, fun j hj ↦
        notMem_neLocus.mp (Finset.notMem_of_lt_min hj <| by rwa [neLocus_comm]), hwit⟩

Premises used: Finset.notMem_of_lt_min, DFinsupp.notMem_neLocus, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → LinearOrder (α i)
⊢ Std.Total fun (x1 x2 : Colex (Π₀ (i : ι), α i)) ↦ x1 ≤ x2

Tactic:
Lex.total_le (ι := ιᵒᵈ)

Premises used: Colex, OrderDual, DFinsupp.Lex.total_le
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
⊢ LE.le (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))

Tactic:
le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ ?_)

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, le_of_lt_or_eq
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
refine :
  ∀
    (hne :
      ¬Eq (α := Lex (Π₀ (i : ι), α i))
          ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
          ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))),
    LT.lt (α := Lex (Π₀ (i : ι), α i))
      ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
      ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))
⊢ LE.le (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))

Tactic:
refine le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ ?_)

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, le_of_lt_or_eq
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne :
  ¬Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
      ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))
⊢ LT.lt (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))

Tactic:
⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
    fun j hj ↦ notMem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_gt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩

Premises used: Finset.min', Iff.mpr, DFinsupp.mem_neLocus, Finset.min'_le, Finset.min'_mem, Pi.Lex, DFinsupp.notMem_neLocus, LE.le.lt_of_ne, LE.le.not_gt, DFinsupp.nonempty_neLocus_iff, And.intro, DFinsupp.neLocus, Exists.intro, Iff.mp, ofLex, DFunLike.coe, toLex
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne :
  ¬Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
      ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))
⊢ LT.lt (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))

Tactic:
exact ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
    fun j hj ↦ notMem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_gt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne :
  ¬Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
      ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))
⊢ LT.lt (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))

Tactic:
classical
  exact ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
    fun j hj ↦ notMem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_gt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (α i)
⊢ Monotone (α := Π₀ (i : ι), α i) (β := Colex (Π₀ (i : ι), α i))
    (⇑toColex : (a : Π₀ (i : ι), α i) → Colex (Π₀ (i : ι), α i))

Tactic:
toLex_monotone (ι := ιᵒᵈ)

Premises used: DFinsupp.toLex_monotone, Colex, OrderDual
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddLeftStrictMono.{u_2} (α i)
x x_1 x_2 : Lex (Π₀ (i : ι), α i)
h : x_1 < x_2
a : ι
lta :
  ∀ (j : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j a →
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) j =
        (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) j
ha :
  (fun {i : ι} ↦ ((fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) i : α i → α i → Prop))
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
dsimp :
  (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a <
    (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) a
⊢ (fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) a
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) (x + x_1) : Π₀ (i : ι), α i) : (a : ι) → α a) a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) (x + x_2) : Π₀ (i : ι), α i) : (a : ι) → α a) a)

Tactic:
dsimp
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddLeftStrictMono.{u_2} (α i)
x x_1 x_2 : Lex (Π₀ (i : ι), α i)
h : x_1 < x_2
a : ι
lta :
  ∀ (j : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j a →
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) j =
        (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) j
ha :
  (fun {i : ι} ↦ ((fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) i : α i → α i → Prop))
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
⊢ (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a <
    (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) a

Tactic:
gcongr
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddLeftStrictMono.{u_2} (α i)
⊢ AddLeftStrictMono (Colex (Π₀ (i : ι), α i))

Tactic:
Lex.addLeftStrictMono (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.addLeftStrictMono, OrderDual
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddLeftStrictMono.{u_2} (α i)
⊢ AddLeftMono (Lex (Π₀ (i : ι), α i))

Tactic:
addLeftMono_of_addLeftStrictMono _

Premises used: Lex, addLeftMono_of_addLeftStrictMono
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddLeftStrictMono.{u_2} (α i)
⊢ AddLeftMono (Colex (Π₀ (i : ι), α i))

Tactic:
Lex.addLeftMono (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.addLeftMono, OrderDual
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddRightStrictMono.{u_2} (α i)
f x x_1 : Lex (Π₀ (i : ι), α i)
h : x < x_1
a : ι
lta :
  ∀ (j : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j a →
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) j =
        (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) j
ha :
  (fun {i : ι} ↦ ((fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) i : α i → α i → Prop))
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
dsimp :
  (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) f : Π₀ (i : ι), α i) : (a : ι) → α a) a <
    (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a +
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) f : Π₀ (i : ι), α i) : (a : ι) → α a) a
⊢ (fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) a
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
            (Function.swap (φ := fun (a a_1 : Lex (Π₀ (i : ι), α i)) ↦ Lex (Π₀ (i : ι), α i))
              (fun (x1 x2 : Lex (Π₀ (i : ι), α i)) ↦ x1 + x2) f x) :
          Π₀ (i : ι), α i) :
        (a : ι) → α a)
      a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
            (Function.swap (φ := fun (a a_1 : Lex (Π₀ (i : ι), α i)) ↦ Lex (Π₀ (i : ι), α i))
              (fun (x1 x2 : Lex (Π₀ (i : ι), α i)) ↦ x1 + x2) f x_1) :
          Π₀ (i : ι), α i) :
        (a : ι) → α a)
      a)

Tactic:
dsimp
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddRightStrictMono.{u_2} (α i)
f x x_1 : Lex (Π₀ (i : ι), α i)
h : x < x_1
a : ι
lta :
  ∀ (j : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j a →
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) j =
        (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) j
ha :
  (fun {i : ι} ↦ ((fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) i : α i → α i → Prop))
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
⊢ (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) f : Π₀ (i : ι), α i) : (a : ι) → α a) a <
    (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a +
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) f : Π₀ (i : ι), α i) : (a : ι) → α a) a

Tactic:
gcongr
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddRightStrictMono.{u_2} (α i)
⊢ AddRightStrictMono (Colex (Π₀ (i : ι), α i))

Tactic:
Lex.addRightStrictMono (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.addRightStrictMono, OrderDual
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddRightStrictMono.{u_2} (α i)
⊢ AddRightMono (Lex (Π₀ (i : ι), α i))

Tactic:
addRightMono_of_addRightStrictMono _

Premises used: Lex, addRightMono_of_addRightStrictMono
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddRightStrictMono.{u_2} (α i)
⊢ AddRightMono (Colex (Π₀ (i : ι), α i))

Tactic:
Lex.addRightMono (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.addRightMono, OrderDual
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddCommMonoid (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : ∀ (i : ι), IsOrderedCancelAddMonoid.{u_2} (α i)
⊢ IsOrderedCancelAddMonoid (Colex (Π₀ (i : ι), α i))

Tactic:
Lex.isOrderedCancelAddMonoid (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.isOrderedCancelAddMonoid, OrderDual
-- Module: Mathlib.Data.DFinsupp.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddCommGroup (α i)
inst_2 : (i : ι) → PartialOrder (α i)
inst_3 : ∀ (i : ι), IsOrderedAddMonoid.{u_2} (α i)
⊢ IsOrderedAddMonoid (Colex (Π₀ (i : ι), α i))

Tactic:
Lex.isOrderedAddMonoid (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.isOrderedAddMonoid, OrderDual
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
b : γ
v : Π₀ (i : ι), β i
i : ι
⊢ (b • v : (a : ι) → β a) i = b • (v : (a : ι) → β a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
b : γ
v : Π₀ (i : ι), β i
⊢ (⇑(b • v) : (a : ι) → β a) = b • (⇑v : (a : ι) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
δ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
inst_2 : (i : ι) → SMulZeroClass.{u_1, v} δ (β i)
inst_3 : ∀ (i : ι), SMulCommClass.{w, u_1, v} γ δ (β i)
r : γ
s : δ
m : Π₀ (i : ι), β i
i : ι
⊢ (r • s • m : (a : ι) → β a) i = (s • r • m : (a : ι) → β a) i

Tactic:
simp only [smul_apply, smul_comm r s (m i)]

Premises used: DFinsupp.smul_apply, SMulCommClass.smul_comm, DFunLike.coe