-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the
spaces of continuous (semi)linear maps.  -/
ContinuousLinearEquiv.arrowCongrSL : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      {𝕜₄ : Type u_4} →
        {E : Type u_5} →
          {F : Type u_6} →
            {G : Type u_7} →
              {H : Type u_8} →
                [inst : AddCommGroup E] →
                  [inst_1 : AddCommGroup F] →
                    [inst_2 : AddCommGroup G] →
                      [inst_3 : AddCommGroup H] →
                        [inst_4 : NormedField 𝕜] →
                          [inst_5 : NormedField 𝕜₂] →
                            [inst_6 : NormedField 𝕜₃] →
                              [inst_7 : NormedField 𝕜₄] →
                                [inst_8 : Module 𝕜 E] →
                                  [inst_9 : Module 𝕜₂ F] →
                                    [inst_10 : Module 𝕜₃ G] →
                                      [inst_11 : Module 𝕜₄ H] →
                                        [inst_12 : TopologicalSpace E] →
                                          [inst_13 : TopologicalSpace F] →
                                            [inst_14 : TopologicalSpace G] →
                                              [inst_15 : TopologicalSpace H] →
                                                [inst_16 : IsTopologicalAddGroup G] →
                                                  [inst_17 : IsTopologicalAddGroup H] →
                                                    [inst_18 : ContinuousConstSMul 𝕜₃ G] →
                                                      [inst_19 : ContinuousConstSMul 𝕜₄ H] →
                                                        {σ₁₂ : 𝕜 →+* 𝕜₂} →
                                                          {σ₂₁ : 𝕜₂ →+* 𝕜} →
                                                            {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                                                              {σ₁₃ : 𝕜 →+* 𝕜₃} →
                                                                {σ₃₄ : 𝕜₃ →+* 𝕜₄} →
                                                                  {σ₄₃ : 𝕜₄ →+* 𝕜₃} →
                                                                    {σ₂₄ : 𝕜₂ →+* 𝕜₄} →
                                                                      {σ₁₄ : 𝕜 →+* 𝕜₄} →
                                                                        [inst_20 : RingHomInvPair σ₁₂ σ₂₁] →
                                                                          [inst_21 : RingHomInvPair σ₂₁ σ₁₂] →
                                                                            [inst_22 : RingHomInvPair σ₃₄ σ₄₃] →
                                                                              [inst_23 : RingHomInvPair σ₄₃ σ₃₄] →
                                                                                [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] →
                                                                                  [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] →
                                                                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                                                                      [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] →
                                                                                        [RingHomCompTriple σ₂₃ σ₃₄
                                                                                              σ₂₄] →
                                                                                          [RingHomCompTriple σ₁₂ σ₂₄
                                                                                                σ₁₄] →
                                                                                            [RingHomIsometric σ₁₂] →
                                                                                              [RingHomIsometric σ₂₁] →
                                                                                                (E ≃SL[σ₁₂] F) →
                                                                                                  (H ≃SL[σ₄₃] G) →
                                                                                                    ⋯ ≃SL[σ₄₃] ⋯