-- 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
i : ι
mk :
  i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf) : Multiset ι).toFinset →
    Eq.{w + 1} (α := γ)
      ((φ 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) :
        γ)
      (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)
                i ≠
              0 then
          (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)
        else 0 :
        γ)
⊢ i ∈ (↑(Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s hf) : Multiset ι).toFinset →
    Eq.{w + 1} (α := γ)
      ((φ 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) :
        γ)
      (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)
                i ≠
              0 then
          (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)
        else 0 :
        γ)

Tactic:
_