∀ (G : Type u_1) (H : Type u_2),
  Function.RightInverse
    (fun x =>
      match x with
      | (x, y) => Multiplicative.ofAdd (Multiplicative.toAdd x, Multiplicative.toAdd y))
    fun x => (Multiplicative.ofAdd (Multiplicative.toAdd x).1, Multiplicative.ofAdd (Multiplicative.toAdd x).2)