-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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
⊢ ∑
      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))
have mk : HAdd.hAdd (α := γ) (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (f x))
    (∑ x ∈ (sf + sg).toFinset, (φ x : (a : β x) → γ) (g x)) =
  HAdd.hAdd (α := γ) (∑ x ∈ sf.toFinset, (φ x : (a : β x) → γ) (f x)) (∑ x ∈ sg.toFinset, (φ x : (a : β x) → γ) (g x))
Tactic: simp only [AddMonoidHom.toZeroHom_coe, coe_add, coe_mk', Pi.add_apply, map_add,
      Finset.sum_add_distrib]