-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the
spaces of continuous (semi)linear maps. This version is for the type alias
`CompactConvergenceCLM`.  -/
ContinuousLinearEquiv.compactConvergenceCLMCongrSL : {𝕜 : Type u_7} →
  {𝕜₂ : Type u_8} →
    {𝕜₃ : Type u_9} →
      {𝕜₄ : Type u_10} →
        {E : Type u_11} →
          {F : Type u_12} →
            {G : Type u_13} →
              {H : Type u_14} →
                [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 σ₁₂ σ₂₄
                                                                                                σ₁₄] →
                                                                                            (E ≃SL[σ₁₂] F) →
                                                                                              (H ≃SL[σ₄₃] G) →
                                                                                                CompactConvergenceCLM
                                                                                                    σ₁₄ E H ≃SL[σ₄₃]
                                                                                                  CompactConvergenceCLM
                                                                                                    σ₂₃ F G