-- Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : CommSemiring S
inst_5 : Algebra R S
inst_6 : Decomposition ℳ
i : ι
refine_2 :
  ∀ (x : ↥(ℳ i)),
    Eq (α := ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
      ((((AlgebraTensorModule.curry
                    (((((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                                  ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
                                (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S]
                                  ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
                              (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                                      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S]
                                        ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
                                    (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S]
                                      ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
                                  ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                                      S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                                    S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                                S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
                            coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
                          lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i :
                        ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
                      (Submodule.toBaseChange S (ℳ i) :
                        TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i) →ₗ[S] ↥(Submodule.baseChange S (ℳ i)))) :
                  S →ₗ[S] ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) :
                (a : S) → ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
              1 :
            (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
          x :
        ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
      ((((AlgebraTensorModule.curry
                    ((LinearMap.id ∘ₗ lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i) ∘ₗ
                      Submodule.toBaseChange S (ℳ i)) :
                  S →ₗ[S] ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) :
                (a : S) → ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
              1 :
            (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
          x :
        ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
⊢ Eq (α := TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i)))
    (((((lmap (M := fun (x : ι) ↦ TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ x)) (N := fun (i : ι) ↦
                  ↥(Submodule.baseChange S (ℳ i))) fun (x : ι) ↦ Submodule.toBaseChange S (ℳ x) :
                (⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) →ₗ[S]
                  ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
              (((↑(directSumRight R S S fun (i : ι) ↦ ↥(ℳ i)) :
                      (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) :
                    (S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i)) ∘ₗ
                  ((↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) :
                      S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                    S ⊗[R] M →ₗ[S] S ⊗[R] ⨁ (i : ι), ↥(ℳ i)) :
                S ⊗[R] M →ₗ[S] ⨁ (i : ι), TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i))) ∘ₗ
            coeLinearMap fun (i : ι) ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
          lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i :
        ↥(Submodule.baseChange S (ℳ i)) →ₗ[S] ⨁ (i : ι), ↥(Submodule.baseChange S (ℳ i))) ∘ₗ
      (Submodule.toBaseChange S (ℳ i) : TensorProduct.{u_2, u_4, u_3} R S ↥(ℳ i) →ₗ[S] ↥(Submodule.baseChange S (ℳ i))))
    ((LinearMap.id ∘ₗ lof S ι (fun (i : ι) ↦ ↥(Submodule.baseChange S (ℳ i))) i) ∘ₗ Submodule.toBaseChange S (ℳ i))

Tactic:
ext : 3