-- 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
⊢ 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))))
have 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 ι))
                    sorry :
                  { 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))
Tactic: change (∑ i ∈ _, _) = (∑ i ∈ _, _) + ∑ i ∈ _, _