∀ (R : Type u_5) [inst : CommSemiring R] (S : Type u_4) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type u_1}
  [inst_3 : DecidableEq ι₁] (M₁ : ι₁ → Type u_2) (M₂' : Type u_3) [inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)]
  [inst_5 : AddCommMonoid M₂'] [inst_6 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_7 : Module R M₂']
  [inst_8 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_9 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)],
  (DirectSum.toModule S ι₁ (TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) M₂') fun i =>
        TensorProduct.AlgebraTensorModule.map (DirectSum.lof S ι₁ M₁ i) LinearMap.id) ∘ₗ
      TensorProduct.AlgebraTensorModule.lift
        (DirectSum.toModule S ι₁ (M₂' →ₗ[R] DirectSum ι₁ fun i => TensorProduct R (M₁ i) M₂') fun x =>
          (TensorProduct.AlgebraTensorModule.mk R S (M₁ x) M₂').compr₂
            (DirectSum.lof S ι₁ (fun i => TensorProduct R (M₁ i) M₂') x)) =
    LinearMap.id