-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ (DFinsupp.mk' (β := fun (t : (i : ι) → κ i) ↦ N t)
          (fun (p : (i : ι) → κ i) ↦
            (f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
              (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_1 : (a : κ i_1) → M i_1 a)
                (p i_1))
          (Trunc.map
            (fun
                (s :
                  (i_1 : ι) →
                    { s : Multiset (κ i_1) //
                      ∀ (i_2 : κ i_1),
                        i_2 ∈ s ∨
                          (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_1).toFun (β :=
                              fun (j : κ i_1) ↦ M i_1 j) i_2 =
                            0 }) ↦
              Subtype.mk (p := fun (s : Multiset ((i : ι) → κ i)) ↦
                ∀ (i_1 : (i : ι) → κ i),
                  i_1 ∈ s ∨
                    Eq.{uN + 1} (α := N i_1)
                      ((f i_1 : (a : (i : ι) → M i (i_1 i)) → N i_1) fun (i_2 : ι) ↦
                        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_2 :
                            (a : κ i_2) → M i_2 a)
                          (i_1 i_2))
                      0)
                (Multiset.map
                  (fun (f : (a : ι) → Membership.mem (γ := Multiset ι) (Finset.val Finset.univ) a → κ a) (i : ι) ↦
                    f i ⋯)
                  (Multiset.pi (β := κ) (Finset.val Finset.univ) fun (i_1 : ι) ↦ (↑(s i_1) : Multiset (κ i_1))))
                ⋯)
            (Trunc.finChoice (α := fun (i_1 : ι) ↦
              { s : Multiset (κ i_1) //
                ∀ (i_2 : κ i_1),
                  i_2 ∈ s ∨
                    (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_1).toFun (β :=
                        fun (j : κ i_1) ↦ M i_1 j) i_2 =
                      0 })
              fun (i_1 : ι) ↦
              (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_1).support' (β :=
                fun (j : κ i_1) ↦ M i_1 j))) :
        (a : (i : ι) → κ i) → N a)
      p =
    (HSMul.hSMul (β := Π₀ (t : (i : ι) → κ i), N t) c
          (DFinsupp.mk' (β := fun (t : (i : ι) → κ i) ↦ N t)
            (fun (p : (i : ι) → κ i) ↦
              (f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
                (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1 : (a : κ i_1) → M i_1 a) (p i_1))
            (Trunc.map
              (fun
                  (s :
                    (i_1 : ι) →
                      { s : Multiset (κ i_1) //
                        ∀ (i_2 : κ i_1),
                          i_2 ∈ s ∨
                            (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1).toFun (β :=
                                fun (j : κ i_1) ↦ M i_1 j) i_2 =
                              0 }) ↦
                Subtype.mk (p := fun (s : Multiset ((i : ι) → κ i)) ↦
                  ∀ (i_1 : (i : ι) → κ i),
                    i_1 ∈ s ∨
                      Eq.{uN + 1} (α := N i_1)
                        ((f i_1 : (a : (i : ι) → M i (i_1 i)) → N i_1) fun (i_2 : ι) ↦
                          (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_2 : (a : κ i_2) → M i_2 a)
                            (i_1 i_2))
                        0)
                  (Multiset.map
                    (fun (f : (a : ι) → Membership.mem (γ := Multiset ι) (Finset.val Finset.univ) a → κ a) (i : ι) ↦
                      f i ⋯)
                    (Multiset.pi (β := κ) (Finset.val Finset.univ) fun (i_1 : ι) ↦ (↑(s i_1) : Multiset (κ i_1))))
                  ⋯)
              (Trunc.finChoice (α := fun (i_1 : ι) ↦
                { s : Multiset (κ i_1) //
                  ∀ (i_2 : κ i_1),
                    i_2 ∈ s ∨
                      (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1).toFun (β := fun (j : κ i_1) ↦
                          M i_1 j) i_2 =
                        0 })
                fun (i_1 : ι) ↦
                (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1).support' (β := fun (j : κ i_1) ↦
                  M i_1 j)))) :
        (a : (i : ι) → κ i) → N a)
      p
have dsimp : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_1 : (a : κ i_1) → M i_1 a) (p i_1)) =
  HSMul.hSMul (β := N p) c
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1 : (a : κ i_1) → M i_1 a) (p i_1))
Tactic: dsimp