-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
ι₁ : Type v₁
inst_1 : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst_2 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_3 : AddCommMonoid M₁'
inst_4 : AddCommMonoid M₂'
inst_5 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_6 : Module R M₁'
inst_7 : Module R M₂'
f : M₁' →ₗ[R] M₂'
⊢ Eq (α := (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i))
    (((↑(directSumRight R R M₂' M₁) :
            (M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
          (M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) ∘ₗ
        (rTensor (⨁ (i : ι₁), M₁ i) f : (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) :
      (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i))
    ((lmap (M := fun (x : ι₁) ↦ TensorProduct.{u, w₁', w₁} R M₁' (M₁ x)) (N := fun (x : ι₁) ↦
            TensorProduct.{u, w₂', w₁} R M₂' (M₁ x)) fun (x : ι₁) ↦ rTensor (M₁ x) f :
          (⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) →ₗ[R]
            ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) ∘ₗ
        ((↑(directSumRight R R M₁' M₁) :
            (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) :
          (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) :
      (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i))
have a : ∀ (x : M₁') (i : ι₁) (x_1 : M₁ i) (i_1 : ι₁),
  (((((AlgebraTensorModule.curry
                        (((↑(directSumRight R R M₂' M₁) :
                              (M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
                            (M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) ∘ₗ
                          (rTensor (⨁ (i : ι₁), M₁ i) f :
                            (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] M₂' ⊗[R] ⨁ (i : ι₁), M₁ i)) :
                      M₁' →ₗ[R] (⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
                    (a : M₁') → (⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), M₂' ⊗[R] M₁ i)
                  x ∘ₗ
                lof R ι₁ M₁ i :
              (a : M₁ i) → ⨁ (i : ι₁), M₂' ⊗[R] M₁ i)
            x_1 :
          ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
        (a : ι₁) → M₂' ⊗[R] M₁ a)
      i_1 =
    (((((AlgebraTensorModule.curry
                        ((lmap (M := fun (x : ι₁) ↦ TensorProduct.{u, w₁', w₁} R M₁' (M₁ x)) (N := fun (x : ι₁) ↦
                              TensorProduct.{u, w₂', w₁} R M₂' (M₁ x)) fun (x : ι₁) ↦ rTensor (M₁ x) f :
                            (⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) →ₗ[R]
                              ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) ∘ₗ
                          ((↑(directSumRight R R M₁' M₁) :
                              (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) :
                            (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i))) :
                      M₁' →ₗ[R] (⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
                    (a : M₁') → (⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), M₂' ⊗[R] M₁ i)
                  x ∘ₗ
                lof R ι₁ M₁ i :
              (a : M₁ i) → ⨁ (i : ι₁), M₂' ⊗[R] M₁ i)
            x_1 :
          ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
        (a : ι₁) → M₂' ⊗[R] M₁ a)
      i_1
Tactic: ext