-- 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)
⊢ ∀ (m : R) (x : ⨂[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))
          (m • x)) =
      HSMul.hSMul (α := R) (β := (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)) →ₗ[R] ⨂[R] (i : ι ⊕ ι₂), N i)
        ((RingHom.id R : (a : R) → R) m : R)
        ((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))
              x) :
          (⨂[R] (i : ι₂), N (Sum.inr i)) →ₗ[R] ⨂[R] (i : ι ⊕ ι₂), N i)

Tactic:
simp