∀ {G : Type u_1} [inst : Add G] {a : G},
  Function.RightInverse
    (fun u =>
      let __Equiv := Equiv.Perm.equivUnitsEnd.symm ((Units.map AddConstMap.toEnd) u);
      { toEquiv := __Equiv, map_add_const' := ⋯ })
    ⇑AddConstEquiv.toAddConstMapHom.toHomUnits