[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
⊢ toDFinsupp (single i m) = DFinsupp.single i m
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
i✝ : ι
⊢ ↑(toDFinsupp (single i m)) i✝ = ↑(DFinsupp.single i m) i✝
[PROOFSTEP]
simp [Finsupp.single_apply, DFinsupp.single_apply]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
⊢ DFinsupp.support (Finsupp.toDFinsupp f) = f.support
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a✝ : ι
⊢ a✝ ∈ DFinsupp.support (Finsupp.toDFinsupp f) ↔ a✝ ∈ f.support
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
i : ι
⊢ i ∈ support f ↔ ↑f i ≠ 0
[PROOFSTEP]
simp only [DFinsupp.mem_support_iff]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ (toFinsupp f).support = support f
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a✝ : ι
⊢ a✝ ∈ (toFinsupp f).support ↔ a✝ ∈ support f
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ toFinsupp (single i m) = Finsupp.single i m
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a✝ : ι
⊢ ↑(toFinsupp (single i m)) a✝ = ↑(Finsupp.single i m) a✝
[PROOFSTEP]
simp [Finsupp.single_apply, DFinsupp.single_apply]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : (m : M) → Decidable (m ≠ 0)
inst✝ : Module R M
⊢ ↑(finsuppLequivDFinsupp R) = Finsupp.toDFinsupp
[PROOFSTEP]
simp only [@LinearEquiv.coe_coe]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : (m : M) → Decidable (m ≠ 0)
inst✝ : Module R M
⊢ ↑(finsuppLequivDFinsupp R) = Finsupp.toDFinsupp
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ i ∈ (splitSupport f).val ∨ split f i = 0
[PROOFSTEP]
rw [← Finset.mem_def, mem_splitSupport_iff_nonzero]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ split f i ≠ 0 ∨ split f i = 0
[PROOFSTEP]
exact (em _).symm
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
⊢ (i : ι) × η i →₀ N
[PROOFSTEP]
haveI := Classical.decEq ι
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this : DecidableEq ι
⊢ (i : ι) × η i →₀ N
[PROOFSTEP]
haveI := fun i => Classical.decEq (η i →₀ N)
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
⊢ (i : ι) × η i →₀ N
[PROOFSTEP]
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⟩
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0
⊢ g.fst ∈ DFinsupp.support f
[PROOFSTEP]
simp only [Ne.def, DFinsupp.mem_support_toFun]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0
⊢ ¬↑f g.fst = 0
[PROOFSTEP]
intro h
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0
h : ↑f g.fst = 0
⊢ False
[PROOFSTEP]
dsimp at hg 
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : ¬↑(↑f g.fst) g.snd = 0
h : ↑f g.fst = 0
⊢ False
[PROOFSTEP]
rw [h] at hg 
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : ¬↑0 g.snd = 0
h : ↑f g.fst = 0
⊢ False
[PROOFSTEP]
simp only [coe_zero, Pi.zero_apply, not_true] at hg 
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
⊢ (fun f =>
        onFinset (Finset.sigma (DFinsupp.support f) fun j => (↑f j).support) (fun ji => ↑(↑f ji.fst) ji.snd)
          (_ :
            ∀ (g : (i : ι) × η i),
              (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0 → g ∈ Finset.sigma (DFinsupp.support f) fun j => (↑f j).support))
      ((fun f =>
          { toFun := split f,
            support' :=
              Trunc.mk
                { val := (splitSupport f).val,
                  property := (_ : ∀ (i : ι), i ∈ (splitSupport f).val ∨ split f i = 0) } })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
a✝ : (i : ι) × η i
⊢ ↑((fun f =>
            onFinset (Finset.sigma (DFinsupp.support f) fun j => (↑f j).support) (fun ji => ↑(↑f ji.fst) ji.snd)
              (_ :
                ∀ (g : (i : ι) × η i),
                  (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0 →
                    g ∈ Finset.sigma (DFinsupp.support f) fun j => (↑f j).support))
          ((fun f =>
              { toFun := split f,
                support' :=
                  Trunc.mk
                    { val := (splitSupport f).val,
                      property := (_ : ∀ (i : ι), i ∈ (splitSupport f).val ∨ split f i = 0) } })
            f))
      a✝ =
    ↑f a✝
[PROOFSTEP]
simp [split]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
⊢ (fun f =>
        { toFun := split f,
          support' :=
            Trunc.mk
              { val := (splitSupport f).val, property := (_ : ∀ (i : ι), i ∈ (splitSupport f).val ∨ split f i = 0) } })
      ((fun f =>
          onFinset (Finset.sigma (DFinsupp.support f) fun j => (↑f j).support) (fun ji => ↑(↑f ji.fst) ji.snd)
            (_ :
              ∀ (g : (i : ι) × η i),
                (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0 → g ∈ Finset.sigma (DFinsupp.support f) fun j => (↑f j).support))
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑((fun f =>
                { toFun := split f,
                  support' :=
                    Trunc.mk
                      { val := (splitSupport f).val,
                        property := (_ : ∀ (i : ι), i ∈ (splitSupport f).val ∨ split f i = 0) } })
              ((fun f =>
                  onFinset (Finset.sigma (DFinsupp.support f) fun j => (↑f j).support) (fun ji => ↑(↑f ji.fst) ji.snd)
                    (_ :
                      ∀ (g : (i : ι) × η i),
                        (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0 →
                          g ∈ Finset.sigma (DFinsupp.support f) fun j => (↑f j).support))
                f))
          i✝)
      a✝ =
    ↑(↑f i✝) a✝
[PROOFSTEP]
simp [split]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
⊢ DFinsupp.support (↑sigmaFinsuppEquivDFinsupp f) = splitSupport f
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ a✝ ∈ DFinsupp.support (↑sigmaFinsuppEquivDFinsupp f) ↔ a✝ ∈ splitSupport f
[PROOFSTEP]
rw [DFinsupp.mem_support_toFun]
[GOAL]
case a
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ ↑(↑sigmaFinsuppEquivDFinsupp f) a✝ ≠ 0 ↔ a✝ ∈ splitSupport f
[PROOFSTEP]
exact (Finsupp.mem_splitSupport_iff_nonzero _ _).symm
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
a : (i : ι) × η i
n : N
⊢ ↑sigmaFinsuppEquivDFinsupp (single a n) = DFinsupp.single a.fst (single a.snd n)
[PROOFSTEP]
obtain ⟨i, a⟩ := a
[GOAL]
case mk
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
⊢ ↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n) =
    DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)
[PROOFSTEP]
ext j b
[GOAL]
case mk.h.h
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) i) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) i) b
[PROOFSTEP]
classical simp [split_apply, Finsupp.single_apply]
[GOAL]
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) i) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) i) b
[PROOFSTEP]
simp [split_apply, Finsupp.single_apply]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
[PROOFSTEP]
suffices Finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
this : ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
[PROOFSTEP]
simp [split_apply, dif_neg h, this]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
[PROOFSTEP]
have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ { fst := i, snd := a } ≠ { fst := j, snd := b }
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : { fst := i, snd := a } ≠ { fst := j, snd := b }
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
[PROOFSTEP]
classical rw [Finsupp.single_apply, if_neg H]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : { fst := i, snd := a } ≠ { fst := j, snd := b }
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
[PROOFSTEP]
rw [Finsupp.single_apply, if_neg H]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
⊢ ↑sigmaFinsuppEquivDFinsupp (f + g) = ↑sigmaFinsuppEquivDFinsupp f + ↑sigmaFinsuppEquivDFinsupp g
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (f + g)) i✝) a✝ =
    ↑(↑(↑sigmaFinsuppEquivDFinsupp f + ↑sigmaFinsuppEquivDFinsupp g) i✝) a✝
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R✝ : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R✝
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
⊢ ↑sigmaFinsuppEquivDFinsupp (r • f) = SMul.smul r (↑sigmaFinsuppEquivDFinsupp f)
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
R✝ : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R✝
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (r • f)) i✝) a✝ = ↑(↑(SMul.smul r (↑sigmaFinsuppEquivDFinsupp f)) i✝) a✝
[PROOFSTEP]
rfl
