∀ {k : Type u_3} {P₁ : Type u_1} {V₁ : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁],
  Function.RightInverse
    (fun u =>
      { toFun := ⇑↑u, invFun := ⇑↑u⁻¹, left_inv := ⋯, right_inv := ⋯,
        linear := (LinearMap.GeneralLinearGroup.generalLinearEquiv k V₁) ((Units.map AffineMap.linearHom) u),
        map_vadd' := ⋯ })
    fun e => { val := ↑e, inv := ↑e.symm, val_inv := ⋯, inv_val := ⋯ }