awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j : ℕ
rw : (∃ (b : ℕ) (a : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
⊢ (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
rw [exists_comm]

Premises used: exists_comm
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j a b : ℕ
rw rw₁ : a + b = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j
⊢ b + a = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j : ℕ
⊢ (∃ (b : ℕ) (a : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
exact exists₂_congr (fun a b ↦ by rw [add_comm])

Premises used: exists₂_congr
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
⊢ ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔
                      ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
rw :
  {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))

Tactic:
rw [← map_prodComm_antidiagonal]

Premises used: Finset.map_prodComm_antidiagonal
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
simp_rw :
  map
      (({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
        (Equiv.prodComm ℕ ℕ).toEmbedding)
      (@antidiagonal _ Nat.instAddMonoid _ (n - k)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))
⊢ {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))

Tactic:
simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h, map_map]

Premises used: Finset.map_filter, Finset.Nat.antidiagonal_filter_le_fst_of_le, Finset.map_map
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
h₁ :
  ∀ (i j : ℕ),
    (i, j) ∈
        map
          (({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
            (Equiv.prodComm ℕ ℕ).toEmbedding)
          (@antidiagonal _ Nat.instAddMonoid _ (n - k)) ↔
      (i, j) ∈
        map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
          (@antidiagonal _ Nat.instAddMonoid _ (n - k))
⊢ map
      (({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
        (Equiv.prodComm ℕ ℕ).toEmbedding)
      (@antidiagonal _ Nat.instAddMonoid _ (n - k)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))

Tactic:
ext ⟨i, j⟩
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
i j : ℕ
⊢ (i, j) ∈
      map
        (({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
          (Equiv.prodComm ℕ ℕ).toEmbedding)
        (@antidiagonal _ Nat.instAddMonoid _ (n - k)) ↔
    (i, j) ∈
      map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ (n - k))

Tactic:
simpa using aux₂ i j
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
x : Fin (n + 1)
i : ℕ
h : i < n + 1
rw : i ≤ n
⊢ (i, n - i) ∈ @antidiagonal _ Nat.instAddMonoid _ n

Tactic:
rw [mem_antidiagonal, add_comm, Nat.sub_add_cancel]

Premises used: add_comm, Finset.HasAntidiagonal.mem_antidiagonal, Nat.sub_add_cancel
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
x : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ i ≤ n

Tactic:
Nat.le_of_lt_succ h

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
x : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ i ≤ n

Tactic:
exact Nat.le_of_lt_succ h

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
a b : α →₀ N
⊢ Pi.Lex (β := fun {i : α} ↦ N) r (fun {i : α} ↦ s) (⇑a : (a : α) → N) (⇑b : (a : α) → N) = Finsupp.Lex r s a b

Tactic:
rfl

Premises used: Finsupp.Lex, rfl
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
a b : α →₀ N
⊢ Finsupp.Lex r s a b ↔
    ∃ (j : α),
      (∀ (d : α), r d j → Eq.{u_2 + 1} (α := N) ((a : (a : α) → N) d : N) ((b : (a : α) → N) d : N)) ∧
        s ((a : (a : α) → N) j) ((b : (a : α) → N) j)

Tactic:
.rfl

Premises used: Iff.rfl, Pi.Lex, Finsupp.Lex
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
⊢ Eq (α := (x y : α →₀ N) → Prop) (Finsupp.Lex r s)
    (InvImage (DFinsupp.Lex (α := fun (x : α) ↦ N) r fun (x : α) ↦ s) toDFinsupp)

Tactic:
rfl

Premises used: Pi.Lex, Finsupp.Lex, DFinsupp.Lex, rfl
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : LT α
inst_2 : LT N
a b : Lex (α →₀ N)
⊢ a < b ↔
    ∃ (i : α),
      (∀ j < i,
          Eq.{u_2 + 1} (α := N) ((((ofLex : (a : Lex (α →₀ N)) → α →₀ N) a : α →₀ N) : (a : α) → N) j : N)
            ((((ofLex : (a : Lex (α →₀ N)) → α →₀ N) b : α →₀ N) : (a : α) → N) j : N)) ∧
        LT.lt.{u_2} (α := N) ((((ofLex : (a : Lex (α →₀ N)) → α →₀ N) a : α →₀ N) : (a : α) → N) i : N)
          ((((ofLex : (a : Lex (α →₀ N)) → α →₀ N) b : α →₀ N) : (a : α) → N) i : N)

Tactic:
.rfl

Premises used: Iff.rfl, Pi.Lex, Finsupp.Lex
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : LT α
inst_2 : LT N
a b : Colex (α →₀ N)
⊢ a < b ↔
    ∃ (i : α),
      (∀ (j : α),
          i < j →
            Eq.{u_2 + 1} (α := N) ((((ofColex : (a : Colex (α →₀ N)) → α →₀ N) a : α →₀ N) : (a : α) → N) j : N)
              ((((ofColex : (a : Colex (α →₀ N)) → α →₀ N) b : α →₀ N) : (a : α) → N) j : N)) ∧
        LT.lt.{u_2} (α := N) ((((ofColex : (a : Colex (α →₀ N)) → α →₀ N) a : α →₀ N) : (a : α) → N) i : N)
          ((((ofColex : (a : Colex (α →₀ N)) → α →₀ N) b : α →₀ N) : (a : α) → N) i : N)

Tactic:
.rfl

Premises used: Iff.rfl, Pi.Lex, Finsupp.Lex
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : Preorder N
r : α → α → Prop
inst_2 : IsStrictOrder α r
x y : α →₀ N
hlt : x < y
⊢ ∃ (i : α),
    (∀ (j : α),
        r j i →
          LE.le.{u_2} (α := N) ((x : (a : α) → N) j : N) ((y : (a : α) → N) j : N) ∧
            LE.le.{u_2} (α := N) ((y : (a : α) → N) j : N) ((x : (a : α) → N) j : N)) ∧
      LT.lt.{u_2} (α := N) ((x : (a : α) → N) i : N) ((y : (a : α) → N) i : N)

Tactic:
DFinsupp.lex_lt_of_lt_of_preorder r (id hlt : x.toDFinsupp < y.toDFinsupp)

Premises used: DFinsupp.lex_lt_of_lt_of_preorder, id
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : PartialOrder N
r : α → α → Prop
inst_2 : IsStrictOrder α r
x y : α →₀ N
hlt : x < y
⊢ Pi.Lex (β := fun (a : α) ↦ N) r (fun {i : α} (x1 x2 : N) ↦ x1 < x2) (⇑x : (a : α) → N) (⇑y : (a : α) → N)

Tactic:
DFinsupp.lex_lt_of_lt r (id hlt : x.toDFinsupp < y.toDFinsupp)

Premises used: DFinsupp.lex_lt_of_lt, id
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : Unique α
inst_2 : LT N
r : α → α → Prop
inst_3 : Std.Irrefl r
x y : α →₀ N
⊢ Finsupp.Lex r (fun (x1 x2 : N) ↦ x1 < x2) x y ↔
    LT.lt.{u_2} (α := N) ((x : (a : α) → N) default : N) ((y : (a : α) → N) default : N)

Tactic:
Pi.lex_iff_of_unique

Premises used: Pi.lex_iff_of_unique, Finsupp.Lex
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : Unique α
inst_2 : LT N
inst_3 : Preorder α
x y : Lex (α →₀ N)
⊢ x < y ↔
    LT.lt.{u_2} (α := N) ((((ofLex : (a : Lex (α →₀ N)) → α →₀ N) x : α →₀ N) : (a : α) → N) default : N)
      ((((ofLex : (a : Lex (α →₀ N)) → α →₀ N) y : α →₀ N) : (a : α) → N) default : N)

Tactic:
lex_iff_of_unique

Premises used: Finsupp.lex_iff_of_unique
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : Unique α
inst_2 : LT N
inst_3 : Preorder α
x y : Colex (α →₀ N)
⊢ x < y ↔
    LT.lt.{u_2} (α := N) ((((ofColex : (a : Colex (α →₀ N)) → α →₀ N) x : α →₀ N) : (a : α) → N) default : N)
      ((((ofColex : (a : Colex (α →₀ N)) → α →₀ N) y : α →₀ N) : (a : α) → N) default : N)

Tactic:
Lex.lt_iff_of_unique (α := αᵒᵈ)

Premises used: OrderDual, Finsupp.Lex.lt_iff_of_unique
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : LinearOrder α
inst_2 : PartialOrder N
⊢ IsStrictOrder (Colex (α →₀ N)) fun (x1 x2 : Colex (α →₀ N)) ↦ x1 < x2

Tactic:
Lex.isStrictOrder (α := αᵒᵈ)

Premises used: Colex, Finsupp.Lex.isStrictOrder, OrderDual
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : LinearOrder α
inst_2 : Unique α
inst_3 : PartialOrder N
x y : Lex (α →₀ N)
⊢ x ≤ y ↔
    LE.le.{u_2} (α := N) ((((ofLex : (a : Lex (α →₀ N)) → α →₀ N) x : α →₀ N) : (a : α) → N) default : N)
      ((((ofLex : (a : Lex (α →₀ N)) → α →₀ N) y : α →₀ N) : (a : α) → N) default : N)

Tactic:
Pi.lex_le_iff_of_unique

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

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

Premises used: Finsupp.Lex.le_iff_of_unique, OrderDual
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
h₁ :
  (∀ d < a, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)) ∧
    LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)
⊢ ∃ (j : α),
    (∀ d < j, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)) ∧
      LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) j : ℕ) ((single a 1 : (a : α) → ℕ) j : ℕ)

Tactic:
use a
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
h₁ : ∀ d < a, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)
h₂ : LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)
⊢ (∀ d < a, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)) ∧
    LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
d : α
hd : d < a
⊢ Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)

Tactic:
simp only [Finsupp.single_eq_of_ne hd.ne, Finsupp.single_eq_of_ne (hd.trans h).ne]

Premises used: Finsupp.single_eq_of_ne, LT.lt.trans, LT.lt.ne
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)

Tactic:
simp [h.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
inst : LinearOrder α
⊢ StrictMono (β := Colex (α →₀ ℕ)) fun (a : α) ↦ (toColex : (a : α →₀ ℕ) → Colex (α →₀ ℕ)) (single a 1)

Tactic:
fun _ _ h ↦ Lex.single_strictAnti (α := αᵒᵈ) h

Premises used: StrictMono, Finsupp.Lex.single_strictAnti, OrderDual
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ LT.lt (α := Lex (α →₀ ℕ)) ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) (single b 1) : Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) (single a 1) : Lex (α →₀ ℕ)) ↔
    a < b

Tactic:
Lex.single_strictAnti.lt_iff_gt

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

Tactic:
Colex.single_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Finsupp.Colex.single_strictMono
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ LE.le (α := Lex (α →₀ ℕ)) ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) (single b 1) : Lex (α →₀ ℕ))
      ((toLex : (a : α →₀ ℕ) → Lex (α →₀ ℕ)) (single a 1) : Lex (α →₀ ℕ)) ↔
    a ≤ b

Tactic:
Lex.single_strictAnti.le_iff_ge

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

Tactic:
Colex.single_strictMono.le_iff_le

Premises used: StrictMono.le_iff_le, Finsupp.Colex.single_strictMono
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : LinearOrder α
inst_2 : PartialOrder N
⊢ Monotone (α := α →₀ N) (β := Lex (α →₀ N)) (⇑toLex : (a : α →₀ N) → Lex (α →₀ N))

Tactic:
fun a b h ↦ DFinsupp.toLex_monotone (id h : ∀ i, (toDFinsupp a) i ≤ (toDFinsupp b) i)

Premises used: DFinsupp.toLex_monotone, Monotone, id, Finsupp.Lex
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : LinearOrder α
inst_2 : PartialOrder N
⊢ Monotone (α := α →₀ N) (β := Colex (α →₀ N)) (⇑toColex : (a : α →₀ N) → Colex (α →₀ N))

Tactic:
toLex_monotone (α := αᵒᵈ)

Premises used: Colex, OrderDual, Finsupp.toLex_monotone
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddMonoid N
inst_2 : LinearOrder N
inst_3 : AddLeftStrictMono N
⊢ AddLeftStrictMono (Lex (α →₀ N))

Tactic:
⟨fun _ _ _ ⟨a, lta, ha⟩ ↦ ⟨a, fun j ja ↦ congr_arg _ (lta j ja), add_lt_add_right ha _⟩⟩

Premises used: CovariantClass.mk, add_lt_add_right, Add.add, congr_arg, _private.0.Finsupp.Lex.addLeftStrictMono.match_1, HAdd.hAdd, And.intro, LT.lt, Exists.intro, AddZero.toAdd, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddMonoid N
inst_2 : LinearOrder N
inst_3 : AddLeftStrictMono N
⊢ AddLeftStrictMono (Colex (α →₀ N))

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

Premises used: Colex, Finsupp.Lex.addLeftStrictMono, OrderDual
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddMonoid N
inst_2 : LinearOrder N
inst_3 : AddLeftStrictMono N
⊢ AddLeftMono (Lex (α →₀ N))

Tactic:
addLeftMono_of_addLeftStrictMono _

Premises used: addLeftMono_of_addLeftStrictMono
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddMonoid N
inst_2 : LinearOrder N
inst_3 : AddLeftStrictMono N
⊢ AddLeftMono (Colex (α →₀ N))

Tactic:
addLeftMono_of_addLeftStrictMono _

Premises used: addLeftMono_of_addLeftStrictMono
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddMonoid N
inst_2 : LinearOrder N
inst_3 : AddRightStrictMono N
⊢ AddRightStrictMono (Lex (α →₀ N))

Tactic:
⟨fun f _ _ ⟨a, lta, ha⟩ ↦ ⟨a, fun j ja ↦ congr($(lta j ja) + f j), add_lt_add_left ha _⟩⟩

Premises used: CovariantClass.mk, add_lt_add_left, congrArg, Function.swap, id, _private.0.Finsupp.Lex.addLeftStrictMono.match_1, HAdd.hAdd, And.intro, LT.lt, Exists.intro, ofLex, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddMonoid N
inst_2 : LinearOrder N
inst_3 : AddRightStrictMono N
⊢ AddRightStrictMono (Colex (α →₀ N))

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

Premises used: Colex, Finsupp.Lex.addRightStrictMono, OrderDual
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddMonoid N
inst_2 : LinearOrder N
inst_3 : AddRightStrictMono N
⊢ AddRightMono (Lex (α →₀ N))

Tactic:
addRightMono_of_addRightStrictMono _

Premises used: addRightMono_of_addRightStrictMono
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddMonoid N
inst_2 : LinearOrder N
inst_3 : AddRightStrictMono N
⊢ AddRightMono (Colex (α →₀ N))

Tactic:
addRightMono_of_addRightStrictMono _

Premises used: addRightMono_of_addRightStrictMono
-- Module: Mathlib.Data.Finsupp.Lex
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedCancelAddMonoid N
⊢ IsOrderedCancelAddMonoid (Colex (α →₀ N))

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

Premises used: Colex, Finsupp.Lex.isOrderedCancelAddMonoid, OrderDual
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a b : σ →₀ ℕ
rw :
  LE.le.{u_2} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (a + b) : m.syn)
⊢ (m.toSyn : (a : σ →₀ ℕ) → m.syn) a ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)

Tactic:
rw [← map_add]

Premises used: map_add
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a b : σ →₀ ℕ
⊢ LE.le.{u_2} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (a + b) : m.syn)

Tactic:
m.toSyn_monotone le_self_add

Premises used: MonomialOrder.toSyn_monotone, le_self_add
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a b : σ →₀ ℕ
⊢ LE.le.{u_2} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (a + b) : m.syn)

Tactic:
exact m.toSyn_monotone le_self_add

Premises used: MonomialOrder.toSyn_monotone, le_self_add
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a : m.syn
⊢ (m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) a) : m.syn)

Tactic:
have := m.le_add_right 0 (m.toSyn.symm a)
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a : m.syn
this :
  (m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) a) : m.syn)
⊢ 0 ≤ a

Tactic:
simpa [map_add, zero_add]

Premises used: map_add, zero_add
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
⊢ Eq.{u_2 + 1} (α := m.syn) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a : m.syn
⊢ 0 ≤ a

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a : m.syn
⊢ a = 0 ↔ a ≤ 0

Tactic:
eq_bot_iff

Premises used: eq_bot_iff
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn) (0 : m.syn) ↔ a = 0

Tactic:
AddEquiv.map_eq_zero_iff m.toSyn

Premises used: AddEquiv.map_eq_zero_iff, MonomialOrder.toSyn
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a : m.syn
⊢ 0 < a ↔ a ≠ 0

Tactic:
bot_lt_iff_ne_bot

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
⊢ StrictMono.{u_1, u_2} (α := σ →₀ ℕ) (β := m.syn) (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)

Tactic:
apply m.toSyn_monotone.strictMono_of_injective m.toSyn.injective

Premises used: MonomialOrder.toSyn_monotone, Monotone.strictMono_of_injective, AddEquiv.injective, MonomialOrder.toSyn
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedCancelAddMonoid N
a b : Lex (α →₀ N)
h : a ≤ b
c : Lex (α →₀ N)
⊢ a + c ≤ b + c

Tactic:
simpa using h
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
α : Type u_1
N : Type u_2
inst : LinearOrder α
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedCancelAddMonoid N
a b c : Lex (α →₀ N)
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
simpa only [add_le_add_iff_left] using h

Premises used: add_le_add_iff_left