-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
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)
⊢ 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)
have 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)
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 _ _
Cleared hypotheses: h