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