-- 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 :
  ∀ (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)
⊢ 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

Tactic:
ext x