-- 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)
x : (i : ι ⊕ ι₂) → N i
⊢ Eq (α := ⨂[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))
                          (currySum (N := N) (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' := ⋯ } :
          (a : (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂))) → ⨂[R] (i : ι ⊕ ι₂), N i)
        ((((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₂)))) :
              (⨂[R] (i : ι ⊕ ι₂), N i) →ₗ[R] (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂))) :
            (a : ⨂[R] (i : ι ⊕ ι₂), N i) → (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
          ((tprod R (s := N) : (a : (i : ι ⊕ ι₂) → N i) → ⨂[R] (i : ι ⊕ ι₂), N i) x)) :
      ⨂[R] (i : ι ⊕ ι₂), N i)
    ((tprod R (s := N) : (a : (i : ι ⊕ ι₂) → N i) → ⨂[R] (i : ι ⊕ ι₂), N i) x : ⨂[R] (i : ι ⊕ ι₂), N i)
have H : Eq (α := ⨂[R] (i : ι ⊕ ι₂), N i)
  (⨂ₜ[R] (t : ι ⊕ ι₂),
      Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂)) t :
    ⨂[R] (i : ι ⊕ ι₂), N i)
  ((tprod R (s := N) : (a : (i : ι ⊕ ι₂) → N i) → ⨂[R] (i : ι ⊕ ι₂), N i) x : ⨂[R] (i : ι ⊕ ι₂), N i)
Tactic: simp only [lift.tprod, domCoprodDep_apply, lift.tmul, LinearMap.coe_mk, AddHom.coe_mk,
        currySum_apply]