-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_5 : (i : ι) → AddCommMonoid (t' i)
inst_6 : (i : ι) → Module.{u_4, u_12} R (t' i)
r : R
φ : ⨂[R] (i : ι), s i →ₗ[R] LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)
x : (i : ι) → s i
x_1 : (i : ι) → t i
⊢ Eq (α := ⨂[R] (i : ι), t' i)
    ((LinearMap.compMultilinearMap (M₁ := t)
            ((LinearMap.compMultilinearMap (M₁ := s)
                  ((lift (s := s) :
                      (a : MultilinearMap R s ((⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)) →
                        (⨂[R] (i : ι), s i) →ₗ[R] (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)
                    (LinearMap.compMultilinearMap (M₁ := s) (piTensorHomMap (s := t) (t := t'))
                      ((((lift (s := fun (i : ι) ↦
                                  s i →ₗ[R] LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) :
                                (a :
                                    MultilinearMap R (fun (i : ι) ↦ s i →ₗ[R] t i →ₗ[R] t' i)
                                      (MultilinearMap R s (⨂[R] (i : ι), t i →ₗ[R] t' i))) →
                                  (⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R]
                                    MultilinearMap R s (⨂[R] (i : ι), t i →ₗ[R] t' i))
                              ((piLinearMap (M₁ := s) (M₁' := fun (i : ι) ↦
                                    LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) :
                                  (a : MultilinearMap R (fun (i : ι) ↦ t i →ₗ[R] t' i) (⨂[R] (i : ι), t i →ₗ[R] t' i)) →
                                    MultilinearMap R (fun (i : ι) ↦ s i →ₗ[R] t i →ₗ[R] t' i)
                                      (MultilinearMap R s (⨂[R] (i : ι), t i →ₗ[R] t' i)))
                                (tprod R (s := fun (i : ι) ↦
                                  LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)))) :
                            (⨂[R] (i : ι), s i →ₗ[R] LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) →ₗ[R]
                              MultilinearMap R s
                                (⨂[R] (i : ι), LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i))) :
                          (a : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i) →
                            MultilinearMap R s (⨂[R] (i : ι), t i →ₗ[R] t' i))
                        (r • φ))))
                  (tprod R (s := s)) :
                (a : (i : ι) → s i) → (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)
              x)
            (tprod R (s := t)) :
          (a : (i : ι) → t i) → ⨂[R] (i : ι), t' i)
        x_1 :
      ⨂[R] (i : ι), t' i)
    ((LinearMap.compMultilinearMap (M₁ := t)
            (((HSMul.hSMul (β := (⨂[R] (i : ι), s i) →ₗ[R] (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i) r
                      ((lift (s := s) :
                            (a : MultilinearMap R s ((⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)) →
                              (⨂[R] (i : ι), s i) →ₗ[R] (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)
                          (LinearMap.compMultilinearMap (M₁ := s) (piTensorHomMap (s := t) (t := t'))
                            ((((lift (s := fun (i : ι) ↦
                                        s i →ₗ[R] LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) :
                                      (a :
                                          MultilinearMap R (fun (i : ι) ↦ s i →ₗ[R] t i →ₗ[R] t' i)
                                            (MultilinearMap R s (⨂[R] (i : ι), t i →ₗ[R] t' i))) →
                                        (⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R]
                                          MultilinearMap R s (⨂[R] (i : ι), t i →ₗ[R] t' i))
                                    ((piLinearMap (M₁ := s) (M₁' := fun (i : ι) ↦
                                          LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) :
                                        (a :
                                            MultilinearMap R (fun (i : ι) ↦ t i →ₗ[R] t' i)
                                              (⨂[R] (i : ι), t i →ₗ[R] t' i)) →
                                          MultilinearMap R (fun (i : ι) ↦ s i →ₗ[R] t i →ₗ[R] t' i)
                                            (MultilinearMap R s (⨂[R] (i : ι), t i →ₗ[R] t' i)))
                                      (tprod R (s := fun (i : ι) ↦
                                        LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)))) :
                                  (⨂[R] (i : ι),
                                      s i →ₗ[R] LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) →ₗ[R]
                                    MultilinearMap R s
                                      (⨂[R] (i : ι), LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i))) :
                                (a : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i) →
                                  MultilinearMap R s (⨂[R] (i : ι), t i →ₗ[R] t' i))
                              φ)) :
                        (⨂[R] (i : ι), s i) →ₗ[R] (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)).compMultilinearMap
                  (M₁ := s) (tprod R (s := s)) :
                (a : (i : ι) → s i) → (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)
              x)
            (tprod R (s := t)) :
          (a : (i : ι) → t i) → ⨂[R] (i : ι), t' i)
        x_1 :
      ⨂[R] (i : ι), t' i)

Tactic:
simp only [map_smul, LinearMap.compMultilinearMap_apply,
    lift.tprod, smul_apply, LinearMap.smul_apply]

Premises used: PiTensorProduct.lift.tprod, MultilinearMap.smul_apply, LinearMap.smul_apply, LinearMap.compMultilinearMap_apply, map_smul