∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (s : S.Splitting) (n : N) (g : G),
  (fun e => ⟨Function.invFun (⇑S.inl) (e * (s (S.rightHom e))⁻¹), S.rightHom e⟩)
      ((fun x =>
          match x with
          | ⟨n, g⟩ => S.inl n * s g)
        ⟨n, g⟩) =
    ⟨n, g⟩