awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : Π₀ (_a : α), ℕ
simp_rw :
  LT.lt (α := Π₀ (x : α), ℕ)
      ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f) :
        Π₀ (x : α), ℕ)
      ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g) :
        Π₀ (x : α), ℕ) ↔
    f < g
⊢ LT.lt (α := Multiset α) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f : Multiset α)
      ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g : Multiset α) ↔
    f < g

Tactic:
simp_rw [← Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_toDFinsupp]

Premises used: DFinsupp.toMultiset_toDFinsupp, Multiset.toDFinsupp_lt_toDFinsupp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Eq (α := Π₀ (x : α), ℕ)
    ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ)
        ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) (f ⊓ g)) :
      Π₀ (x : α), ℕ)
    ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ)
        ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f ∩ (toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g) :
      Π₀ (x : α), ℕ)

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Eq (α := Π₀ (x : α), ℕ)
    ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ)
        ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) (f ⊔ g)) :
      Π₀ (x : α), ℕ)
    ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ)
        ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f ∪ (toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g) :
      Π₀ (x : α), ℕ)

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.NeLocus
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a : α
⊢ a ∈ f.neLocus (N := N) g ↔ (f : (a : α) → N a) a ≠ (g : (a : α) → N a) a

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: DFinsupp.mem_support_iff, and_iff_right_iff_imp, DFinsupp.neLocus, Finset.mem_filter, Finset.mem_union, Ne.ne_or_ne
-- Module: Mathlib.Data.DFinsupp.NeLocus
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a : α
⊢ a ∉ f.neLocus (N := N) g ↔ (f : (a : α) → N a) a = (g : (a : α) → N a) a

Tactic:
mem_neLocus.not.trans not_ne_iff

Premises used: DFinsupp.mem_neLocus, Iff.not, not_ne_iff, Iff.trans
-- Module: Mathlib.Data.DFinsupp.NeLocus
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
⊢ (↑(f.neLocus (N := N) g) : Set α) = {x : α | (f : (a : α) → N a) x ≠ (g : (a : α) → N a) x}

Tactic:
Set.ext fun _x ↦ mem_neLocus

Premises used: Set.ext, DFinsupp.mem_neLocus
-- Module: Mathlib.Data.DFinsupp.NeLocus
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
h : f = g
⊢ f.neLocus (N := N) f = ∅

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

Premises used: Finset.filter_false, Ne, DFinsupp.neLocus, not_true
-- Module: Mathlib.Data.DFinsupp.NeLocus
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
⊢ (f.neLocus (N := N) 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, DFinsupp.neLocus_eq_empty
-- Module: Mathlib.Data.DFinsupp.NeLocus
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
simp_rw :
  {x ∈ f.support (β := N) ∪ g.support (β := N) | (f : (a : α) → N a) x ≠ (g : (a : α) → N a) x} =
    {x ∈ g.support (β := N) ∪ f.support (β := N) | (g : (a : α) → N a) x ≠ (f : (a : α) → N a) x}
simp_rw₁ :
  {x ∈ f.support (β := N) ∪ g.support (β := N) | (f : (a : α) → N a) x ≠ (g : (a : α) → N a) x} =
    {x ∈ f.support (β := N) ∪ g.support (β := N) | (g : (a : α) → N a) x ≠ (f : (a : α) → N a) x}
⊢ f.neLocus (N := N) g = g.neLocus (N := N) f

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

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

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.NeLocus
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a : α
h : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ a ∈ f.support (β := N)
h₁ : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ (f : (a : α) → N a) a ≠ 0
h₂ : (f : (a : α) → N a) a ≠ 0 a ↔ (f : (a : α) → N a) a ≠ 0
h₃ h₄ : (f : (a : α) → N a) a ≠ 0 ↔ (f : (a : α) → N a) a ≠ 0
⊢ a ∈ f.neLocus (N := N) 0 ↔ a ∈ f.support (β := N)

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

Premises used: DFinsupp.mem_neLocus, Pi.zero_apply, DFinsupp.mem_support_iff, DFinsupp.coe_zero
-- Module: Mathlib.Data.DFinsupp.NeLocus
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
⊢ neLocus (N := N) 0 f = f.support (β := N)

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
zipWith_neLocus_eq_left _ _ _ _ fun _a ↦ add_right_injective

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

Tactic:
zipWith_neLocus_eq_right _ _ _ _ fun _a ↦ add_left_injective

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

Tactic:
mapRange_neLocus_eq _ _ (fun _a ↦ neg_zero) fun _a ↦ neg_injective

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

Tactic:
rw [← neLocus_neg_neg, neg_neg]

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

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

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

Tactic:
simp only [sub_eq_add_neg, @neLocus_add_left α N _ _ _, neLocus_neg_neg]

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

Tactic:
simpa only [sub_eq_add_neg] using @neLocus_add_right α N _ _ _ _ _ _

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

Tactic:
rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]

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

Tactic:
rw [neLocus_comm, neLocus_self_add_right]

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

Tactic:
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]

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

Tactic:
rw [neLocus_comm, neLocus_self_sub_right]

Premises used: DFinsupp.neLocus_comm, DFinsupp.neLocus_self_sub_right
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → LE (α i)
f g : Π₀ (i : ι), α i
⊢ f ≤ g ↔ ∀ (i : ι), (f : (a : ι) → α a) i ≤ (g : (a : ι) → α a) i

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → LE (α i)
f g : Π₀ (i : ι), α i
⊢ (⇑f : (a : ι) → α a) ≤ (⇑g : (a : ι) → α a) ↔ f ≤ g

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → LE (α i)
⊢ Eq (α := (a : Π₀ (i : ι), α i) → (i : ι) → α i)
    (⇑(orderEmbeddingToFun (α := α)) : (a : Π₀ (i : ι), α i) → (i : ι) → α i) (DFunLike.coe (β := α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → LE (α i)
f : Π₀ (i : ι), α i
i : ι
⊢ (orderEmbeddingToFun (α := α) : (a : Π₀ (i : ι), α i) → (i : ι) → α i) f i = (f : (a : ι) → α a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
f g : Π₀ (i : ι), α i
⊢ f < g ↔ f ≤ g ∧ ∃ (i : ι), (f : (a : ι) → α a) i < (g : (a : ι) → α a) i

Tactic:
Pi.lt_def

Premises used: Pi.lt_def
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
f g : Π₀ (i : ι), α i
⊢ (⇑f : (a : ι) → α a) < (⇑g : (a : ι) → α a) ↔ f < g

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
⊢ Monotone (α := Π₀ (i : ι), α i) (DFunLike.coe (β := α))

Tactic:
fun _ _ ↦ id

Premises used: Monotone, id
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
i : ι
a b : α i
inst_2 : DecidableEq ι
⊢ LE.le (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) ↔ a ≤ b

Tactic:
Pi.single_le_single

Premises used: Function.update, Pi.single, dite, Pi.single_le_single
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
i : ι
inst_2 : DecidableEq ι
⊢ Monotone (α := α i) (β := Π₀ (i : ι), α i) (single (β := α) i)

Tactic:
fun _ _ ↦ single_le_single.2

Premises used: Iff.mpr, Monotone, DFinsupp.single_le_single
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
i : ι
a : α i
inst_2 : DecidableEq ι
⊢ LE.le (α := Π₀ (i : ι), α i) 0 (single (β := α) i a) ↔ 0 ≤ a

Tactic:
Pi.single_nonneg

Premises used: Function.update, Pi.single, dite, Pi.single_nonneg
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
i : ι
a : α i
inst_2 : DecidableEq ι
⊢ LE.le (α := Π₀ (i : ι), α i) (single (β := α) i a) 0 ↔ a ≤ 0

Tactic:
Pi.single_nonpos

Premises used: Function.update, Pi.single_nonpos, Pi.single, dite
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → SemilatticeInf (α i)
f g : Π₀ (i : ι), α i
⊢ (⇑(f ⊓ g) : (a : ι) → α a) = (⇑f : (a : ι) → α a) ⊓ (⇑g : (a : ι) → α a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → SemilatticeInf (α i)
f g : Π₀ (i : ι), α i
i : ι
⊢ (f ⊓ g : (a : ι) → α a) i = (f : (a : ι) → α a) i ⊓ (g : (a : ι) → α a) i

Tactic:
zipWith_apply _ _ _ _ _

Premises used: DFinsupp.zipWith_apply
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → SemilatticeSup (α i)
f g : Π₀ (i : ι), α i
⊢ (⇑(f ⊔ g) : (a : ι) → α a) = (⇑f : (a : ι) → α a) ⊔ (⇑g : (a : ι) → α a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → SemilatticeSup (α i)
f g : Π₀ (i : ι), α i
i : ι
⊢ (f ⊔ g : (a : ι) → α a) i = (f : (a : ι) → α a) i ⊔ (g : (a : ι) → α a) i

Tactic:
zipWith_apply _ _ _ _ _

Premises used: DFinsupp.zipWith_apply
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst_2 : DecidableEq ι
inst_3 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
h :
  ∀ (x : ι),
    x ∈ (↑((f ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α)) : Set ι)ᶜ ↔
      x ∈ (↑(f.support (β := α) ∪ g.support (β := α)) : Set ι)ᶜ
⊢ (↑((f ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α)) : Set ι)ᶜ =
    (↑(f.support (β := α) ∪ g.support (β := α)) : Set ι)ᶜ

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst_2 : DecidableEq ι
inst_3 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : ι
⊢ x ∈ (↑((f ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α)) : Set ι)ᶜ ↔
    x ∈ (↑(f.support (β := α) ∪ g.support (β := α)) : Set ι)ᶜ

Tactic:
simp [inf_eq_and_sup_eq_iff]

Premises used: inf_eq_and_sup_eq_iff
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst_2 : DecidableEq ι
inst_3 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (f ⊔ g).support (β := α) ∪ (f ⊓ g).support (β := α) = f.support (β := α) ∪ g.support (β := α)

Tactic:
(union_comm _ _).trans <| support_inf_union_support_sup _ _

Premises used: Finset.union_comm, DFinsupp.support_inf_union_support_sup, Eq.trans
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α_1 : ι → Type u_2
α : ι → Type u_3
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), IsOrderedAddMonoid.{u_3} (α i)
⊢ IsOrderedAddMonoid (Π₀ (i : ι), α i)

Tactic:
{ add_le_add_left := fun _ _ h c i ↦ add_le_add_left (h i) (c i) }

Premises used: add_le_add_left, IsOrderedAddMonoid._proof_1, DFinsupp, DFunLike.coe, IsOrderedAddMonoid.mk
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α_1 : ι → Type u_2
α : ι → Type u_3
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), IsOrderedCancelAddMonoid.{u_3} (α i)
⊢ IsOrderedCancelAddMonoid (Π₀ (i : ι), α i)

Tactic:
{ le_of_add_le_add_left := fun _ _ _ H i ↦ le_of_add_le_add_left (H i) }

Premises used: le_of_add_le_add_left, IsOrderedCancelAddMonoid.mk, IsOrderedCancelAddMonoid._proof_1, DFinsupp
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α_1 : ι → Type u_2
α : Type u_3
β : ι → Type u_4
inst : Semiring α
inst_1 : Preorder α
inst_2 : (i : ι) → AddCommMonoid (β i)
inst_3 : (i : ι) → Preorder (β i)
inst_4 : (i : ι) → Module.{u_3, u_4} α (β i)
inst_5 : ∀ (i : ι), PosSMulMono.{u_3, u_4} α (β i)
⊢ PosSMulMono α (Π₀ (i : ι), β i)

Tactic:
PosSMulMono.lift _ coe_le_coe coe_smul

Premises used: PosSMulMono.lift, DFinsupp.coe_smul
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α_1 : ι → Type u_2
α : Type u_3
β : ι → Type u_4
inst : Semiring α
inst_1 : Preorder α
inst_2 : (i : ι) → AddCommMonoid (β i)
inst_3 : (i : ι) → Preorder (β i)
inst_4 : (i : ι) → Module.{u_3, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosMono.{u_3, u_4} α (β i)
⊢ SMulPosMono α (Π₀ (i : ι), β i)

Tactic:
SMulPosMono.lift _ coe_le_coe coe_smul coe_zero

Premises used: SMulPosMono.lift, DFinsupp.coe_smul, DFinsupp.coe_zero