∀ {S : Type u_1} {R₁ : Type u_2} {R₁' : Type u_3} {R₂' : Type u_7} {M₁ : Type u_4} {M₁' : Type u_5} {M₂' : Type u_6}
  [inst : Semiring R₁] [inst_1 : Semiring R₁'] [inst_2 : Semiring R₂'] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₁'] [inst_5 : AddCommMonoid M₂'] [inst_6 : Module R₁ M₁] [inst_7 : Module R₁' M₁']
  [inst_8 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₁₂' : R₁ →+* R₂'}
  [inst_9 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_10 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_11 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_12 : Semiring S] [inst_13 : Module S M₁]
  [inst_14 : SMulCommClass R₁ S M₁] [inst_15 : RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'] (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (b : Sᵈᵐᵃ)
  (x : M₁ →ₛₗ[σ₁₁'] M₁'),
  ((LinearEquiv.refl R₁ M₁).arrowCongrAddEquiv e₂).toFun (b • x) =
    (RingHom.id Sᵈᵐᵃ) b • ((LinearEquiv.refl R₁ M₁).arrowCongrAddEquiv e₂).toFun x