awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : (erase (β := β) j f : (a : ι) → β a) j = (f - single (β := β) j ((f : (a : ι) → β a) j) : (a : ι) → β a) j
h₁ :
  ∀ (h : j ≠ i),
    (erase (β := β) i f : (a : ι) → β a) j = (f - single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) j
⊢ (erase (β := β) i f : (a : ι) → β a) j = (f - single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) j

Tactic:
rcases eq_or_ne j i with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
j : ι
⊢ (erase (β := β) j f : (a : ι) → β a) j = (f - single (β := β) j ((f : (a : ι) → β a) j) : (a : ι) → β a) j

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : j ≠ i
⊢ (erase (β := β) i f : (a : ι) → β a) j = (f - single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) j

Tactic:
simp [erase_ne h, single_eq_of_ne h]

Premises used: DFinsupp.single_eq_of_ne, DFinsupp.erase_ne
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) i 0) 0

Tactic:
ext fun _ => ite_self _

Premises used: DFinsupp.ext, ite_self, OfNat.ofNat, DFinsupp.toFun
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (β := β) (fun (x : ι) ↦ x ≠ i) f = erase (β := β) i f

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (β := β) (fun (x : ι) ↦ i ≠ x) f = erase (β := β) i f

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
j i : ι
x : β i
rw :
  Eq (α := Π₀ (i : ι), β i) (filter (β := β) (fun (x : ι) ↦ x ≠ j) (single (β := β) i x))
    (if i = j then 0 else single (β := β) i x)
rw₁ : Eq (α := Π₀ (i : ι), β i) (if i ≠ j then single (β := β) i x else 0) (if i = j then 0 else single (β := β) i x)
rw₂ rw₃ :
  Eq (α := Π₀ (i : ι), β i) (if i = j then 0 else single (β := β) i x) (if i = j then 0 else single (β := β) i x)
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) j (single (β := β) i x)) (if i = j then 0 else single (β := β) i x)

Tactic:
rw [← filter_ne_eq_erase, filter_single, ite_not]

Premises used: DFinsupp.filter_single, ite_not, DFinsupp.filter_ne_eq_erase
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
x : β i
rw : Eq (α := Π₀ (i : ι), β i) (if i = i then 0 else single (β := β) i x) 0
rw₁ rw₂ : Eq (α := Π₀ (i : ι), β i) 0 0
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) i (single (β := β) i x)) 0

Tactic:
rw [erase_single, if_pos rfl]

Premises used: if_pos, DFinsupp.erase_single, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
x : β i
h : i ≠ j
rw : Eq (α := Π₀ (i : ι), β i) (if i = j then 0 else single (β := β) i x) (single (β := β) i x)
rw₁ rw₂ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i x) (single (β := β) i x)
⊢ Eq (α := Π₀ (i : ι), β i) (erase (β := β) j (single (β := β) i x)) (single (β := β) i x)

Tactic:
rw [erase_single, if_neg h]

Premises used: DFinsupp.erase_single, if_neg
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
inl : i ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b i = 0
inr : ∀ (hi : i ≠ j), j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0

Tactic:
rcases eq_or_ne i j with (rfl | hi)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
⊢ i ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b i = 0

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
hi : i ≠ j
inr :
  ∀ (hj : j ∈ (↑s : Multiset ι)), j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
inr₁ :
  ∀ (hj : (f : (a : ι) → β a) j = 0),
    j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0

Tactic:
obtain hj | (hj : f j = 0) := s.prop j

Premises used: Subtype.prop, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
hi : i ≠ j
hj : j ∈ (↑s : Multiset ι)
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0

Tactic:
Or.inl (Multiset.mem_cons_of_mem hj)

Premises used: Multiset.mem_cons_of_mem, Or.inl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
hi : i ≠ j
hj : j ∈ (↑s : Multiset ι)
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0

Tactic:
exact Or.inl (Multiset.mem_cons_of_mem hj)

Premises used: Multiset.mem_cons_of_mem, Or.inl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
hi : i ≠ j
hj : (f : (a : ι) → β a) j = 0
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0

Tactic:
Or.inr ((Function.update_of_ne hi.symm b _).trans hj)

Premises used: Ne.symm, Or.inr, Eq.trans, Function.update_of_ne
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
j : ι
hi : i ≠ j
hj : (f : (a : ι) → β a) j = 0
⊢ j ∈ i ::ₘ (↑s : Multiset ι) ∨ Function.update (β := β) (⇑f : (a : ι) → β a) i b j = 0

Tactic:
exact Or.inr ((Function.update_of_ne hi.symm b _).trans hj)

Premises used: Ne.symm, Or.inr, Eq.trans, Function.update_of_ne
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (⇑(f.update (β := β) i b) : (a : ι) → β a) = Function.update (β := β) (⇑f : (a : ι) → β a) i b

Tactic:
rfl

Premises used: Function.update, dite, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
h : ∀ (i_1 : ι), (f.update (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i_1 = (f : (a : ι) → β a) i_1
⊢ f.update (β := β) i ((f : (a : ι) → β a) i) = f

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i i_1 : ι
⊢ (f.update (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i_1 = (f : (a : ι) → β a) i_1

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
h : ∀ (j : ι), (f.update (β := β) i 0 : (a : ι) → β a) j = (erase (β := β) i f : (a : ι) → β a) j
⊢ f.update (β := β) i 0 = erase (β := β) i f

Tactic:
ext j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
h : (f.update (β := β) i 0 : (a : ι) → β a) i = (erase (β := β) i f : (a : ι) → β a) i
h₁ : ∀ (hi : i ≠ j), (f.update (β := β) i 0 : (a : ι) → β a) j = (erase (β := β) i f : (a : ι) → β a) j
⊢ (f.update (β := β) i 0 : (a : ι) → β a) j = (erase (β := β) i f : (a : ι) → β a) j

Tactic:
rcases eq_or_ne i j with (rfl | hi)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ (f.update (β := β) i 0 : (a : ι) → β a) i = (erase (β := β) i f : (a : ι) → β a) i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
hi : i ≠ j
⊢ (f.update (β := β) i 0 : (a : ι) → β a) j = (erase (β := β) i f : (a : ι) → β a) j

Tactic:
simp [hi.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : ∀ (j : ι), (f.update (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) j
⊢ f.update (β := β) i b = single (β := β) i b + erase (β := β) i f

Tactic:
ext j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : (f.update (β := β) i b : (a : ι) → β a) i = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) i
h₁ :
  ∀ (h : i ≠ j),
    (f.update (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) j
⊢ (f.update (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update (β := β) i b : (a : ι) → β a) i = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + erase (β := β) i f : (a : ι) → β a) j

Tactic:
simp [h, h.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : ∀ (j : ι), (f.update (β := β) i b : (a : ι) → β a) j = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) j
⊢ f.update (β := β) i b = erase (β := β) i f + single (β := β) i b

Tactic:
ext j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : (f.update (β := β) i b : (a : ι) → β a) i = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) i
h₁ :
  ∀ (h : i ≠ j),
    (f.update (β := β) i b : (a : ι) → β a) j = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) j
⊢ (f.update (β := β) i b : (a : ι) → β a) j = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update (β := β) i b : (a : ι) → β a) i = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update (β := β) i b : (a : ι) → β a) j = (erase (β := β) i f + single (β := β) i b : (a : ι) → β a) j

Tactic:
simp [h, h.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type u_1
inst_1 : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
rw : erase (β := β) i f + single (β := β) i b = f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b
rw₁ rw₂ :
  f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b =
    f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b
⊢ f.update (β := β) i b = f - single (β := β) i ((f : (a : ι) → β a) i) + single (β := β) i b

Tactic:
rw [update_eq_erase_add_single f i b, erase_eq_sub_single f i]

Premises used: DFinsupp.update_eq_erase_add_single, DFinsupp.erase_eq_sub_single
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
b₁ b₂ : β i
⊢ single (β := β) i (b₁ + b₂) = HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i b₁) (single (β := β) i b₂)

Tactic:
(zipWith_single_single (fun _ => (· + ·)) _ b₁ b₂).symm

Premises used: DFinsupp.zipWith_single_single, HAdd.hAdd, Eq.symm
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f₁ f₂ : Π₀ (i : ι), β i
x : ι
⊢ (erase (β := β) i (f₁ + f₂) : (a : ι) → β a) x = (erase (β := β) i f₁ + erase (β := β) i f₂ : (a : ι) → β a) x

Tactic:
simp [ite_zero_add]

Premises used: ite_zero_add
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type v
inst_1 : (i : ι) → AddGroup (β i)
i : ι
x : β i
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i (-x)) (-single (β := β) i x)

Tactic:
(singleAddHom β i).map_neg x

Premises used: DFinsupp.single, AddMonoidHom.map_neg, DFinsupp.singleAddHom
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type v
inst_1 : (i : ι) → AddGroup (β i)
i : ι
x y : β i
⊢ single (β := β) i (x - y) = HSub.hSub (α := Π₀ (i : ι), β i) (single (β := β) i x) (single (β := β) i y)

Tactic:
(singleAddHom β i).map_sub x y

Premises used: DFinsupp.single, DFinsupp.singleAddHom, AddMonoidHom.map_sub
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type v
inst_1 : (i : ι) → AddGroup (β i)
i : ι
f : Π₀ (i : ι), β i
⊢ erase (β := β) i (-f) = -erase (β := β) i f

Tactic:
(eraseAddHom β i).map_neg f

Premises used: DFinsupp.erase, AddMonoidHom.map_neg, DFinsupp.eraseAddHom
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
inst : DecidableEq ι
β : ι → Type v
inst_1 : (i : ι) → AddGroup (β i)
i : ι
f g : Π₀ (i : ι), β i
⊢ erase (β := β) i (f - g) = erase (β := β) i f - erase (β := β) i g

Tactic:
(eraseAddHom β i).map_sub f g

Premises used: DFinsupp.erase, AddMonoidHom.map_sub, DFinsupp.eraseAddHom
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : i = i'
subst : (single (β := β) i ((f : (a : ι) → β a) i) + erase (β := β) i f : (a : ι) → β a) i = (f : (a : ι) → β a) i
⊢ (single (β := β) i ((f : (a : ι) → β a) i) + erase (β := β) i f : (a : ι) → β a) i' = (f : (a : ι) → β a) i'

Tactic:
subst h
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
⊢ (single (β := β) i ((f : (a : ι) → β a) i) + erase (β := β) i f : (a : ι) → β a) i = (f : (a : ι) → β a) i

Tactic:
simp only [add_apply, single_apply, erase_apply, add_zero, dite_eq_ite, if_true]

Premises used: if_true, DFinsupp.add_apply, DFinsupp.erase_apply, dite_eq_ite, add_zero, DFinsupp.single_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : ¬i = i'
⊢ (single (β := β) i ((f : (a : ι) → β a) i) + erase (β := β) i f : (a : ι) → β a) i' = (f : (a : ι) → β a) i'

Tactic:
simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), zero_add]

Premises used: Ne.symm, zero_add, dif_neg, DFinsupp.add_apply, DFinsupp.erase_apply, DFinsupp.single_apply, if_neg
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : i = i'
subst : (erase (β := β) i f + single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i = (f : (a : ι) → β a) i
⊢ (erase (β := β) i f + single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i' = (f : (a : ι) → β a) i'

Tactic:
subst h
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
⊢ (erase (β := β) i f + single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i = (f : (a : ι) → β a) i

Tactic:
simp only [add_apply, single_apply, erase_apply, zero_add, dite_eq_ite, if_true]

Premises used: if_true, zero_add, DFinsupp.add_apply, DFinsupp.erase_apply, dite_eq_ite, DFinsupp.single_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : ¬i = i'
⊢ (erase (β := β) i f + single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i' = (f : (a : ι) → β a) i'

Tactic:
simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), add_zero]

Premises used: Ne.symm, dif_neg, DFinsupp.add_apply, DFinsupp.erase_apply, add_zero, DFinsupp.single_apply, if_neg
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
obtain :
  ∀ (f : (i : ι) → β i) (s : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }),
    p (mk' (β := fun (i : ι) ↦ β i) f s)
⊢ p f

Tactic:
obtain ⟨f, s⟩ := f
-- 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)
f : (i : ι) → β i
s : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
h : ∀ (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }), p (mk' (β := fun (i : ι) ↦ β i) f (Trunc.mk s))
⊢ p (mk' (β := fun (i : ι) ↦ β i) f s)

Tactic:
induction s using Trunc.induction_on with | _ s
-- 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)
f : (i : ι) → β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
h :
  ∀ (s : Multiset ι) (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)))
⊢ p (mk' (β := fun (i : ι) ↦ β i) f (Trunc.mk s))

Tactic:
obtain ⟨s, H⟩ := s
-- 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)
f : (i : ι) → β i
H : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i ∨ f i = 0
h :
  ∀ (this : f = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) 0 H)))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) 0 H)))

Tactic:
have : f = 0 := funext fun i => (H i).resolve_left (Multiset.notMem_zero _)
-- 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)
f : (i : ι) → β i
H : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i ∨ f i = 0
this : f = 0
h :
  ∀ (H : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i ∨ Eq.{v + 1} (α := β i) (0 i) 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) 0
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (0 i) 0) 0 H)))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) 0 H)))

Tactic:
subst this
-- 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)
H : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i ∨ Eq.{v + 1} (α := β i) (0 i) 0
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) 0
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (0 i) 0) 0 H)))

Tactic:
h0
-- 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)
H : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i ∨ Eq.{v + 1} (α := β i) (0 i) 0
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) 0
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (0 i) 0) 0 H)))

Tactic:
exact h0
-- 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
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))

Tactic:
?_