awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
H : Eq (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y)
i : (↑(↑s : Set ι) : Type u)
⊢ Eq (α := β (↑i : ι)) ((mk (β := β) s x : (a : ι) → β a) (↑i : ι)) ((mk (β := β) s y : (a : ι) → β a) (↑i : ι))

Tactic:
have h1 : (mk s x : ∀ i, β i) i = (mk s y : ∀ i, β i) i := by grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
H : Eq (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y)
i : (↑(↑s : Set ι) : Type u)
h1 : Eq (α := β (↑i : ι)) ((mk (β := β) s x : (a : ι) → β a) (↑i : ι)) ((mk (β := β) s y : (a : ι) → β a) (↑i : ι))
⊢ x i = y i

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : Fintype ι
f : Π₀ (i : ι), β i
⊢ (Equiv.symm (equivFunOnFintype (β := β)) : (a : (i : ι) → β i) → Π₀ (i : ι), β i) (⇑f : (a : ι) → β a) = f

Tactic:
Equiv.symm_apply_apply _ _

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
b : β i
j : ι
⊢ j = i → Membership.mem (γ := Multiset ι) {i} j

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
b : β i
⊢ (⇑(single (β := β) i b) : (a : ι) → β a) = Pi.single (M := β) i b

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i i' : ι
b : β i
rw :
  Eq.{v + 1} (α := β i') (if h : i' = i then Eq.ndrec (motive := β) b ⋯ else 0 i')
    (if h : i = i' then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h b else 0)
⊢ (single (β := β) i b : (a : ι) → β a) i' =
    if h : i = i' then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h b else 0

Tactic:
rw [single_eq_pi_single, Pi.single, Function.update]

Premises used: Function.update, Pi.single, DFinsupp.single_eq_pi_single
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i i' : ι
b : β i
⊢ Eq.{v + 1} (α := β i') (if h : i' = i then Eq.ndrec (motive := β) b ⋯ else 0 i')
    (if h : i = i' then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h b else 0)

Tactic:
simp [@eq_comm _ i i']

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

Tactic:
DFunLike.coe_injective <| Pi.single_zero _

Premises used: Pi.single_zero, DFunLike.coe_injective
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
b : β i
⊢ (single (β := β) i b : (a : ι) → β a) i = b

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i i' : ι
b : β i
h : i' ≠ i
⊢ (single (β := β) i b : (a : ι) → β a) i' = 0

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
⊢ Function.Injective (α := β i) (β := Π₀ (i : ι), β i) (single (β := β) i)

Tactic:
fun _ _ H =>
  Pi.single_injective i <| DFunLike.coe_injective.eq_iff.mpr H

Premises used: Iff.mpr, Function.Injective.eq_iff, DFunLike.coe_injective, Pi.single_injective, Function.Injective
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
mp : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj) → i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
mpr : i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0 → Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj) ↔ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
constructor
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
pos : ∀ (hij : i = j), i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
neg : ∀ (hij : ¬i = j), i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
by_cases hij : i = j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : i = j
pos :
  ∀ (xj : β i) (h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xj)),
    i = i ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
subst hij
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi xj : β i
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xj)
⊢ i = i ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
Or.inl ⟨rfl, heq_of_eq (DFinsupp.single_injective h)⟩

Premises used: DFinsupp.single_injective, heq_of_eq, And.intro, Or.inl, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi xj : β i
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xj)
⊢ i = i ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
exact Or.inl ⟨rfl, heq_of_eq (DFinsupp.single_injective h)⟩

Premises used: Or.inl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
⊢ (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)

Tactic:
have h_coe : ⇑(DFinsupp.single i xi) = DFinsupp.single j xj := congr_arg (⇑) h
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
⊢ (single (β := β) i xi : (a : ι) → β a) i = (single (β := β) j xj : (a : ι) → β a) i

Tactic:
have hci := congr_fun h_coe i
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : (single (β := β) i xi : (a : ι) → β a) i = (single (β := β) j xj : (a : ι) → β a) i
⊢ (single (β := β) i xi : (a : ι) → β a) j = (single (β := β) j xj : (a : ι) → β a) j

Tactic:
have hcj := congr_fun h_coe j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : (single (β := β) i xi : (a : ι) → β a) i = (single (β := β) j xj : (a : ι) → β a) i
hcj : (single (β := β) i xi : (a : ι) → β a) j = (single (β := β) j xj : (a : ι) → β a) j
⊢ xi = (single (β := β) j xj : (a : ι) → β a) i

Tactic:
rw [DFinsupp.single_eq_same] at hci hcj

Premises used: DFinsupp.single_eq_same
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : (single (β := β) i xi : (a : ι) → β a) i = (single (β := β) j xj : (a : ι) → β a) i
hcj : (single (β := β) i xi : (a : ι) → β a) j = (single (β := β) j xj : (a : ι) → β a) j
hci₁ : xi = (single (β := β) j xj : (a : ι) → β a) i
⊢ (single (β := β) i xi : (a : ι) → β a) j = xj

Tactic:
rw [DFinsupp.single_eq_same] at hci hcj

Premises used: DFinsupp.single_eq_same
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : xi = (single (β := β) j xj : (a : ι) → β a) i
hcj : (single (β := β) i xi : (a : ι) → β a) j = xj
⊢ xi = 0

Tactic:
rw [DFinsupp.single_eq_of_ne hij] at hci

Premises used: DFinsupp.single_eq_of_ne
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : xi = (single (β := β) j xj : (a : ι) → β a) i
hcj : (single (β := β) i xi : (a : ι) → β a) j = xj
hci₁ : xi = 0
⊢ (single (β := β) i xi : (a : ι) → β a) j = xj

Tactic:
rw [DFinsupp.single_eq_of_ne hij] at hci

Premises used: DFinsupp.single_eq_of_ne
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : xi = 0
hcj : (single (β := β) i xi : (a : ι) → β a) j = xj
⊢ 0 = xj

Tactic:
rw [DFinsupp.single_eq_of_ne (Ne.symm hij)] at hcj

Premises used: DFinsupp.single_eq_of_ne, Ne.symm
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : xi = 0
hcj : 0 = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
Or.inr ⟨hci, hcj.symm⟩

Premises used: And.intro, Eq.symm, Or.inr
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : xi = 0
hcj : 0 = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
exact Or.inr ⟨hci, hcj.symm⟩

Premises used: Or.inr
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi xj : β i
hxi : xi ≍ xj
mpr mpr₁ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xj) (single (β := β) i xj)
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xj)

Tactic:
rw [eq_of_heq hxi]

Premises used: eq_of_heq
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
mpr : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j xj)
mpr₁ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j 0)
mpr₂ : Eq (α := Π₀ (i : ι), β i) 0 (single (β := β) j 0)
mpr₃ mpr₄ : Eq (α := Π₀ (i : ι), β i) 0 0
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)

Tactic:
rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]

Premises used: DFinsupp.single_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
b : (i : ι) → β i
h : ∀ (i : ι), b i ≠ 0
⊢ Function.Injective (β := Π₀ (i : ι), β i) fun (i : ι) ↦ single (β := β) i (b i)

Tactic:
fun _ _ H =>
  (((single_eq_single_iff _ _ _ _).mp H).resolve_right fun hb => h _ hb.1).left

Premises used: DFinsupp.single_eq_single_iff, And.left, Iff.mp, Function.Injective, Or.resolve_right
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi : β i
rw : i = i ∧ HEq xi (β := β i) 0 ∨ xi = 0 ∧ Eq.{v + 1} (α := β i) 0 0 ↔ xi = 0
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) 0 ↔ xi = 0

Tactic:
rw [← single_zero i, single_eq_single_iff]

Premises used: DFinsupp.single_eq_single_iff, DFinsupp.single_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi : β i
⊢ i = i ∧ HEq xi (β := β i) 0 ∨ xi = 0 ∧ Eq.{v + 1} (α := β i) 0 0 ↔ xi = 0

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi : β i
⊢ Ne (α := Π₀ (i : ι), β i) (single (β := β) i xi) 0 ↔ xi ≠ 0

Tactic:
single_eq_zero.not

Premises used: Iff.not, DFinsupp.single_eq_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
h :
  ∀ (j : ι),
    (filter (β := β) p (single (β := β) i x) : (a : ι) → β a) j =
      (if p i then single (β := β) i x else 0 : (a : ι) → β a) j
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p (single (β := β) i x)) (if p i then single (β := β) i x else 0)

Tactic:
ext j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
j : ι
⊢ (if p i then single (β := β) i x else 0 : (a : ι) → β a) j =
    if p i then (single (β := β) i x : (a : ι) → β a) j else (0 : (a : ι) → β a) j

Tactic:
have := apply_ite (fun x : Π₀ i, β i => x j) (p i) (single i x) 0
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
j : ι
this :
  (if p i then single (β := β) i x else 0 : (a : ι) → β a) j =
    if p i then (single (β := β) i x : (a : ι) → β a) j else 0
⊢ (filter (β := β) p (single (β := β) i x) : (a : ι) → β a) j =
    (if p i then single (β := β) i x else 0 : (a : ι) → β a) j

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
h : p i
rw : Eq (α := Π₀ (i : ι), β i) (if p i then single (β := β) i x else 0) (single (β := β) i x)
rw₁ rw₂ : Eq (α := Π₀ (i : ι), β i) (single (β := β) i x) (single (β := β) i x)
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p (single (β := β) i x)) (single (β := β) i x)

Tactic:
rw [filter_single, if_pos h]

Premises used: if_pos, DFinsupp.filter_single
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
p : ι → Prop
inst_2 : DecidablePred p
i : ι
x : β i
h : ¬p i
rw : Eq (α := Π₀ (i : ι), β i) (if p i then single (β := β) i x else 0) 0
rw₁ rw₂ : Eq (α := Π₀ (i : ι), β i) 0 0
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p (single (β := β) i x)) 0

Tactic:
rw [filter_single, if_neg h]

Premises used: DFinsupp.filter_single, if_neg
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Sigma.mk (β := β) i xi = Sigma.mk (β := β) j xj
refl : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xi)
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)

Tactic:
cases h
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi : β i
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xi)

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
m : β i
⊢ (equivFunOnFintype (β := β) : (a : Π₀ (i : ι), β i) → (i : ι) → β i) (single (β := β) i m) = Pi.single (M := β) i m

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
inst_2 : Fintype ι
i : ι
m : β i
⊢ Eq (α := Π₀ (i : ι), β i)
    ((Equiv.symm (equivFunOnFintype (β := β)) : (a : (i : ι) → β i) → Π₀ (i : ι), β i) (Pi.single (M := β) i m) :
      Π₀ (i : ι), β i)
    (single (β := β) i m : Π₀ (i : ι), β i)

Tactic:
simp only [← single_eq_pi_single, equivFunOnFintype_symm_coe]

Premises used: DFinsupp.equivFunOnFintype_symm_coe, DFinsupp.single_eq_pi_single
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
h :
  ∀ (i_1 : ι),
    (filter (β := β) (fun (x : ι) ↦ i = x) f : (a : ι) → β a) i_1 =
      (single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i_1
⊢ filter (β := β) (fun (x : ι) ↦ i = x) f = single (β := β) i ((f : (a : ι) → β a) i)

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 : ι
h :
  (if i = i_1 then (f : (a : ι) → β a) i_1 else 0) =
    if h : i = i_1 then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i) else 0
⊢ (filter (β := β) (fun (x : ι) ↦ i = x) f : (a : ι) → β a) i_1 =
    (single (β := β) i ((f : (a : ι) → β a) i) : (a : ι) → β a) i_1

Tactic:
rw [filter_apply, single_apply]

Premises used: DFinsupp.filter_apply, DFinsupp.single_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i i_1 : ι
h :
  ∀ (h : i = i_1),
    (f : (a : ι) → β a) i_1 = Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i)
h₁ : ¬i = i_1 → Eq.{v + 1} (α := β i_1) 0 0
⊢ (if i = i_1 then (f : (a : ι) → β a) i_1 else 0) =
    if h : i = i_1 then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h ((f : (a : ι) → β a) i) else 0

Tactic:
split
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i i_1 : ι
h_1 : i = i_1
h : (f : (a : ι) → β a) i_1 = Eq.recOn (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) ⋯ ((f : (a : ι) → β a) i_1)
⊢ (f : (a : ι) → β a) i_1 = Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h_1 ((f : (a : ι) → β a) i)

Tactic:
subst i
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ (f : (a : ι) → β a) i = Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) ⋯ ((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 i_1 : ι
h : ¬i = i_1
⊢ Eq.{v + 1} (α := β i_1) 0 0

Tactic:
simp
-- 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 = single (β := β) i ((f : (a : ι) → β a) i)

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Zero (β₁ i)
inst_3 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
⊢ zipWith (β := β) (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b₁) (single (β := β₂) i b₂) =
    single (β := β) i (f i b₁ b₂)

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

Tactic:
rfl

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

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

Tactic:
simp [h]
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
h :
  ∀ (j : ι),
    (piecewise (β := β) (single (β := β) i ((x : (a : ι) → β a) i)) (erase (β := β) i x) {i} : (a : ι) → β a) j =
      (x : (a : ι) → β a) j
⊢ piecewise (β := β) (single (β := β) i ((x : (a : ι) → β a) i)) (erase (β := β) i x) {i} = x

Tactic:
ext j
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h :
  (if Membership.mem (γ := Set ι) {i} j then (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j
    else (erase (β := β) i x : (a : ι) → β a) j) =
    (x : (a : ι) → β a) j
⊢ (piecewise (β := β) (single (β := β) i ((x : (a : ι) → β a) i)) (erase (β := β) i x) {i} : (a : ι) → β a) j =
    (x : (a : ι) → β a) j

Tactic:
rw [piecewise_apply]

Premises used: DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
pos :
  ∀ (h : Membership.mem (γ := Set ι) {i} j),
    (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j = (x : (a : ι) → β a) j
neg : ∀ (h : j ∉ {i}), (erase (β := β) i x : (a : ι) → β a) j = (x : (a : ι) → β a) j
⊢ (if Membership.mem (γ := Set ι) {i} j then (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j
    else (erase (β := β) i x : (a : ι) → β a) j) =
    (x : (a : ι) → β a) j

Tactic:
split_ifs with h
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : Membership.mem (γ := Set ι) {i} j
pos : (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) i = (x : (a : ι) → β a) i
pos₁ pos₂ : (x : (a : ι) → β a) i = (x : (a : ι) → β a) i
⊢ (single (β := β) i ((x : (a : ι) → β a) i) : (a : ι) → β a) j = (x : (a : ι) → β a) j

Tactic:
rw [(id h : j = i), single_eq_same]

Premises used: DFinsupp.single_eq_same, id
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∉ {i}
⊢ (erase (β := β) i x : (a : ι) → β a) j = (x : (a : ι) → β a) j

Tactic:
erase_ne h

Premises used: DFinsupp.erase_ne
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∉ {i}
⊢ (erase (β := β) i x : (a : ι) → β a) j = (x : (a : ι) → β a) j

Tactic:
exact erase_ne h

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

Tactic:
ext j