awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this : DecidableEq ι
haveI : (this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)) → (i : ι) × η i →₀ N
⊢ (i : ι) × η i →₀ N

Tactic:
haveI := fun i => Classical.decEq (η i →₀ N)
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this_1 : DecidableEq ι
this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)
onFinset :
  ∀ (g : (i : ι) × η i)
    (hg :
      Ne.{u_5 + 1} (α := N)
        ((fun (ji : (i : ι) × η i) ↦
            (((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                (ji.snd (β := fun (i : ι) ↦ η i)) :
              N))
          g)
        0),
    g.fst (β := fun (i : ι) ↦ η i) ∈ f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
⊢ (i : ι) × η i →₀ N

Tactic:
refine
      onFinset (Finset.sigma f.support fun j => (f j).support) (fun ji => f ji.1 ji.2) fun g hg =>
        Finset.mem_sigma.mpr ⟨?_, mem_support_iff.mpr hg⟩

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finsupp.support, Finset.sigma, Finset.mem_sigma, Sigma.fst, DFinsupp.support, Finsupp.onFinset, And.intro, Sigma.snd, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this_1 : DecidableEq ι
this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)
g : (i : ι) × η i
hg :
  Ne.{u_5 + 1} (α := N)
    ((fun (ji : (i : ι) × η i) ↦
        (((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
            (ji.snd (β := fun (i : ι) ↦ η i)) :
          N))
      g)
    0
simp :
  ¬Eq (α := Finsupp.{u_4, u_5} (η (g.fst (β := fun (i : ι) ↦ η i))) N)
      ((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i))) 0
⊢ g.fst (β := fun (i : ι) ↦ η i) ∈ f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)

Tactic:
simp only [Ne, DFinsupp.mem_support_toFun]

Premises used: DFinsupp.mem_support_toFun, Ne
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this_1 : DecidableEq ι
this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)
g : (i : ι) × η i
hg :
  ¬Eq.{u_5 + 1} (α := N)
      (((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i)) : (a : η g.fst) → N)
          (g.snd (β := fun (i : ι) ↦ η i)) :
        N)
      (0 : N)
h :
  Eq (α := Finsupp.{u_4, u_5} (η (g.fst (β := fun (i : ι) ↦ η i))) N)
    ((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i))) 0
⊢ ¬Eq.{u_5 + 1} (α := N) ((0 : (a : η g.fst) → N) (g.snd (β := fun (i : ι) ↦ η i)) : N) (0 : N)

Tactic:
rw [h] at hg
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this_1 : DecidableEq ι
this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)
g : (i : ι) × η i
hg :
  ¬Eq.{u_5 + 1} (α := N)
      (((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i)) : (a : η g.fst) → N)
          (g.snd (β := fun (i : ι) ↦ η i)) :
        N)
      (0 : N)
h :
  Eq (α := Finsupp.{u_4, u_5} (η (g.fst (β := fun (i : ι) ↦ η i))) N)
    ((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i))) 0
hg₁ : ¬Eq.{u_5 + 1} (α := N) ((0 : (a : η g.fst) → N) (g.snd (β := fun (i : ι) ↦ η i)) : N) (0 : N)
⊢ Eq (α := Finsupp.{u_4, u_5} (η (g.fst (β := fun (i : ι) ↦ η i))) N)
    ((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i))) 0

Tactic:
rw [h] at hg
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
this_1 : DecidableEq ι
this : (i : ι) → DecidableEq (Finsupp.{u_4, u_5} (η i) N)
g : (i : ι) × η i
hg : ¬Eq.{u_5 + 1} (α := N) ((0 : (a : η g.fst) → N) (g.snd (β := fun (i : ι) ↦ η i)) : N) (0 : N)
h :
  Eq (α := Finsupp.{u_4, u_5} (η (g.fst (β := fun (i : ι) ↦ η i))) N)
    ((f : (a : ι) → η a →₀ N) (g.fst (β := fun (i : ι) ↦ η i))) 0
⊢ False

Tactic:
simp only [coe_zero, Pi.zero_apply, not_true] at hg

Premises used: Pi.zero_apply, not_true, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : (i : ι) × η i →₀ N
h :
  ∀ (a : (i : ι) × η i),
    Eq.{u_5 + 1} (α := N)
      (((fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
                (onFinset
                    (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
                      ((f : (a : ι) → η a →₀ N) j).support)
                    (fun (ji : (i : ι) × η i) ↦
                      ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                        (ji.snd (β := fun (i : ι) ↦ η i)))
                    ⋯ :
                  (i : ι) × η i →₀ N))
              ((fun (f : (i : ι) × η i →₀ N) ↦
                  (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
                      (Trunc.mk
                        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                          f.splitSupport (αs := η).val ⋯)) :
                    Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
                f) :
            (a : (i : ι) × η i) → N)
          a :
        N)
      ((f : (a : (i : ι) × η i) → N) a : N)
⊢ (fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
        (onFinset
            (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
              ((f : (a : ι) → η a →₀ N) j).support)
            (fun (ji : (i : ι) × η i) ↦
              ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                (ji.snd (β := fun (i : ι) ↦ η i)))
            ⋯ :
          (i : ι) × η i →₀ N))
      ((fun (f : (i : ι) × η i →₀ N) ↦
          (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
              (Trunc.mk
                (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                  f.splitSupport (αs := η).val ⋯)) :
            Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : (i : ι) × η i →₀ N
a : (i : ι) × η i
⊢ Eq.{u_5 + 1} (α := N)
    (((fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
              (onFinset
                  (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
                    ((f : (a : ι) → η a →₀ N) j).support)
                  (fun (ji : (i : ι) × η i) ↦
                    ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                      (ji.snd (β := fun (i : ι) ↦ η i)))
                  ⋯ :
                (i : ι) × η i →₀ N))
            ((fun (f : (i : ι) × η i →₀ N) ↦
                (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
                    (Trunc.mk
                      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                        f.splitSupport (αs := η).val ⋯)) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
              f) :
          (a : (i : ι) × η i) → N)
        a :
      N)
    ((f : (a : (i : ι) × η i) → N) a : N)

Tactic:
simp [split]

Premises used: Finsupp.split
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
h :
  ∀ (i : ι) (a : η i),
    Eq.{u_5 + 1} (α := N)
      ((((fun (f : (i : ι) × η i →₀ N) ↦
                    (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
                        (Trunc.mk
                          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                            f.splitSupport (αs := η).val ⋯)) :
                      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
                  ((fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
                      (onFinset
                          (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
                            ((f : (a : ι) → η a →₀ N) j).support)
                          (fun (ji : (i : ι) × η i) ↦
                            ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                              (ji.snd (β := fun (i : ι) ↦ η i)))
                          ⋯ :
                        (i : ι) × η i →₀ N))
                    f) :
                (a : ι) → η a →₀ N)
              i :
            (a : η i) → N)
          a :
        N)
      (((f : (a : ι) → η a →₀ N) i : (a : η i) → N) a : N)
⊢ (fun (f : (i : ι) × η i →₀ N) ↦
        (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
            (Trunc.mk
              (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                f.splitSupport (αs := η).val ⋯)) :
          Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
      ((fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
          (onFinset
              (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
                ((f : (a : ι) → η a →₀ N) j).support)
              (fun (ji : (i : ι) × η i) ↦
                ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                  (ji.snd (β := fun (i : ι) ↦ η i)))
              ⋯ :
            (i : ι) × η i →₀ N))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
i : ι
a : η i
⊢ Eq.{u_5 + 1} (α := N)
    ((((fun (f : (i : ι) × η i →₀ N) ↦
                  (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
                      (Trunc.mk
                        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                          f.splitSupport (αs := η).val ⋯)) :
                    Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
                ((fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
                    (onFinset
                        (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
                          ((f : (a : ι) → η a →₀ N) j).support)
                        (fun (ji : (i : ι) × η i) ↦
                          ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                            (ji.snd (β := fun (i : ι) ↦ η i)))
                        ⋯ :
                      (i : ι) × η i →₀ N))
                  f) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)
    (((f : (a : ι) → η a →₀ N) i : (a : η i) → N) a : N)

Tactic:
simp [split]

Premises used: Finsupp.split
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : Zero N
f : (i : ι) × η i →₀ N
⊢ (⇑((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
          Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
      (a : ι) → η a →₀ N) =
    f.split (αs := η)

Tactic:
rfl

Premises used: Finsupp.comapDomain, rfl, Finsupp.split
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
s : (i : ι) × η i
⊢ Eq.{u_5 + 1} (α := N)
    ((((Equiv.symm (sigmaFinsuppEquivDFinsupp (η := η)) : (a : Π₀ (i : ι), η i →₀ N) → (i : ι) × η i →₀ N) f :
            (i : ι) × η i →₀ N) :
          (a : (i : ι) × η i) → N)
        s :
      N)
    (((f : (a : ι) → η a →₀ N) (s.fst (β := fun (i : ι) ↦ η i)) : (a : η s.fst) → N) (s.snd (β := fun (i : ι) ↦ η i)) :
      N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
inst_2 : (i : ι) → (x : Finsupp.{u_4, u_5} (η i) N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
h :
  ∀ (a : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
          ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f))
        a ↔
      a ∈ f.splitSupport (αs := η)
⊢ DFinsupp.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f) =
    f.splitSupport (αs := η)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
inst_2 : (i : ι) → (x : Finsupp.{u_4, u_5} (η i) N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a : ι
h :
  (((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
            Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
          (a : ι) → η a →₀ N)
        a ≠
      0 ↔
    a ∈ f.splitSupport (αs := η)
⊢ Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
        ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f))
      a ↔
    a ∈ f.splitSupport (αs := η)

Tactic:
rw [DFinsupp.mem_support_toFun]

Premises used: DFinsupp.mem_support_toFun
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
inst_2 : (i : ι) → (x : Finsupp.{u_4, u_5} (η i) N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a : ι
⊢ (((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
            Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
          (a : ι) → η a →₀ N)
        a ≠
      0 ↔
    a ∈ f.splitSupport (αs := η)

Tactic:
(Finsupp.mem_splitSupport_iff_nonzero _ _).symm

Premises used: Finsupp.comapDomain, Iff.symm, Finsupp.mem_splitSupport_iff_nonzero, Finsupp.split
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
inst_2 : (i : ι) → (x : Finsupp.{u_4, u_5} (η i) N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a : ι
⊢ (((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
            Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
          (a : ι) → η a →₀ N)
        a ≠
      0 ↔
    a ∈ f.splitSupport (αs := η)

Tactic:
exact (Finsupp.mem_splitSupport_iff_nonzero _ _).symm

Premises used: Iff.symm, Finsupp.mem_splitSupport_iff_nonzero
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
a : (i : ι) × η i
n : N
obtain :
  ∀ (i : ι) (a : η i),
    Eq (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
          (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
        Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
      (DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
          ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
          (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
        Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
⊢ Eq (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (single a n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    (DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (a.fst (β := fun (i : ι) ↦ η i))
        (single (a.snd (β := fun (i : ι) ↦ η i)) n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)

Tactic:
obtain ⟨i, a⟩ := a
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
h :
  ∀ (j : ι) (b : η j),
    Eq.{u_5 + 1} (α := N)
      (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                    (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              j :
            (a : η j) → N)
          b :
        N)
      (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                  ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                  (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
                (a : ι) → η a →₀ N)
              j :
            (a : η j) → N)
          b :
        N)
⊢ Eq (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
        (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    (DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
        ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
        (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)

Tactic:
ext j b
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
pos :
  ∀ (h : i = j),
    Eq.{u_5 + 1} (α := N)
      (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                    (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              j :
            (a : η j) → N)
          b :
        N)
      (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                  ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                  (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
                (a : ι) → η a →₀ N)
              j :
            (a : η j) → N)
          b :
        N)
neg :
  ∀ (h : ¬i = j),
    Eq.{u_5 + 1} (α := N)
      (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                    (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              j :
            (a : η j) → N)
          b :
        N)
      (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                  ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                  (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
                (a : ι) → η a →₀ N)
              j :
            (a : η j) → N)
          b :
        N)
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
pos :
  ∀ (b : η i),
    Eq.{u_5 + 1} (α := N)
      (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                    (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              i :
            (a : η i) → N)
          b :
        N)
      (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                  ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                  (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
                (a : ι) → η a →₀ N)
              i :
            (a : η i) → N)
          b :
        N)
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)

Tactic:
subst h
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a b : η i
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        b :
      N)

Tactic:
simp [split_apply, Finsupp.single_apply]

Premises used: Finsupp.split_apply, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a b : η i
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        b :
      N)

Tactic:
classical simp [split_apply, Finsupp.single_apply]

Premises used: Finsupp.split_apply, Finsupp.single_apply