-- 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)
H :
  ∀ (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)
⊢ (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 • φ))) =
    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)

Tactic:
ext