∀ (R : Type u_4) {ι : Type u_3} (M₂ : Type u_2) (M₃ : Type u_1) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₃] [inst_5 : Subsingleton ι] (i : ι),
  Function.RightInverse (MultilinearMap.ofSubsingleton R M₂ M₃ i).invFun (MultilinearMap.ofSubsingleton R M₂ M₃ i).toFun