∀ (𝕜 : Type u_5) {ι : Type u_3} {ι' : Type u_4} (G : Type u_2) (G' : Type u_1) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G']
  [inst_4 : NormedSpace 𝕜 G'] (σ : ι ≃ ι'),
  Function.RightInverse (ContinuousMultilinearMap.domDomCongrEquiv σ).invFun
    (ContinuousMultilinearMap.domDomCongrEquiv σ).toFun