∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M],
  TensorProduct.directLimitRight f M =
    ((TensorProduct.comm R M (Module.DirectLimit G f)).trans (TensorProduct.directLimitLeft f M)).trans
      (Module.DirectLimit.congr (fun x => TensorProduct.comm R (G x) M) ⋯)