-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
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))
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
⊢ 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)

Tactic:
classical
  refine (DFinsupp.sumAddHom_apply _ _).trans ?_
  refine Finset.sum_subset (MultilinearMap.support_dfinsuppFamily_subset _ _) ?_
  simp

Premises used: Finset.sum_subset, MultilinearMap.support_dfinsuppFamily_subset, DFinsupp.sumAddHom_apply, Eq.trans