{R : Type u_1} →
  {S : Type u_2} →
    {G : Type u_3} →
      [inst : MulOneClass R] →
        [inst_1 : MulOneClass S] →
          [inst_2 : FunLike G S R] →
            [MonoidHomClass G S R] →
              (f : R → S) → (g : G) → (r : R) → Function.LeftInverse (⇑g) f → [Invertible (f r)] → Invertible r