case a
ι : Type u_1
R : Type ?u.69432
M : Type ?u.69435
η : ι → Type u_3
N : Type u_2
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
ι : Type u_1
R : Type ?u.69432
M : Type ?u.69435
η : ι → Type u_3
N : Type u_2
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
ext
case a
ι : Type u_1
R : Type ?u.69432
M : Type ?u.69435
η : ι → Type u_3
N : Type u_2
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
case a
ι : Type u_1
R : Type ?u.69432
M : Type ?u.69435
η : ι → Type u_3
N : Type u_2
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
rw [Dfinsupp.mem_support_toFun]
no goals
case a
ι : Type u_1
R : Type ?u.69432
M : Type ?u.69435
η : ι → Type u_3
N : Type u_2
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
exact (Finsupp.mem_splitSupport_iff_nonzero _ _).symm