-- Module: Mathlib.Data.DFinsupp.BigOperators
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{v, w} (β i) γ
f : (i : ι) → β i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
mk :
  ∑
      i ∈
        Multiset.toFinset
          (↑((fun
                    (ys :
                      { s : Multiset ι //
                        ∀ (i : ι),
                          i ∈ s ∨
                            toFun (β := fun (i : ι) ↦ β i)
                                (mk' (β := fun (i : ι) ↦ β i) g
                                  (Quot.mk
                                    (⇑trueSetoid :
                                      { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } →
                                        { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } → Prop)
                                    (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg hg)))
                                i =
                              0 }) ↦
                  (Subtype.mk (p := fun (s : Multiset ι) ↦
                      ∀ (i : ι),
                        i ∈ s ∨
                          Eq.{v + 1} (α := β i)
                            ((fun (i : ι) ↦
                                ((fun (x : ι) (x1 x2 : β x) ↦ x1 + x2) 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) sf
                                              hf)) :
                                        (a : ι) → β a)
                                      i)
                                    ((mk' (β := fun (i : ι) ↦ β i) g
                                          (Quot.mk
                                            (⇑trueSetoid :
                                              { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } →
                                                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } → Prop)
                                            (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg
                                              hg)) :
                                        (a : ι) → β a)
                                      i) :
                                  β i))
                              i)
                            0)
                      ((↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) sf hf) : Multiset ι) +
                        (↑ys : Multiset ι))
                      ⋯ :
                    { s : Multiset ι //
                      ∀ (i : ι),
                        i ∈ s ∨
                          Eq.{v + 1} (α := β i)
                            ((fun (i : ι) ↦
                                ((fun (x : ι) (x1 x2 : β x) ↦ x1 + x2) 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) sf
                                              hf)) :
                                        (a : ι) → β a)
                                      i)
                                    ((mk' (β := fun (i : ι) ↦ β i) g
                                          (Quot.mk
                                            (⇑trueSetoid :
                                              { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } →
                                                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } → Prop)
                                            (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg
                                              hg)) :
                                        (a : ι) → β a)
                                      i) :
                                  β i))
                              i)
                            0 }))
                (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg hg)) :
            Multiset ι),
      ((fun (i : ι) ↦ (↑(φ i) : ZeroHom (β i) γ)) i : (a : β i) → γ)
        ((HAdd.hAdd (α := Π₀ (i : ι), β 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) sf hf)))
              (mk' (β := fun (i : ι) ↦ β i) g
                (Quot.mk
                  (⇑trueSetoid :
                    { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } →
                      { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } → Prop)
                  (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg hg))) :
            (a : ι) → β a)
          i) =
    HAdd.hAdd (α := γ)
      (∑ i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) sf hf) : Multiset ι).toFinset,
        ((fun (i : ι) ↦ (↑(φ i) : ZeroHom (β i) γ)) 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) sf hf)) :
              (a : ι) → β a)
            i))
      (∑ i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg hg) : Multiset ι).toFinset,
        ((fun (i : ι) ↦ (↑(φ i) : ZeroHom (β i) γ)) i : (a : β i) → γ)
          ((mk' (β := fun (i : ι) ↦ β i) g
                (Quot.mk
                  (⇑trueSetoid :
                    { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } →
                      { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } → Prop)
                  (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg hg)) :
              (a : ι) → β a)
            i))
⊢ ZeroHom.toFun (sumZeroHom (β := β) fun (i : ι) ↦ (↑(φ i) : ZeroHom (β i) γ))
      (HAdd.hAdd (α := Π₀ (i : ι), β 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) sf hf)))
        (mk' (β := fun (i : ι) ↦ β i) g
          (Quot.mk
            (⇑trueSetoid :
              { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } →
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } → Prop)
            (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg hg)))) =
    HAdd.hAdd (α := γ)
      (ZeroHom.toFun (M := Π₀ (i : ι), β i) (sumZeroHom (β := β) fun (i : ι) ↦ (↑(φ i) : ZeroHom (β 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) sf hf))))
      (ZeroHom.toFun (M := Π₀ (i : ι), β i) (sumZeroHom (β := β) fun (i : ι) ↦ (↑(φ i) : ZeroHom (β i) γ))
        (mk' (β := fun (i : ι) ↦ β i) g
          (Quot.mk
            (⇑trueSetoid :
              { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } →
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ g i = 0 } → Prop)
            (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ g i = 0) sg hg))))

Tactic:
change (∑ i ∈ _, _) = (∑ i ∈ _, _) + ∑ i ∈ _, _

Premises used: Finset.sum