-- Mathlib.Topology.Algebra.Module.Equiv
/-- A pair of continuous (semi)linear equivalences generates a linear equivalence between the spaces
of continuous linear maps. See also `ContinuousLinearEquiv.arrowCongr`.  -/
ContinuousLinearEquiv.arrowCongrEquivₛₗ : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    {R₃ : Type u_3} →
      [inst : Semiring R₁] →
        [inst_1 : Semiring R₂] →
          [inst_2 : Semiring R₃] →
            {σ₁₂ : R₁ →+* R₂} →
              {σ₂₁ : R₂ →+* R₁} →
                [inst_3 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_4 : RingHomInvPair σ₂₁ σ₁₂] →
                    {σ₂₃ : R₂ →+* R₃} →
                      {σ₁₃ : R₁ →+* R₃} →
                        [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                          {M₁ : Type u_4} →
                            [inst_6 : TopologicalSpace M₁] →
                              [inst_7 : AddCommMonoid M₁] →
                                {M₂ : Type u_5} →
                                  [inst_8 : TopologicalSpace M₂] →
                                    [inst_9 : AddCommMonoid M₂] →
                                      {M₃ : Type u_6} →
                                        [inst_10 : TopologicalSpace M₃] →
                                          [inst_11 : AddCommMonoid M₃] →
                                            {M₄ : Type u_7} →
                                              [inst_12 : TopologicalSpace M₄] →
                                                [inst_13 : AddCommMonoid M₄] →
                                                  [inst_14 : Module R₁ M₁] →
                                                    [inst_15 : Module R₂ M₂] →
                                                      [inst_16 : Module R₃ M₃] →
                                                        {R₄ : Type u_8} →
                                                          [inst_17 : Semiring R₄] →
                                                            [inst_18 : Module R₄ M₄] →
                                                              {σ₃₄ : R₃ →+* R₄} →
                                                                {σ₄₃ : R₄ →+* R₃} →
                                                                  [inst_19 : RingHomInvPair σ₃₄ σ₄₃] →
                                                                    [inst_20 : RingHomInvPair σ₄₃ σ₃₄] →
                                                                      {σ₂₄ : R₂ →+* R₄} →
                                                                        {σ₁₄ : R₁ →+* R₄} →
                                                                          [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] →
                                                                            [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] →
                                                                              [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] →
                                                                                [inst_24 : SMulCommClass R₃ R₃ M₃] →
                                                                                  [inst_25 : SMulCommClass R₄ R₄ M₄] →
                                                                                    [inst_26 : ContinuousAdd M₃] →
                                                                                      [inst_27 :
                                                                                          ContinuousConstSMul R₃ M₃] →
                                                                                        [inst_28 : ContinuousAdd M₄] →
                                                                                          [inst_29 :
                                                                                              ContinuousConstSMul R₄
                                                                                                M₄] →
                                                                                            (M₁ ≃SL[σ₁₂] M₂) →
                                                                                              (M₄ ≃SL[σ₄₃] M₃) →
                                                                                                (M₁ →SL[σ₁₄]
                                                                                                    M₄) ≃ₛₗ[σ₄₃]
                                                                                                  M₂ →SL[σ₂₃] M₃