-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R
intro intro₁ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ ((e i).repr.symm : (a : ιM i →₀ R) → M i) (x i) : N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ ((e i).repr.symm : (a : ιM i →₀ R) → M i) (x i) : N)
intro₂ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (Finsupp.linearCombination R (⇑(e i) : (a : ιM i) → M i) : (a : ιM i →₀ R) → M i) (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (Finsupp.linearCombination R (⇑(e i) : (a : ιM i) → M i) : (a : ιM i →₀ R) → M i) (x i) :
      N)
intro₃ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (x i).sum fun (i_1 : ιM i) (a : R) ↦ HSMul.hSMul (β := M i) a ((e i : (a : ιM i) → M i) i_1 : M i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (x i).sum fun (i_1 : ιM i) (a : R) ↦ HSMul.hSMul (β := M i) a ((e i : (a : ιM i) → M i) i_1 : M i) :
      N)
intro₄ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        ∑ x_1 ∈ (x i).support,
          HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M i) ((x i : (a : ιM i) → R) x_1 : R)
            ((e i : (a : ιM i) → M i) x_1 : M i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        ∑ x_1 ∈ (x i).support,
          HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M i) ((x i : (a : ιM i) → R) x_1 : R)
            ((e i : (a : ιM i) → M i) x_1 : M i) :
      N)
intro₅ :
  Eq.{u_4 + 1} (α := N)
    (∑ r ∈ Fintype.piFinset (δ := ιM) fun (i : ι) ↦ (x i).support,
      (f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M i) ((x i : (a : ιM i) → R) (r i) : R)
          ((e i : (a : ιM i) → M i) (r i) : M i))
    (∑ r ∈ Fintype.piFinset (δ := ιM) fun (i : ι) ↦ (x i).support,
      (g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M i) ((x i : (a : ιM i) → R) (r i) : R)
          ((e i : (a : ιM i) → M i) (r i) : M i))
⊢ Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
have intro₆ : Eq.{u_4 + 1} (α := N)
  (∑ x_1 ∈ Fintype.piFinset (δ := ιM) fun (i : ι) ↦ (x i).support,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (∏ i : ι, (x i : (a : ιM i) → R) (x_1 i))
      ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (x_1 i) : N))
  (∑ x_1 ∈ Fintype.piFinset (δ := ιM) fun (i : ι) ↦ (x i).support,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (∏ i : ι, (x i : (a : ιM i) → R) (x_1 i))
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (x_1 i) : N))
Tactic: simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]