-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
N : Type u_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, u_1} R (fun (i : ι) ↦ M i (p i)) N
x : (i : ι) → Π₀ (j : κ i), M i j
refine :
  Eq.{u_1 + 1} (α := N)
    (DFinsupp.sum (β := fun (a : (i : ι) → κ i) ↦ N)
      ((((dfinsuppFamilyₗ (κ := κ) (M := M) (N := fun (p : (i : ι) → κ i) ↦ N) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N))
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N)) :
          (a : (i : ι) → (fun (i : ι) ↦ Π₀ (j : κ i), M i j) i) → Π₀ (i : (i : ι) → κ i), N)
        x)
      fun (x : (i : ι) → κ i) ↦
      (⇑(LinearMap.toAddMonoidHom.{uR, uR, u_1, u_1} (R := R) (S := R) (modM₁ := (fun (x : (i : ι) → κ i) ↦ inst_6) x)
            (modM₂ := inst_6) (σ := RingHom.id R) ((fun (x : (i : ι) → κ i) ↦ (LinearMap.id : N →ₗ[R] N)) x)) :
        (a : N) → N))
    (∑ p ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
      (f p : (a : (i : ι) → M i (p i)) → N) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i))
⊢ Eq.{u_1 + 1} (α := N)
    ((((fromDFinsuppEquiv κ R (M := M) :
                (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                  MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N)
              f :
            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N) :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → N)
        x :
      N)
    (∑ p ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
        (f p : (a : (i : ι) → M i (p i)) → N) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i) :
      N)
have refine₁ : ∀ (x_1 : (i : ι) → κ i),
  Membership.mem (γ := Finset ((i : ι) → κ i)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i)) x_1 →
    x_1 ∉
        DFinsupp.support (β := fun (a : (i : ι) → κ i) ↦ N)
          ((((dfinsuppFamilyₗ (κ := κ) (M := M) (N := fun (p : (i : ι) → κ i) ↦ N) :
                    (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                      MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N))
                  f :
                MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N)) :
              (a : (i : ι) → (fun (i : ι) ↦ Π₀ (j : κ i), M i j) i) → Π₀ (i : (i : ι) → κ i), N)
            x) →
      Eq.{u_1 + 1} (α := N)
        ((fun (x : (i : ι) → κ i) ↦
            ((⇑(LinearMap.toAddMonoidHom.{uR, uR, u_1, u_1} (R := R) (S := R) (modM₁ :=
                    (fun (x : (i : ι) → κ i) ↦ inst_6) x) (modM₂ := inst_6) (σ := RingHom.id R)
                    ((fun (x : (i : ι) → κ i) ↦ (LinearMap.id : N →ₗ[R] N)) x)) :
                (a : N) → N) :
              (a : N) → N))
          x_1
          ((((((dfinsuppFamilyₗ (κ := κ) (M := M) (N := fun (p : (i : ι) → κ i) ↦ N) :
                          (a : (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) N) →
                            MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N))
                        f :
                      MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (i : (i : ι) → κ i), N)) :
                    (a : (i : ι) → (fun (i : ι) ↦ Π₀ (j : κ i), M i j) i) → Π₀ (i : (i : ι) → κ i), N)
                  x :
                Π₀ (i : (i : ι) → κ i), N) :
              (a : (i : ι) → κ i) → N)
            x_1))
        0
Tactic: classical
  refine (DFinsupp.sumAddHom_apply _ _).trans ?_
  refine Finset.sum_subset (MultilinearMap.support_dfinsuppFamily_subset _ _) ?_
  simp