∀ {R₁ : Type u_5} {R₂ : Type u_3} {R₁' : Type u_6} {R₂' : Type u_4} {M₁ : Type u_7} {M₂ : Type u_1} {M₁' : Type u_8}
  {M₂' : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₁'] [inst_3 : Semiring R₂']
  [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁'] [inst_7 : AddCommMonoid M₂']
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁'] [inst_11 : Module R₂' M₂']
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'}
  {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [inst_12 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_13 : RingHomInvPair σ₂₁ σ₁₂] [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂)
  (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₂ →ₛₗ[σ₂₂'] M₂'),
  (fun f => (↑e₂ ∘ₛₗ f) ∘ₛₗ ↑e₁.symm) ((fun f => (↑e₂.symm ∘ₛₗ f) ∘ₛₗ ↑e₁) f) = f