-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
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)
⊢ (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)
have 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)
Tactic: ext