∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} {R₂ : Type u_6} {R₃ : Type u_7}
  [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R₂ N] [inst_7 : AddCommMonoid P] [inst_8 : Module R₃ P] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [inst_11 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_12 : RingHomInvPair σ₂₁ σ₁₂] [inst_13 : RingHomInvPair σ₂₃ σ₃₂] [inst_14 : RingHomInvPair σ₃₂ σ₂₃]
  [inst_15 : RingHomInvPair σ₁₃ σ₃₁] [inst_16 : RingHomInvPair σ₃₁ σ₁₃] (f : M ≃ₛₗ[σ₁₂] N) (f₂ : N ≃ₛₗ[σ₂₃] P),
  Finsupp.mapRange.linearEquiv (f.trans f₂) = (Finsupp.mapRange.linearEquiv f).trans (Finsupp.mapRange.linearEquiv f₂)