awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  toFun (β := fun (j : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)) ↦
      δ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι) j)
      ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
      a =
    0
inl :
  Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
    (((f : (a : ι) → Π₀ (j : α a), δ a j) ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x)) :
        (a_1 : α ⟨i, a⟩.fst) → δ ⟨i, a⟩.fst a_1)
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
    0
⊢ Membership.mem (γ := Multiset ((x : ι) × α x))
      ((↑s : Multiset ι).toFinset.attach.val.bind fun (i : ↥(↑s : Multiset ι).toFinset) ↦
        Multiset.map (Sigma.mk (β := fun (x : ι) ↦ α x) (↑i : ι)) (↑(fs i) : Multiset (α (↑i : ι))))
      (Sigma.mk (β := fun (x : ι) ↦ α x) i a) ∨
    Eq (α :=
      δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x))
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
      (((f : (a : ι) → Π₀ (j : α a), δ a j) ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x)) :
          (a_1 : α ⟨i, a⟩.fst) → δ ⟨i, a⟩.fst a_1)
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
      0

Tactic:
right
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  toFun (β := fun (j : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)) ↦
      δ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι) j)
      ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
      a =
    0
⊢ Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
    (((f : (a : ι) → Π₀ (j : α a), δ a j) ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x)) :
        (a_1 : α ⟨i, a⟩.fst) → δ ⟨i, a⟩.fst a_1)
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
    0

Tactic:
simp [toFun_eq_coe (f i) ▸ ha]
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
⊢ Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
      (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a ∨
    toFun (β := fun (j : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)) ↦
        δ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι) j)
        ((f : (a : ι) → Π₀ (j : α a), δ a j)
          (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
        a =
      0

Tactic:
cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with
            | inl ha =>
              left; rw [Multiset.mem_bind]
              use ⟨i, Multiset.mem_toFinset.mpr hi⟩
              constructor
              case right => simp [ha]
              case left => apply Multiset.mem_attach
            | inr ha => right; simp [toFun_eq_coe (f i) ▸ ha]

Premises used: Iff.mpr, Subtype.mk, Multiset.mem_attach, Subtype.prop, Multiset.mem_bind, Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0
inr :
  Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
    (((f : (a : ι) → Π₀ (j : α a), δ a j) ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x)) :
        (a_1 : α ⟨i, a⟩.fst) → δ ⟨i, a⟩.fst a_1)
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
    0
⊢ Membership.mem (γ := Multiset ((x : ι) × α x))
      ((↑s : Multiset ι).toFinset.attach.val.bind fun (i : ↥(↑s : Multiset ι).toFinset) ↦
        Multiset.map (Sigma.mk (β := fun (x : ι) ↦ α x) (↑i : ι)) (↑(fs i) : Multiset (α (↑i : ι))))
      (Sigma.mk (β := fun (x : ι) ↦ α x) i a) ∨
    Eq (α :=
      δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x))
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
      (((f : (a : ι) → Π₀ (j : α a), δ a j) ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x)) :
          (a_1 : α ⟨i, a⟩.fst) → δ ⟨i, a⟩.fst a_1)
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
      0

Tactic:
right
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0
⊢ Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
    (((f : (a : ι) → Π₀ (j : α a), δ a j) ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x)) :
        (a_1 : α ⟨i, a⟩.fst) → δ ⟨i, a⟩.fst a_1)
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
    0

Tactic:
simp [toFun_eq_coe f ▸ hi]
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
⊢ i ∈ (↑s : Multiset ι) ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0

Tactic:
cases s.prop i with
          | inl hi =>
            cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with
            | inl ha =>
              left; rw [Multiset.mem_bind]
              use ⟨i, Multiset.mem_toFinset.mpr hi⟩
              constructor
              case right => simp [ha]
              case left => apply Multiset.mem_attach
            | inr ha => right; simp [toFun_eq_coe (f i) ▸ ha]
          | inr hi => right; simp [toFun_eq_coe f ▸ hi]

Premises used: Multiset.mem_attach, Subtype.prop, Multiset.mem_bind
-- 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 : ι) (j : α i), δ i j
i : ι
j : α i
⊢ (f.sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j) =
    ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) 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 : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
    (sigmaUncurry (α := α) (δ := δ) 0) 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Set.Mem, Trunc.map, Multiset.dedup, setOf, Trunc.bind, Trunc.mk, Multiset.Mem, Multiset.ofList, Multiset.pmap, DFinsupp.sigmaUncurry, Trunc.liftOn, Multiset.join, List.foldr, Multiset.bind, Multiset.attach, 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 : ι) (j : α i), δ i j
⊢ (f + g).sigmaUncurry (α := α) (δ := δ) = f.sigmaUncurry (α := α) (δ := δ) + g.sigmaUncurry (α := α) (δ := δ)

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, 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 : ι) (j : α i), δ i j
⊢ (r • f).sigmaUncurry (α := α) (δ := δ) = r • f.sigmaUncurry (α := α) (δ := δ)

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
⊢ δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).fst (β := fun (x : ι) ↦ α x))
    ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).snd (β := fun (x : ι) ↦ α x))

Tactic:
exact x
-- 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
h :
  ∀ (i' : ι) (j' : α i'),
    Eq (α :=
      δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').fst (β := fun (x : ι) ↦ α x))
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').snd (β := fun (x : ι) ↦ α x)))
      ((sigmaUncurry (α := α) (δ := δ) (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x)) :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))
      ((single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))
⊢ Eq (α := Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
    (sigmaUncurry (α := α) (δ := δ) (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x)))
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x)

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) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
h :
  Eq (α := δ i' j')
    ((sigmaUncurry (α := α) (δ := δ) (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x)) :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') :
      δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').fst (β := fun (x : ι) ↦ α x))
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').snd (β := fun (x : ι) ↦ α x)))
    ((single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))
⊢ Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').snd (β := fun (x : ι) ↦ α x)))
    ((sigmaUncurry (α := α) (δ := δ) (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x)) :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))
    ((single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))

Tactic:
dsimp only
-- 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
h :
  ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j' =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j')
⊢ Eq (α := δ i' j')
    ((sigmaUncurry (α := α) (δ := δ) (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x)) :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') :
      δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').fst (β := fun (x : ι) ↦ α x))
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').snd (β := fun (x : ι) ↦ α x)))
    ((single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))

Tactic:
rw [sigmaUncurry_apply]

Premises used: DFinsupp.sigmaUncurry_apply
-- 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
h :
  ∀ (j' : α i),
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i :
          (a : α i) → δ i a)
        j' =
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
h₁ :
  ∀ (hi : i ≠ i'),
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
          (a : α i') → δ i' a)
        j' =
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i' j')
⊢ ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j' =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j')

Tactic:
obtain rfl | hi := eq_or_ne i i'

Premises used: eq_or_ne, 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
h :
  (single (β := δ i) j x : (a : α i) → δ i a) j' =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
⊢ ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i :
        (a : α i) → δ i a)
      j' =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')

Tactic:
rw [single_eq_same]

Premises used: DFinsupp.single_eq_same
-- 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
h :
  ∀ (x : δ i j'),
    (single (β := δ i) j' x : (a : α i) → δ i a) j' =
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (x : ι) ↦ α x) i j') x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
h₁ :
  ∀ (hj : j' ≠ j),
    (single (β := δ i) j x : (a : α i) → δ i a) j' =
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
⊢ (single (β := δ i) j x : (a : α i) → δ i a) j' =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')

Tactic:
obtain rfl | hj := eq_or_ne j' j

Premises used: eq_or_ne, 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j' : α i
x : δ i j'
h :
  x =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j') x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
h₁ h₂ : x = x
⊢ (single (β := δ i) j' x : (a : α i) → δ i a) j' =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j') x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')

Tactic:
rw [single_eq_same, single_eq_same]

Premises used: DFinsupp.single_eq_same
-- 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
h : Sigma.mk (β := fun (x : ι) ↦ α x) i j' ≠ Sigma.mk (β := fun (x : ι) ↦ α x) i j
⊢ (single (β := δ i) j x : (a : α i) → δ i a) j' =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')

Tactic:
rw [single_eq_of_ne hj, single_eq_of_ne]

Premises used: DFinsupp.single_eq_of_ne
-- 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ Sigma.mk (β := fun (x : ι) ↦ α x) i j' ≠ Sigma.mk (β := fun (x : ι) ↦ α x) i j

Tactic:
simpa using hj
-- 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)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
hi : i ≠ i'
⊢ ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j' =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j')

Tactic:
simp [hi]
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → 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))
h :
  ∀ (i : ι) (j : α i),
    Eq (α :=
      δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).fst (β := fun (x : ι) ↦ α x))
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).snd (β := fun (x : ι) ↦ α x)))
      ((f.sigmaCurry (α := α) (δ := δ).sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
      ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
⊢ f.sigmaCurry (α := α) (δ := δ).sigmaUncurry (α := α) (δ := δ) = f

Tactic:
ext ⟨i, j⟩