awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι), PosSMulReflectLE.{u_3, u_4} α (β i)
⊢ PosSMulReflectLE α (Π₀ (i : ι), β i)

Tactic:
PosSMulReflectLE.lift _ coe_le_coe coe_smul

Premises used: DFinsupp.coe_smul, PosSMulReflectLE.lift
-- 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 : ι), SMulPosReflectLE.{u_3, u_4} α (β i)
⊢ SMulPosReflectLE α (Π₀ (i : ι), β i)

Tactic:
SMulPosReflectLE.lift _ coe_le_coe coe_smul coe_zero

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

Tactic:
PosSMulStrictMono.lift _ coe_le_coe coe_smul

Premises used: PosSMulStrictMono.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 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (β i)
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → Module.{u_3, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosStrictMono.{u_3, u_4} α (β i)
⊢ SMulPosStrictMono α (Π₀ (i : ι), β i)

Tactic:
SMulPosStrictMono.lift _ coe_le_coe coe_smul coe_zero

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

Tactic:
SMulPosReflectLT.lift _ coe_le_coe coe_smul coe_zero

Premises used: SMulPosReflectLT.lift, DFinsupp.coe_smul, DFinsupp.coe_zero
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
⊢ ∀ (a : Π₀ (i : ι), α i), 0 ≤ a

Tactic:
simp [le_def]

Premises used: DFinsupp.le_def
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
⊢ Eq (α := Π₀ (i : ι), α i) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
f g : Π₀ (i : ι), α i
⊢ f + g = 0 ↔ f = 0 ∧ g = 0

Tactic:
simp [DFunLike.ext_iff, forall_and]

Premises used: DFunLike.ext_iff, forall_and
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
s : Finset ι
hf : f.support (β := α) ⊆ s
⊢ f ≤ g ↔ ∀ i ∈ s, (f : (a : ι) → α a) i ≤ (g : (a : ι) → α a) i

Tactic:
⟨fun h s _ ↦ h s, fun h s ↦
    if H : s ∈ f.support then h s (hf H) else (notMem_support_iff.1 H).symm ▸ zero_le⟩

Premises used: zero_le, DFinsupp.notMem_support_iff, Membership.mem, Eq.rec, DFinsupp.support, dite, Iff.intro, Iff.mp, Eq.symm
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
⊢ f ≤ g ↔ ∀ i ∈ f.support (β := α), (f : (a : ι) → α a) i ≤ (g : (a : ι) → α a) i

Tactic:
le_iff' <| Subset.refl _

Premises used: Finset.Subset.refl, DFinsupp.le_iff'
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : a ∈ f.support (β := α)
rw : ∀ (ha : 0 < (f : (a : ι) → α a) a), 0 < (g : (a : ι) → α a) a
⊢ a ∈ g.support (β := α)

Tactic:
rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢

Premises used: DFinsupp.mem_support_iff, pos_iff_ne_zero
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : 0 < (f : (a : ι) → α a) a
⊢ 0 < (g : (a : ι) → α a) a

Tactic:
ha.trans_le (h _)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : 0 < (f : (a : ι) → α a) a
⊢ 0 < (g : (a : ι) → α a) a

Tactic:
exact ha.trans_le (h _)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
hfg : f ≤ g
⊢ f.support (β := α) ⊆ g.support (β := α)

Tactic:
support_monotone hfg

Premises used: DFinsupp.support_monotone
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ (∀ (i_1 : ι),
      Membership.mem (γ := Finset ι) {i} i_1 → (single (β := α) i a : (a : ι) → α a) i_1 ≤ (f : (a : ι) → α a) i_1) ↔
    a ≤ (f : (a : ι) → α a) i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ single (β := α) i a ≤ f ↔ a ≤ (f : (a : ι) → α a) i

Tactic:
exact (le_iff' support_single_subset).trans <| by simp

Premises used: DFinsupp.le_iff', DFinsupp.support_single_subset, Iff.trans
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ single (β := α) i a ≤ f ↔ a ≤ (f : (a : ι) → α a) i

Tactic:
classical exact (le_iff' support_single_subset).trans <| by simp

Premises used: DFinsupp.le_iff', DFinsupp.support_single_subset, Iff.trans
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α 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 : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f g : Π₀ (i : ι), α i
h : ∀ (i : ι), (f - g : (a : ι) → α a) i = ((⇑f : (a : ι) → α a) - (⇑g : (a : ι) → α a)) i
⊢ (⇑(f - g) : (a : ι) → α a) = (⇑f : (a : ι) → α a) - (⇑g : (a : ι) → α a)

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f g : Π₀ (i : ι), α i
i : ι
⊢ (f - g : (a : ι) → α a) i = ((⇑f : (a : ι) → α a) - (⇑g : (a : ι) → α a)) i

Tactic:
tsub_apply f g i

Premises used: DFinsupp.tsub_apply
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f g : Π₀ (i : ι), α i
i : ι
⊢ (f - g : (a : ι) → α a) i = ((⇑f : (a : ι) → α a) - (⇑g : (a : ι) → α a)) i

Tactic:
exact tsub_apply f g i

Premises used: DFinsupp.tsub_apply
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
⊢ OrderedSub (Π₀ (i : ι), α i)

Tactic:
⟨fun _ _ _ ↦ forall_congr' fun _ ↦ tsub_le_iff_right⟩

Premises used: OrderedSub.mk, tsub_le_iff_right, forall_congr'
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f_1 g_1 : Π₀ (i : ι), α i
i : ι
a b : α i
inst_5 : ∀ (i : ι), AddLeftMono.{u_2} (α i)
f g : Π₀ (i : ι), α i
h : f ≤ g
exists : g = f + (g - f)
⊢ ∃ (c : Π₀ (i : ι), α i), g = f + c

Tactic:
exists g - f
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f_1 g_1 : Π₀ (i : ι), α i
i : ι
a b : α i
inst_5 : ∀ (i : ι), AddLeftMono.{u_2} (α i)
f g : Π₀ (i : ι), α i
h : f ≤ g
h₁ : ∀ (i : ι), (g : (a : ι) → α a) i = (f + (g - f) : (a : ι) → α a) i
⊢ g = f + (g - f)

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f_1 g_1 : Π₀ (i : ι), α i
i_1 : ι
a b : α i_1
inst_5 : ∀ (i : ι), AddLeftMono.{u_2} (α i)
f g : Π₀ (i : ι), α i
h : f ≤ g
i : ι
⊢ (g : (a : ι) → α a) i = (f + (g - f) : (a : ι) → α a) i

Tactic:
(add_tsub_cancel_of_le <| h i).symm

Premises used: Eq.symm, add_tsub_cancel_of_le
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f_1 g_1 : Π₀ (i : ι), α i
i_1 : ι
a b : α i_1
inst_5 : ∀ (i : ι), AddLeftMono.{u_2} (α i)
f g : Π₀ (i : ι), α i
h : f ≤ g
i : ι
⊢ (g : (a : ι) → α a) i = (f + (g - f) : (a : ι) → α a) i

Tactic:
exact (add_tsub_cancel_of_le <| h i).symm

Premises used: Eq.symm, add_tsub_cancel_of_le
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
h :
  ∀ (j : ι),
    (single (β := α) i (a - b) : (a : ι) → α a) j =
      (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
⊢ single (β := α) i (a - b) = HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b)

Tactic:
ext j
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
h :
  ∀ {a b : α j},
    (single (β := α) j (a - b) : (a : ι) → α a) j =
      (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) j a) (single (β := α) j b) : (a : ι) → α a) j
h₁ :
  ∀ (h : j ≠ i),
    (single (β := α) i (a - b) : (a : ι) → α a) j =
      (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j

Tactic:
obtain rfl | h := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
inst_5 : DecidableEq ι
j : ι
a b : α j
h :
  (single (β := α) j (a - b) : (a : ι) → α a) j =
    (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
h₁ : a - b = (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
h₂ : a - b = a - (single (β := α) j b : (a : ι) → α a) j
h₃ h₄ : a - b = a - b
⊢ (single (β := α) j (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) j a) (single (β := α) j b) : (a : ι) → α a) j

Tactic:
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]

Premises used: DFinsupp.single_eq_same, DFinsupp.tsub_apply
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
h : j ≠ i
h₁ :
  (single (β := α) i (a - b) : (a : ι) → α a) j =
    (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
h₂ : 0 = (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
h₃ : 0 = 0 - (single (β := α) i b : (a : ι) → α a) j
h₄ : 0 = HSub.hSub (α := α j) 0 0
h₅ h₆ : Eq.{u_2 + 1} (α := α j) 0 0
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j

Tactic:
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]

Premises used: DFinsupp.tsub_apply, tsub_self, DFinsupp.single_eq_of_ne
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f g : Π₀ (i : ι), α i
inst_5 : DecidableEq ι
inst_6 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (f - g).support (β := α) ⊆ f.support (β := α)

Tactic:
simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
    Ne, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]

Premises used: zero_le, DFinsupp.coe_tsub, Ne, tsub_eq_zero_iff_le, imp_true_iff, DFinsupp.mem_support_iff, Finset.subset_iff, Pi.sub_apply, not_imp_not
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f g : Π₀ (i : ι), α i
inst_5 : DecidableEq ι
inst_6 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ f.support (β := α) \ g.support (β := α) ⊆ (f - g).support (β := α)

Tactic:
simp +contextual [subset_iff]

Premises used: Finset.subset_iff
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → LinearOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_3 : DecidableEq ι
f g : Π₀ (i : ι), α i
h : ∀ (a : ι), a ∈ (f ⊓ g).support (β := α) ↔ a ∈ f.support (β := α) ∩ g.support (β := α)
⊢ (f ⊓ g).support (β := α) = f.support (β := α) ∩ g.support (β := α)

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → LinearOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_3 : DecidableEq ι
f g : Π₀ (i : ι), α i
a : ι
⊢ a ∈ (f ⊓ g).support (β := α) ↔ a ∈ f.support (β := α) ∩ g.support (β := α)

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → LinearOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_3 : DecidableEq ι
f g : Π₀ (i : ι), α i
h : ∀ (a : ι), a ∈ (f ⊔ g).support (β := α) ↔ a ∈ f.support (β := α) ∪ g.support (β := α)
⊢ (f ⊔ g).support (β := α) = f.support (β := α) ∪ g.support (β := α)

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → LinearOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_3 : DecidableEq ι
f g : Π₀ (i : ι), α i
a : ι
⊢ a ∈ (f ⊔ g).support (β := α) ↔ a ∈ f.support (β := α) ∪ g.support (β := α)

Tactic:
simp [imp_iff_not_or]

Premises used: imp_iff_not_or
-- Module: Mathlib.Data.DFinsupp.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → LinearOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_3 : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ Disjoint f g ↔ Disjoint (f.support (β := α)) (g.support (β := α))

Tactic:
simp [disjoint_iff, bot_eq_zero, ← DFinsupp.support_eq_empty]

Premises used: DFinsupp.disjoint_iff, DFinsupp.support_eq_empty, bot_eq_zero
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
i : ι
j : α i
⊢ ((f.sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
    (f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
⊢ Eq (α := Π₀ (i : ι) (j : α i), δ i j) (sigmaCurry (α := α) (δ := δ) 0) 0

Tactic:
rfl

Premises used: Multiset.filterMap, Multiset.map, List.map, Trunc.map, Trunc.bind, Multiset.zero, Trunc.mk, Multiset.ofList, Trunc.liftOn, DFinsupp.sigmaCurry, List.filterMap, rfl, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
h :
  ∀ (i : ι) (j : α i),
    (((f + g).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
      ((HAdd.hAdd (α := Π₀ (i : ι) (j : α i), δ i j) (f.sigmaCurry (α := α) (δ := δ)) (g.sigmaCurry (α := α) (δ := δ)) :
              (a : ι) → Π₀ (j : α a), δ a j)
            i :
          (a : α i) → δ i a)
        j
⊢ (f + g).sigmaCurry (α := α) (δ := δ) =
    HAdd.hAdd (α := Π₀ (i : ι) (j : α i), δ i j) (f.sigmaCurry (α := α) (δ := δ)) (g.sigmaCurry (α := α) (δ := δ))

Tactic:
ext (i j)
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
i : ι
j : α i
⊢ (((f + g).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
    ((HAdd.hAdd (α := Π₀ (i : ι) (j : α i), δ i j) (f.sigmaCurry (α := α) (δ := δ)) (g.sigmaCurry (α := α) (δ := δ)) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i :
        (a : α i) → δ i a)
      j

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : Monoid γ
inst_2 : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst_3 : (i : ι) → (j : α i) → DistribMulAction.{w, v} γ (δ i j)
r : γ
f : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
h :
  ∀ (i : ι) (j : α i),
    (((r • f).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
      ((HSMul.hSMul (β := Π₀ (i : ι) (j : α i), δ i j) r (f.sigmaCurry (α := α) (δ := δ)) :
              (a : ι) → Π₀ (j : α a), δ a j)
            i :
          (a : α i) → δ i a)
        j
⊢ (r • f).sigmaCurry (α := α) (δ := δ) =
    HSMul.hSMul (β := Π₀ (i : ι) (j : α i), δ i j) r (f.sigmaCurry (α := α) (δ := δ))

Tactic:
ext (i j)
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : Monoid γ
inst_2 : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst_3 : (i : ι) → (j : α i) → DistribMulAction.{w, v} γ (δ i j)
r : γ
f : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
i : ι
j : α i
⊢ (((r • f).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
    ((HSMul.hSMul (β := Π₀ (i : ι) (j : α i), δ i j) r (f.sigmaCurry (α := α) (δ := δ)) : (a : ι) → Π₀ (j : α a), δ a j)
          i :
        (a : α i) → δ i a)
      j

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
ij : (i : ι) × α i
x : δ (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i))
obtain :
  ∀ (i : ι) (j : α i)
    (x :
      δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
        ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))),
    Eq (α := Π₀ (i : ι) (j : α i), δ i j)
      (sigmaCurry (α := α) (δ := δ)
        (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x))
      (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j)
        ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
        (single (β := δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i)))
          ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)) x))
⊢ Eq (α := Π₀ (i : ι) (j : α i), δ i j)
    (sigmaCurry (α := α) (δ := δ)
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))) ij
        x))
    (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) (ij.fst (β := fun (i : ι) ↦ α i))
      (single (β := δ (ij.fst (β := fun (i : ι) ↦ α i))) (ij.snd (β := fun (i : ι) ↦ α i)) x))

Tactic:
obtain ⟨i, j⟩ := ij