awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
h :
  (∀ (j : ℕ),
      (fun (x1 x2 : ℕ) ↦ x1 < x2) j 0 →
        Eq (α := (@fun {i : ℕ} ↦ ℕ) j)
          ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ)
                    ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (HAdd.hAdd (α := ℕ →₀ ℕ) (single 0 1) (single 1 1))) :
                  ℕ →₀ ℕ) :
                (a : ℕ) → ℕ)
              j :
            ℕ)
          ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2)) : ℕ →₀ ℕ) :
                (a : ℕ) → ℕ)
              j :
            ℕ)) ∧
    (@fun {i : ℕ} (x1 x2 : ℕ) ↦ x1 < x2) 0
      ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ)
              ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (HAdd.hAdd (α := ℕ →₀ ℕ) (single 0 1) (single 1 1))) :
            ℕ →₀ ℕ) :
          (a : ℕ) → ℕ)
        0)
      ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2)) : ℕ →₀ ℕ) :
          (a : ℕ) → ℕ)
        0)
⊢ GT.gt (α := Lex (ℕ →₀ ℕ)) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2) : Lex (ℕ →₀ ℕ))
    ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (HAdd.hAdd (α := ℕ →₀ ℕ) (single 0 1) (single 1 1)) : Lex (ℕ →₀ ℕ))

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

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
h :
  (∀ (j : ℕ),
      (fun (x1 x2 : ℕ) ↦ x1 < x2) j 0 →
        Eq (α := (@fun {i : ℕ} ↦ ℕ) j)
          ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1)) : ℕ →₀ ℕ) :
                (a : ℕ) → ℕ)
              j :
            ℕ)
          ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 1)) : ℕ →₀ ℕ) :
                (a : ℕ) → ℕ)
              j :
            ℕ)) ∧
    (@fun {i : ℕ} (x1 x2 : ℕ) ↦ x1 < x2) 0
      ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1)) : ℕ →₀ ℕ) :
          (a : ℕ) → ℕ)
        0)
      ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 1)) : ℕ →₀ ℕ) :
          (a : ℕ) → ℕ)
        0)
⊢ LT.lt (α := Lex (ℕ →₀ ℕ)) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1) : Lex (ℕ →₀ ℕ))
    ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 1) : Lex (ℕ →₀ ℕ))

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

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
h :
  (∀ (j : ℕ),
      (fun (x1 x2 : ℕ) ↦ x1 < x2) j 0 →
        Eq (α := (@fun {i : ℕ} ↦ ℕ) j)
          ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1)) : ℕ →₀ ℕ) :
                (a : ℕ) → ℕ)
              j :
            ℕ)
          ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2)) : ℕ →₀ ℕ) :
                (a : ℕ) → ℕ)
              j :
            ℕ)) ∧
    (@fun {i : ℕ} (x1 x2 : ℕ) ↦ x1 < x2) 0
      ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1)) : ℕ →₀ ℕ) :
          (a : ℕ) → ℕ)
        0)
      ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2)) : ℕ →₀ ℕ) :
          (a : ℕ) → ℕ)
        0)
⊢ LT.lt (α := Lex (ℕ →₀ ℕ)) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1) : Lex (ℕ →₀ ℕ))
    ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2) : Lex (ℕ →₀ ℕ))

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

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
c d : σ →₀ ℕ
⊢ LE.le (α := syn (σ := σ) lex) ((toSyn lex : (a : σ →₀ ℕ) → lex.syn) c : syn (σ := σ) lex)
      ((toSyn lex : (a : σ →₀ ℕ) → lex.syn) d : syn (σ := σ) lex) ↔
    LE.le (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) c : Lex (σ →₀ ℕ))
      ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d : Lex (σ →₀ ℕ))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
inst : LinearOrder σ
inst_1 : WellFoundedGT σ
c d : σ →₀ ℕ
⊢ LT.lt (α := syn (σ := σ) lex) ((toSyn lex : (a : σ →₀ ℕ) → lex.syn) c : syn (σ := σ) lex)
      ((toSyn lex : (a : σ →₀ ℕ) → lex.syn) d : syn (σ := σ) lex) ↔
    LT.lt (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) c : Lex (σ →₀ ℕ))
      ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d : Lex (σ →₀ ℕ))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
inst : LinearOrder σ
inst_1 : Unique σ
c d : σ →₀ ℕ
⊢ LT.lt (α := syn (σ := σ) lex) ((toSyn lex : (a : σ →₀ ℕ) → lex.syn) c : syn (σ := σ) lex)
      ((toSyn lex : (a : σ →₀ ℕ) → lex.syn) d : syn (σ := σ) lex) ↔
    LT.lt (α := ℕ) ((c : (a : σ) → ℕ) default : ℕ) ((d : (a : σ) → ℕ) default : ℕ)

Tactic:
simp only [MonomialOrder.lex_lt_iff, Finsupp.Lex.lt_iff_of_unique, ofLex_toLex]

Premises used: ofLex_toLex, MonomialOrder.lex_lt_iff, Finsupp.Lex.lt_iff_of_unique
-- Module: Mathlib.Data.Finsupp.MonomialOrder
Goal:
σ : Type u_1
inst : LinearOrder σ
inst_1 : Unique σ
c d : σ →₀ ℕ
⊢ LE.le (α := syn (σ := σ) lex) ((toSyn lex : (a : σ →₀ ℕ) → lex.syn) c : syn (σ := σ) lex)
      ((toSyn lex : (a : σ →₀ ℕ) → lex.syn) d : syn (σ := σ) lex) ↔
    LE.le (α := ℕ) ((c : (a : σ) → ℕ) default : ℕ) ((d : (a : σ) → ℕ) default : ℕ)

Tactic:
simp only [MonomialOrder.lex_le_iff, Finsupp.Lex.le_iff_of_unique, ofLex_toLex]

Premises used: ofLex_toLex, Finsupp.Lex.le_iff_of_unique, MonomialOrder.lex_le_iff
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
a : α
⊢ a ∈ f.neLocus g ↔ Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((g : (a : α) → N) a : N)

Tactic:
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
    and_iff_right_iff_imp] using Ne.ne_or_ne _

Premises used: Finsupp.mem_support_iff, Finsupp.neLocus, and_iff_right_iff_imp, Finset.mem_filter, Finset.mem_union, Ne.ne_or_ne
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
a : α
⊢ a ∉ f.neLocus g ↔ Eq.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((g : (a : α) → N) a : N)

Tactic:
mem_neLocus.not.trans not_ne_iff

Premises used: Finsupp.mem_neLocus, Iff.not, not_ne_iff, Iff.trans
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
h :
  ∀ (x : α),
    x ∈ (↑(f.neLocus g) : Set α) ↔
      Membership.mem (γ := Set α) {x : α | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} x
⊢ (↑(f.neLocus g) : Set α) = {x : α | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)}

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
x : α
⊢ x ∈ (↑(f.neLocus g) : Set α) ↔
    Membership.mem (γ := Set α) {x : α | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} x

Tactic:
mem_neLocus

Premises used: Set.Mem, setOf, Finsupp.mem_neLocus, Not
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
x : α
⊢ x ∈ (↑(f.neLocus g) : Set α) ↔
    Membership.mem (γ := Set α) {x : α | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} x

Tactic:
exact mem_neLocus

Premises used: Finsupp.mem_neLocus
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
h : f = g
⊢ f.neLocus f = ∅

Tactic:
simp only [neLocus, Ne, not_true, Finset.filter_false]

Premises used: Finset.filter_false, Finsupp.neLocus, Ne, not_true
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
⊢ (f.neLocus g).Nonempty ↔ f ≠ g

Tactic:
Finset.nonempty_iff_ne_empty.trans neLocus_eq_empty.not

Premises used: Iff.not, Finset.nonempty_iff_ne_empty, Iff.trans, Finsupp.neLocus_eq_empty
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
simp_rw :
  {x ∈ f.support ∪ g.support | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} =
    {x ∈ g.support ∪ f.support | Ne.{u_3 + 1} (α := N) ((g : (a : α) → N) x : N) ((f : (a : α) → N) x : N)}
simp_rw₁ :
  {x ∈ f.support ∪ g.support | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} =
    {x ∈ f.support ∪ g.support | Ne.{u_3 + 1} (α := N) ((g : (a : α) → N) x : N) ((f : (a : α) → N) x : N)}
⊢ f.neLocus g = g.neLocus f

Tactic:
simp_rw [neLocus, Finset.union_comm, ne_comm]

Premises used: Finset.union_comm, Finsupp.neLocus, ne_comm
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f : α →₀ N
h : ∀ (a : α), a ∈ f.neLocus 0 ↔ a ∈ f.support
⊢ f.neLocus 0 = f.support

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f : α →₀ N
a : α
h : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔ a ∈ f.support
h₁ :
  Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔
    Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
h₂ : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 a : N) ↔ Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
h₃ h₄ :
  Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N) ↔ Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
⊢ a ∈ f.neLocus 0 ↔ a ∈ f.support

Tactic:
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]

Premises used: Finsupp.mem_support_iff, Finsupp.mem_neLocus, Pi.zero_apply, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f : α →₀ N
⊢ neLocus 0 f = f.support

Tactic:
(neLocus_comm _ _).trans (neLocus_zero_right _)

Premises used: Finsupp.neLocus_zero_right, Finsupp.neLocus_comm, Eq.trans
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
inst_3 : DecidableEq M
inst_4 : Zero M
f g : α →₀ N
F : N → M
F0 : F 0 = 0
x : α
⊢ x ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → x ∈ f.neLocus g

Tactic:
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F

Premises used: Finsupp.mapRange_apply, Finsupp.mem_neLocus, congr_arg, not_imp_not
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero M
inst_3 : DecidableEq P
inst_4 : Zero P
inst_5 : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective.{u_3 + 1, u_4 + 1} (β := P) fun (g : N) ↦ F f g
h : ∀ (a : α), a ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a ∈ g₁.neLocus g₂
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero M
inst_3 : DecidableEq P
inst_4 : Zero P
inst_5 : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective.{u_3 + 1, u_4 + 1} (β := P) fun (g : N) ↦ F f g
a : α
⊢ a ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a ∈ g₁.neLocus g₂

Tactic:
simpa only [mem_neLocus] using (hF _).ne_iff

Premises used: Finsupp.mem_neLocus, Function.Injective.ne_iff
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : DecidableEq α
inst_1 : DecidableEq M
inst_2 : Zero M
inst_3 : DecidableEq P
inst_4 : Zero P
inst_5 : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective.{u_2 + 1, u_4 + 1} (β := P) fun (f : M) ↦ F f g
h : ∀ (a : α), a ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a ∈ f₁.neLocus f₂
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : DecidableEq α
inst_1 : DecidableEq M
inst_2 : Zero M
inst_3 : DecidableEq P
inst_4 : Zero P
inst_5 : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective.{u_2 + 1, u_4 + 1} (β := P) fun (f : M) ↦ F f g
a : α
⊢ a ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a ∈ f₁.neLocus f₂

Tactic:
simpa only [mem_neLocus] using (hF _).ne_iff

Premises used: Finsupp.mem_neLocus, Function.Injective.ne_iff
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : DecidableEq M
inst_3 : Zero M
inst_4 : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
h : ∀ (a : α), a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a ∈ f.neLocus g
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : DecidableEq M
inst_3 : Zero M
inst_4 : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
a : α
⊢ a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a ∈ f.neLocus g

Tactic:
simpa only [mem_neLocus] using hF.ne_iff

Premises used: Finsupp.mem_neLocus, Function.Injective.ne_iff
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddLeftCancelMonoid N
f g h : α →₀ N
⊢ (f + g).neLocus (f + h) = g.neLocus h

Tactic:
zipWith_neLocus_eq_left _ _ _ _ add_right_injective

Premises used: add_right_injective, Finsupp.zipWith_neLocus_eq_left
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddRightCancelMonoid N
f g h : α →₀ N
⊢ (f + h).neLocus (g + h) = f.neLocus g

Tactic:
zipWith_neLocus_eq_right _ _ _ _ add_left_injective

Premises used: Finsupp.zipWith_neLocus_eq_right, add_left_injective
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
⊢ (-f).neLocus (-g) = f.neLocus g

Tactic:
mapRange_neLocus_eq _ _ neg_zero neg_injective

Premises used: neg_injective, Finsupp.mapRange_neLocus_eq, neg_zero
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : (- -f).neLocus (-g) = f.neLocus (-g)
rw₁ rw₂ : f.neLocus (-g) = f.neLocus (-g)
⊢ (-f).neLocus g = f.neLocus (-g)

Tactic:
rw [← neLocus_neg_neg, neg_neg]

Premises used: Finsupp.neLocus_neg_neg, neg_neg
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : (f + -g).neLocus (g + -g) = (f - g).support
rw₁ : (f + -g).neLocus 0 = (f - g).support
rw₂ : (f + -g).support = (f - g).support
rw₃ rw₄ : (f + -g).support = (f + -g).support
⊢ f.neLocus g = (f - g).support

Tactic:
rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]

Premises used: add_neg_cancel, sub_eq_add_neg, Finsupp.neLocus_add_right, Finsupp.neLocus_zero_right, Neg.neg
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g₁ g₂ : α →₀ N
⊢ (f - g₁).neLocus (f - g₂) = g₁.neLocus g₂

Tactic:
simp only [sub_eq_add_neg, neLocus_add_left, neLocus_neg_neg]

Premises used: Finsupp.neLocus_neg_neg, Finsupp.neLocus_add_left, sub_eq_add_neg
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f₁ f₂ g : α →₀ N
⊢ (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂

Tactic:
simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _

Premises used: sub_eq_add_neg, Finsupp.neLocus_add_right
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f + g) = neLocus 0 g
rw₁ : f.neLocus (f + g) = (f + 0).neLocus (f + g)
rw₂ rw₃ : f.neLocus (f + g) = f.neLocus (f + g)
⊢ f.neLocus (f + g) = g.support

Tactic:
rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]

Premises used: Finsupp.neLocus_add_left, Finsupp.neLocus_zero_left, add_zero, OfNat.ofNat
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f + g) = g.support
rw₁ rw₂ : g.support = g.support
⊢ (f + g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_add_right]

Premises used: Finsupp.neLocus_comm, Finsupp.neLocus_self_add_right
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f + -g) = g.support
rw₁ : (-g).support = g.support
rw₂ rw₃ : g.support = g.support
⊢ f.neLocus (f - g) = g.support

Tactic:
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]

Premises used: sub_eq_add_neg, Finsupp.support_neg, Finsupp.neLocus_self_add_right
-- Module: Mathlib.Data.Finsupp.NeLocus
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : f.neLocus (f - g) = g.support
rw₁ rw₂ : g.support = g.support
⊢ (f - g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_sub_right]

Premises used: Finsupp.neLocus_comm, Finsupp.neLocus_self_sub_right
-- Module: Mathlib.Data.Int.Lemmas
Goal:
m n : ℕ
⊢ HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ) ≤ (↑(m - n) : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Int.Lemmas
Goal:
n : ℕ
⊢ LE.le (α := ℤ) 0 (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
rw : a.natAbs = b.natAbs ↔ a * a = b * b
⊢ a.natAbs = b.natAbs ↔ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2

Tactic:
rw [sq, sq]

Premises used: sq
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b

Tactic:
natAbs_eq_iff_mul_self_eq

Premises used: Int.natAbs_eq_iff_mul_self_eq
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b

Tactic:
exact natAbs_eq_iff_mul_self_eq

Premises used: Int.natAbs_eq_iff_mul_self_eq
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
rw : a.natAbs < b.natAbs ↔ a * a < b * b
⊢ a.natAbs < b.natAbs ↔ HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2

Tactic:
rw [sq, sq]

Premises used: sq
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
natAbs_lt_iff_mul_self_lt

Premises used: Int.natAbs_lt_iff_mul_self_lt
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
exact natAbs_lt_iff_mul_self_lt

Premises used: Int.natAbs_lt_iff_mul_self_lt
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
rw : a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
⊢ a.natAbs ≤ b.natAbs ↔ HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2

Tactic:
rw [sq, sq]

Premises used: sq
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
natAbs_le_iff_mul_self_le

Premises used: Int.natAbs_le_iff_mul_self_le
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
exact natAbs_le_iff_mul_self_le

Premises used: Int.natAbs_le_iff_mul_self_le
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
rw : a.natAbs = b.natAbs ↔ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
rw₁ rw₂ : a.natAbs = b.natAbs ↔ a.natAbs = b.natAbs
⊢ a.natAbs = b.natAbs ↔ a = b

Tactic:
rw [← sq_eq_sq₀ ha hb, ← natAbs_eq_iff_sq_eq]

Premises used: Int.natAbs_eq_iff_sq_eq, sq_eq_sq₀
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = b

Tactic:
simpa only [Int.natAbs_neg, neg_inj] using
    natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) (neg_nonneg_of_nonpos hb)

Premises used: Int.natAbs_inj_of_nonneg_of_nonneg, neg_nonneg_of_nonpos, neg_inj, Int.natAbs_neg
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = -b

Tactic:
simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg ha (neg_nonneg_of_nonpos hb)

Premises used: Int.natAbs_inj_of_nonneg_of_nonneg, neg_nonneg_of_nonpos, Int.natAbs_neg
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ -a = b

Tactic:
simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) hb

Premises used: Int.natAbs_inj_of_nonneg_of_nonneg, neg_nonneg_of_nonpos, Int.natAbs_neg
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
rw : |HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)| ≤ (↑n : ℤ)
⊢ (HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)).natAbs ≤ n

Tactic:
rw [← Nat.cast_le (α := ℤ), natCast_natAbs]

Premises used: Nat.cast_le, Int.natCast_natAbs
-- Module: Mathlib.Data.Int.Lemmas
Goal:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)| ≤ (↑n : ℤ)

Tactic:
abs_sub_le_of_nonneg_of_le (natCast_nonneg a) (ofNat_le.mpr a_le_n)
    (natCast_nonneg b) (ofNat_le.mpr b_le_n)

Premises used: Iff.mpr, Int.ofNat_le, abs_sub_le_of_nonneg_of_le, Int.natCast_nonneg