-- Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Finite ι
inst_1 : Semiring R
inst_2 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_3 : AddCommMonoid N
inst_4 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_5 : Module R N
inst_6 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j) fun (i : ι) ↦
        DFinsupp.lsingle (M := M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j) fun (i : ι) ↦
        DFinsupp.lsingle (M := M i) (p i))
x : (i : ι) → Π₀ (j : κ i), M i j
H :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
H₁ :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N)
      ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
        N)
      ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          (fun (i : ι) ↦ ((x i).sum (β := M i) (DFinsupp.single (β := M i)) : Π₀ (i_1 : κ i), M i i_1)) i :
        N)
H₂ :
  ∀ (val : Fintype ι),
    Eq.{uN + 1} (α := N)
      (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
        (f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
      (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i),
        (g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
          DFinsupp.single (β := M i) (r i) ((x i : (a : κ i) → M i a) (r i)))
H₃ :
  ∀ (val : Fintype ι) (p : (a : ι) → κ a),
    Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i)) p →
      Eq.{uN + 1} (α := N)
        ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
            DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
          N)
        ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
            DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
          N)
H₄ :
  ∀ (val : Fintype ι) (p : (a : ι) → κ a),
    Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i)) p →
      ∀
        (h :
          ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
            Eq.{uN + 1} (α := N)
              ((f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j) fun (i : ι) ↦
                      DFinsupp.lsingle (M := M i) (p i) :
                    (a : (i : ι) → M i (p i)) → N)
                  x :
                N)
              ((g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j) fun (i : ι) ↦
                      DFinsupp.lsingle (M := M i) (p i) :
                    (a : (i : ι) → M i (p i)) → N)
                  x :
                N)),
        Eq.{uN + 1} (α := N)
          ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
              DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
            N)
          ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦
              DFinsupp.single (β := M i) (p i) ((x i : (a : κ i) → M i a) (p i)) :
            N)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → Π₀ (j : κ i), M i j) → N) fun (i : ι) ↦ x i : N)

Tactic:
classical
  cases nonempty_fintype ι
  rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]
  simp_rw [DFinsupp.sum, MultilinearMap.map_sum_finset]
  congr! 1 with p
  simp_rw [MultilinearMap.ext_iff] at h
  exact h _ _

Premises used: DFinsupp.sum, nonempty_fintype, MultilinearMap.ext_iff, MultilinearMap.map_sum_finset