-- 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 (α := (Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) →ₗ[R] Π₀ (p : (i : ι) → κ i), ⨂[R] (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)))) ∘ₗ
      (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)))))
    LinearMap.id
have h : ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)) (i : (i : ι) → κ i),
  (((compMultilinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₂ := ⨂[R] (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)))) ∘ₗ
                      (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))))) ∘ₗ
                    DFinsupp.lsingle (R := R) (M := fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p :
                  (⨂[R] (i : ι), M i (p i)) →ₗ[R] Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
                (tprod R (s := fun (i : ι) ↦ M i (p i)) :
                  MultilinearMap R (fun (i : ι) ↦ M i (p i)) (⨂[R] (i : ι), M i (p i))) :
              (a : (i : ι) → M i (p i)) → Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            x :
          Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      i =
    (((compMultilinearMap (M₁ := fun (i : ι) ↦ M i (p i))
                (LinearMap.id ∘ₗ
                  DFinsupp.lsingle (R := R) (M := fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p)
                (tprod R (s := fun (i : ι) ↦ M i (p i))) :
              (a : (i : ι) → M i (p i)) → Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            x :
          Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      i
Tactic: ext p x