awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
h : ¬f i = 0
⊢ p
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
h : ∀ (j : ι), (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
⊢ f + single (β := β) i b = single (β := β) i b + f

Tactic:
ext j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
j : ι
pos : ∀ (H : i = j), (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
neg : ∀ (H : ¬i = j), (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
⊢ (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j

Tactic:
by_cases H : i = j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : i = j
pos : (f + single (β := β) i b : (a : ι) → β a) i = (single (β := β) i b + f : (a : ι) → β a) i
⊢ (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j

Tactic:
subst H
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
⊢ (f + single (β := β) i b : (a : ι) → β a) i = (single (β := β) i b + f : (a : ι) → β a) i

Tactic:
simp [h1]
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : ¬i = j
⊢ (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j

Tactic:
simp [H]
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
simp :
  (if H : i ∈ s then (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HAdd.hAdd (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
⊢ (mk (β := β) s (x + y) : (a : ι) → β a) i =
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y) : (a : ι) → β a) i

Tactic:
simp only [add_apply, mk_apply]

Premises used: DFinsupp.add_apply, DFinsupp.mk_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HAdd.hAdd (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
neg : i ∉ s → 0 = HAdd.hAdd (α := β i) 0 0
⊢ (if H : i ∈ s then (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HAdd.hAdd (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)

Tactic:
split_ifs
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∈ s
⊢ (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HAdd.hAdd (α := β i) (β := β i)
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
      (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∉ s
neg neg₁ : Eq.{v + 1} (α := β i) 0 0
⊢ 0 = HAdd.hAdd (α := β i) 0 0

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HAdd.hAdd (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
neg : i ∉ s → 0 = HAdd.hAdd (α := β i) 0 0
pos₁ :
  ∀ (h : i ∈ s),
    (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HAdd.hAdd (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
neg₁ : i ∉ s → 0 = HAdd.hAdd (α := β i) 0 0
⊢ (if H : i ∈ s then (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HAdd.hAdd (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)

Tactic:
split_ifs <;> [rfl; rw [zero_add]]

Premises used: zero_add
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
s : Finset ι
i : ι
simp : (if H : i ∈ s then 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) = (0 : (a : ι) → β a) i
⊢ (mk (β := β) s 0 : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
simp only [mk_apply]

Premises used: DFinsupp.mk_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
s : Finset ι
i : ι
pos : ∀ (h : i ∈ s), 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) = (0 : (a : ι) → β a) i
neg : i ∉ s → 0 = (0 : (a : ι) → β a) i
⊢ (if H : i ∈ s then 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) = (0 : (a : ι) → β a) i

Tactic:
split_ifs
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
s : Finset ι
i : ι
h : i ∈ s
⊢ 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) = (0 : (a : ι) → β a) i

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
s : Finset ι
i : ι
h : i ∉ s
⊢ 0 = (0 : (a : ι) → β a) i

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
simp :
  Eq.{v + 1} (α := β i) (if H : i ∈ s then (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (-if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
⊢ (mk (β := β) s (-x) : (a : ι) → β a) i = (-mk (β := β) s x : (a : ι) → β a) i

Tactic:
simp only [neg_apply, mk_apply]

Premises used: DFinsupp.neg_apply, DFinsupp.mk_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      -x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h)
neg : i ∉ s → Eq.{v + 1} (α := β i) 0 (-0)
⊢ Eq.{v + 1} (α := β i) (if H : i ∈ s then (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (-if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)

Tactic:
split_ifs
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∈ s
⊢ (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    -x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h)

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∉ s
neg neg₁ : Eq.{v + 1} (α := β i) 0 0
⊢ Eq.{v + 1} (α := β i) 0 (-0)

Tactic:
rw [neg_zero]

Premises used: neg_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      -x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h)
neg : i ∉ s → Eq.{v + 1} (α := β i) 0 (-0)
pos₁ :
  ∀ (h : i ∈ s),
    (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      -x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h)
neg₁ : i ∉ s → Eq.{v + 1} (α := β i) 0 (-0)
⊢ Eq.{v + 1} (α := β i) (if H : i ∈ s then (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (-if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)

Tactic:
split_ifs <;> [rfl; rw [neg_zero]]

Premises used: neg_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
simp :
  (if H : i ∈ s then (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSub.hSub (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
⊢ (mk (β := β) s (x - y) : (a : ι) → β a) i =
    (HSub.hSub (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y) : (a : ι) → β a) i

Tactic:
simp only [sub_apply, mk_apply]

Premises used: DFinsupp.mk_apply, DFinsupp.sub_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSub.hSub (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
neg : i ∉ s → 0 = HSub.hSub (α := β i) 0 0
⊢ (if H : i ∈ s then (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSub.hSub (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)

Tactic:
split_ifs
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∈ s
⊢ (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HSub.hSub (α := β i) (β := β i)
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
      (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∉ s
neg neg₁ : Eq.{v + 1} (α := β i) 0 0
⊢ 0 = HSub.hSub (α := β i) 0 0

Tactic:
rw [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSub.hSub (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
neg : i ∉ s → 0 = HSub.hSub (α := β i) 0 0
pos₁ :
  ∀ (h : i ∈ s),
    (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSub.hSub (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
neg₁ : i ∉ s → 0 = HSub.hSub (α := β i) 0 0
⊢ (if H : i ∈ s then (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSub.hSub (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)

Tactic:
split_ifs <;> [rfl; rw [sub_zero]]

Premises used: sub_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
dsimp : {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} = {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
⊢ Eq.{u + 1} (α := Finset ι)
    ((fun (xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }) ↦
        {i ∈ (↑xs : Multiset ι).toFinset | (f : (a : ι) → β a) i ≠ 0})
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0) sx hx))
    ((fun (xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }) ↦
        {i ∈ (↑xs : Multiset ι).toFinset | (f : (a : ι) → β a) i ≠ 0})
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0) sy hy))

Tactic:
dsimp only [Subtype.coe_mk, toFun_eq_coe] at *

Premises used: Subtype.coe_mk, DFinsupp.toFun_eq_coe
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
h : ∀ (i : ι), i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} ↔ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
⊢ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} = {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
h : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} → i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
h₁ : i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0} → i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
⊢ i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} ↔ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}

Tactic:
constructor
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
⊢ i ∈ sx.toFinset

Tactic:
rcases Finset.mem_filter.1 H with ⟨_, h⟩

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
left : i ∈ sx.toFinset
⊢ (f : (a : ι) → β a) i ≠ 0

Tactic:
rcases Finset.mem_filter.1 H with ⟨_, h⟩

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
left : i ∈ sx.toFinset
h : (f : (a : ι) → β a) i ≠ 0
⊢ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}

Tactic:
Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hy i).resolve_right h, h⟩

Premises used: Iff.mpr, And.intro, Finset.mem_filter, Or.resolve_right, Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
left : i ∈ sx.toFinset
h : (f : (a : ι) → β a) i ≠ 0
⊢ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}

Tactic:
exact Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hy i).resolve_right h, h⟩

Premises used: Iff.mpr, And.intro, Finset.mem_filter, Or.resolve_right, Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
⊢ i ∈ sy.toFinset

Tactic:
rcases Finset.mem_filter.1 H with ⟨_, h⟩

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
left : i ∈ sy.toFinset
⊢ (f : (a : ι) → β a) i ≠ 0

Tactic:
rcases Finset.mem_filter.1 H with ⟨_, h⟩

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
left : i ∈ sy.toFinset
h : (f : (a : ι) → β a) i ≠ 0
⊢ i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}

Tactic:
Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hx i).resolve_right h, h⟩

Premises used: Iff.mpr, And.intro, Finset.mem_filter, Or.resolve_right, Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
left : i ∈ sy.toFinset
h : (f : (a : ι) → β a) i ≠ 0
⊢ i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}

Tactic:
exact Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hx i).resolve_right h, h⟩

Premises used: Iff.mpr, And.intro, Finset.mem_filter, Or.resolve_right, Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
⊢ support (β := β) (mk (β := β) s x) ⊆ s

Tactic:
fun _ H => Multiset.mem_toFinset.1 (Finset.mem_filter.1 H).1

Premises used: Set.Mem, setOf, Multiset.Mem, And.left, Iff.mp, Finset.mem_filter, Multiset.mem_toFinset