-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp (goal)
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : (i : ι) → DecidableEq (κ i)
⊢ Eq (α := (⨂[R] (i : ι), Π₀ (j : κ i), M i j) →ₗ[R] ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
    (((DFinsupp.lsum R (M := fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) :
          (a : (i : (i : ι) → κ i) → (⨂[R] (i_1 : ι), M i_1 (i i_1)) →ₗ[R] ⨂[R] (i : ι), Π₀ (j : κ i), M i j) →
            (Π₀ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) →ₗ[R] ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
        fun (p : (i : ι) → κ i) ↦
        (lift (s := fun (i : ι) ↦ M i (p i)) :
            (a : MultilinearMap R (fun (i : ι) ↦ M i (p i)) (⨂[R] (i : ι), Π₀ (j : κ i), M i j)) →
              (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
          (compMultilinearMap (M₁ := fun (i : ι) ↦ M i (p i))
            (map (s := fun (i : ι) ↦ M i (p i)) (t := fun (i : ι) ↦ Π₀ (i_1 : κ i), M i i_1) fun (i : ι) ↦
              DFinsupp.lsingle (M := M i) (p i))
            (tprod R (s := fun (i : ι) ↦ M i (p i))))) ∘ₗ
      (lift (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j) :
          (a : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))) →
            (⨂[R] (i : ι), Π₀ (j : κ i), M i j) →ₗ[R] Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
        ((MultilinearMap.fromDFinsuppEquiv κ R (M := M) :
            (a :
                (p : (i : ι) → κ i) →
                  MultilinearMap R (fun (i : ι) ↦ M i (p i)) (Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))) →
              MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) (Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)))
          fun (p : (i : ι) → κ i) ↦
          compMultilinearMap (M₁ := fun (i : ι) ↦ M i (p i))
            (DFinsupp.lsingle (R := R) (M := fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p)
            (tprod R (s := fun (i : ι) ↦ M i (p i)))))
    LinearMap.id
have H : ∀ (x : (i : ι) → κ i) (x_1 : (i : ι) → M i (x i)),
  Eq (α := ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
    ((MultilinearMap.compLinearMap (M₁ := fun (i : ι) ↦ M i (x i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
            (compMultilinearMap (M₁ := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
              (((DFinsupp.lsum R (M := fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) :
                    (a :
                        (i : (i : ι) → κ i) → (⨂[R] (i_1 : ι), M i_1 (i i_1)) →ₗ[R] ⨂[R] (i : ι), Π₀ (j : κ i), M i j) →
                      (Π₀ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) →ₗ[R] ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
                  fun (p : (i : ι) → κ i) ↦
                  (lift (s := fun (i : ι) ↦ M i (p i)) :
                      (a : MultilinearMap R (fun (i : ι) ↦ M i (p i)) (⨂[R] (i : ι), Π₀ (j : κ i), M i j)) →
                        (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
                    (compMultilinearMap (M₁ := fun (i : ι) ↦ M i (p i))
                      (map (s := fun (i : ι) ↦ M i (p i)) (t := fun (i : ι) ↦ Π₀ (i_1 : κ i), M i i_1) fun (i : ι) ↦
                        DFinsupp.lsingle (M := M i) (p i))
                      (tprod R (s := fun (i : ι) ↦ M i (p i))))) ∘ₗ
                (lift (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j) :
                    (a :
                        MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j)
                          (Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))) →
                      (⨂[R] (i : ι), Π₀ (j : κ i), M i j) →ₗ[R] Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
                  ((MultilinearMap.fromDFinsuppEquiv κ R (M := M) :
                      (a :
                          (p : (i : ι) → κ i) →
                            MultilinearMap R (fun (i : ι) ↦ M i (p i))
                              (Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))) →
                        MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j)
                          (Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)))
                    fun (p : (i : ι) → κ i) ↦
                    compMultilinearMap (M₁ := fun (i : ι) ↦ M i (p i))
                      (DFinsupp.lsingle (R := R) (M := fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p)
                      (tprod R (s := fun (i : ι) ↦ M i (p i)))))
              (tprod R (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j)))
            fun (i : ι) ↦ DFinsupp.lsingle (M := M i) (x i) :
          (a : (i : ι) → M i (x i)) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
        x_1 :
      ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
    ((MultilinearMap.compLinearMap (M₁ := fun (i : ι) ↦ M i (x i)) (M₁' := fun (i : ι) ↦ Π₀ (j : κ i), M i j)
            (compMultilinearMap (M₁ := fun (i : ι) ↦ Π₀ (j : κ i), M i j) LinearMap.id
              (tprod R (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j)))
            fun (i : ι) ↦ DFinsupp.lsingle (M := M i) (x i) :
          (a : (i : ι) → M i (x i)) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
        x_1 :
      ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
Tactic: ext x