-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
H :
  ∀ (x : (i : ι ⊕ ι₂) → N i),
    Eq (α := ⨂[R] (i : ι ⊕ ι₂), N i)
      ((LinearMap.compMultilinearMap (M₁ := N)
              (TensorProduct.lift
                  {
                    toFun := fun (a : ⨂[R] (i₁ : ι), N (Sum.inl i₁)) ↦
                      (lift (s := fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) :
                          (a : MultilinearMap R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) (⨂[R] (i : ι ⊕ ι₂), N i)) →
                            (⨂[R] (i : ι₂), N (Sum.inr i)) →ₗ[R] ⨂[R] (i : ι ⊕ ι₂), N i)
                        ((((lift (s := fun (i : ι) ↦ N (Sum.inl i)) :
                                  (a :
                                      MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i))
                                        (MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))) →
                                    (⨂[R] (i : ι), N (Sum.inl i)) →ₗ[R]
                                      MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))
                                ((currySumEquiv (N := N) :
                                    (a : MultilinearMap R N (⨂[R] (i : ι ⊕ ι₂), N i)) →
                                      MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i))
                                        (MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i)))
                                  (tprod R (s := N))) :
                              (⨂[R] (i : ι), N (Sum.inl i)) →ₗ[R]
                                MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i)) :
                            (a : ⨂[R] (i : ι), N (Sum.inl i)) →
                              MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))
                          a),
                    map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
                (lift (s := N) :
                    (a : MultilinearMap R N ((⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))) →
                      (⨂[R] (i : ι ⊕ ι₂), N i) →ₗ[R]
                        (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
                  (domCoprodDep (N := N) (tprod R (s := fun (i₁ : ι) ↦ N (Sum.inl i₁)))
                    (tprod R (s := fun (i₂ : ι₂) ↦ N (Sum.inr i₂)))))
              (tprod R (s := N)) :
            (a : (i : ι ⊕ ι₂) → N i) → ⨂[R] (i : ι ⊕ ι₂), N i)
          x :
        ⨂[R] (i : ι ⊕ ι₂), N i)
      ((LinearMap.compMultilinearMap (M₁ := N) LinearMap.id (tprod R (s := N)) :
            (a : (i : ι ⊕ ι₂) → N i) → ⨂[R] (i : ι ⊕ ι₂), N i)
          x :
        ⨂[R] (i : ι ⊕ ι₂), N i)
⊢ Eq (α := (⨂[R] (i : ι ⊕ ι₂), N i) →ₗ[R] ⨂[R] (i : ι ⊕ ι₂), N i)
    (TensorProduct.lift
        {
          toFun := fun (a : ⨂[R] (i₁ : ι), N (Sum.inl i₁)) ↦
            (lift (s := fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) :
                (a : MultilinearMap R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) (⨂[R] (i : ι ⊕ ι₂), N i)) →
                  (⨂[R] (i : ι₂), N (Sum.inr i)) →ₗ[R] ⨂[R] (i : ι ⊕ ι₂), N i)
              ((((lift (s := fun (i : ι) ↦ N (Sum.inl i)) :
                        (a :
                            MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i))
                              (MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))) →
                          (⨂[R] (i : ι), N (Sum.inl i)) →ₗ[R]
                            MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))
                      ((currySumEquiv (N := N) :
                          (a : MultilinearMap R N (⨂[R] (i : ι ⊕ ι₂), N i)) →
                            MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i))
                              (MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i)))
                        (tprod R (s := N))) :
                    (⨂[R] (i : ι), N (Sum.inl i)) →ₗ[R]
                      MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i)) :
                  (a : ⨂[R] (i : ι), N (Sum.inl i)) →
                    MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))
                a),
          map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (lift (s := N) :
          (a : MultilinearMap R N ((⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))) →
            (⨂[R] (i : ι ⊕ ι₂), N i) →ₗ[R] (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
        (domCoprodDep (N := N) (tprod R (s := fun (i₁ : ι) ↦ N (Sum.inl i₁)))
          (tprod R (s := fun (i₂ : ι₂) ↦ N (Sum.inr i₂)))))
    LinearMap.id

Tactic:
ext