-- 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₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_6 : AddCommMonoid M₁'
inst_7 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_8 : AddCommMonoid M₂'
inst_9 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_10 : Module R M₁'
inst_11 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_12 : Module R M₂'
inst_13 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_14 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
inst_15 : Module S M₁'
inst_16 : IsScalarTower R S M₁'
toFun :
  ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)
invFun :
  (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂
left :
  Eq (α :=
    (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S]
      ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
    ((AlgebraTensorModule.lift
          (toModule S ι₁ (M := M₁)
            ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) fun (i₁ : ι₁) ↦
            LinearMap.flip
              (toModule R ι₂ (M := M₂) (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
                fun (i₂ : ι₂) ↦
                LinearMap.flip
                  (AlgebraTensorModule.curry
                      (lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) :
                    M₁ i₁ →ₗ[S] M₂ i₂ →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)))) :
        ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S]
          ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) ∘ₗ
      (toModule S (ι₁ × ι₂) (M := fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
          ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun (i : ι₁ × ι₂) ↦
          AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2) :
        (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S]
          (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂))
    LinearMap.id
⊢ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)
have right : Eq (α := ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
  ((toModule S (ι₁ × ι₂) (M := fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
        ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun (i : ι₁ × ι₂) ↦
        AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2)) ∘ₗ
      AlgebraTensorModule.lift
        (toModule S ι₁ (M := M₁)
          ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) fun (i₁ : ι₁) ↦
          LinearMap.flip
            (toModule R ι₂ (M := M₂) (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
              fun (i₂ : ι₂) ↦
              LinearMap.flip
                (AlgebraTensorModule.curry
                    (lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) :
                  M₁ i₁ →ₗ[S] M₂ i₂ →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)))) :
    ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
  (LinearMap.id : ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
Tactic: refine LinearEquiv.ofLinear ?toFun ?invFun ?left ?right