-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
mk :
  ∀ x ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf) : Multiset ι).toFinset,
    Eq.{w + 1} (α := γ)
      ((φ x : (a : β x) → γ)
          ((mk' (β := fun (i : ι) ↦ β i) f
                (Quot.mk
                  (⇑trueSetoid :
                    { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } →
                      { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } → Prop)
                  (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf)) :
              (a : ι) → β a)
            x) :
        γ)
      (if
            (mk' (β := fun (i : ι) ↦ β i) f
                    (Quot.mk
                      (⇑trueSetoid :
                        { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } →
                          { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } → Prop)
                      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf)) :
                  (a : ι) → β a)
                x ≠
              0 then
          (fun (x : ι) ↦ ((⇑(φ x) : (a : β x) → γ) : (a : β x) → γ)) x
            ((mk' (β := fun (i : ι) ↦ β i) f
                  (Quot.mk
                    (⇑trueSetoid :
                      { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } →
                        { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } → Prop)
                    (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf)) :
                (a : ι) → β a)
              x)
        else 0 :
        γ)
⊢ Eq.{w + 1} (α := γ)
    (∑ i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf) : Multiset ι).toFinset,
      (φ i : (a : β i) → γ)
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Quot.mk
                (⇑trueSetoid :
                  { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } →
                    { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } → Prop)
                (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf)) :
            (a : ι) → β a)
          i))
    (∑ i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf) : Multiset ι).toFinset with
      (mk' (β := fun (i : ι) ↦ β i) f
              (Quot.mk
                (⇑trueSetoid :
                  { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } →
                    { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } → Prop)
                (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf)) :
            (a : ι) → β a)
          i ≠
        0,
      (fun (x : ι) ↦ ((⇑(φ x) : (a : β x) → γ) : (a : β x) → γ)) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Quot.mk
                (⇑trueSetoid :
                  { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } →
                    { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 } → Prop)
                (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf)) :
            (a : ι) → β a)
          i))

Tactic:
rw [Finset.sum_filter, Finset.sum_congr rfl]

Premises used: Finset.sum_filter, Finset.sum_congr, rfl