-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
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)
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
⊢ 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

Tactic:
ext p x