-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst_3 : DecidableEq ι₁
inst_4 : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₂ : ι₂ → Type w₂
inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_6 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_7 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_8 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_9 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_10 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
i₁ : ι₁
m₁ : M₁ i₁
i₂ : ι₂
m₂ : M₂ i₂
rw :
  Eq (α := ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
    (((lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂) :
            TensorProduct.{u, w₁, w₂} R (M₁ (i₁, i₂).1) (M₂ (i₁, i₂).2) →ₗ[S]
              ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
          (a : M₁ (i₁, i₂).1 ⊗[R] M₂ (i₁, i₂).2) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
        (m₁ ⊗ₜ[R] m₂) :
      ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
    (((TensorProduct.directSum R S M₁ M₂ :
            ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[S]
              ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
          (a : (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
        ((lof S ι₁ M₁ i₁ : (a : M₁ i₁) → ⨁ (i : ι₁), M₁ i) m₁ ⊗ₜ[R]
          (lof R ι₂ M₂ i₂ : (a : M₂ i₂) → ⨁ (i : ι₂), M₂ i) m₂) :
      ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
⊢ Eq (α := (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
    (((LinearEquiv.symm (TensorProduct.directSum R S M₁ M₂) :
            (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) ≃ₗ[S]
              (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) :
          (a : ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) → (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
        (((lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂) :
              TensorProduct.{u, w₁, w₂} R (M₁ (i₁, i₂).1) (M₂ (i₁, i₂).2) →ₗ[S]
                ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
            (a : M₁ (i₁, i₂).1 ⊗[R] M₂ (i₁, i₂).2) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
          (m₁ ⊗ₜ[R] m₂)) :
      (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
    ((lof S ι₁ M₁ i₁ : (a : M₁ i₁) → ⨁ (i : ι₁), M₁ i) m₁ ⊗ₜ[R] (lof R ι₂ M₂ i₂ : (a : M₂ i₂) → ⨁ (i : ι₂), M₂ i) m₂ :
      (⨁ (i : ι₁), M₁ i) ⊗[R] ⨁ (i : ι₂), M₂ i)
have rw₁ : Eq (α := ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
  (((lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂) :
          TensorProduct.{u, w₁, w₂} R (M₁ (i₁, i₂).1) (M₂ (i₁, i₂).2) →ₗ[S]
            ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
        (a : M₁ (i₁, i₂).1 ⊗[R] M₂ (i₁, i₂).2) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
      (m₁ ⊗ₜ[R] m₂) :
    ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
  (((lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂) :
          TensorProduct.{u, w₁, w₂} R (M₁ (i₁, i₂).1) (M₂ (i₁, i₂).2) →ₗ[S]
            ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
        (a : M₁ (i₁, i₂).1 ⊗[R] M₂ (i₁, i₂).2) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
      (m₁ ⊗ₜ[R] m₂) :
    ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
Tactic: rw [LinearEquiv.symm_apply_eq, directSum_lof_tmul_lof]