-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
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)
⊢ 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
have 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' := sorry, map_smul' := sorry } ∘ₗ
              (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)
Tactic: ext