-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ 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))
have 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 :
      γ)
Tactic: rw [Finset.sum_filter, Finset.sum_congr rfl]