∀ (M : Type u_1) [inst : Monoid M] {R' : Type u_2} [inst_1 : Ring R'] [inst_2 : MulSemiringAction M R'] (U : Subring R')
  [inst_3 : IsInvariantSubring M U], ↑(IsInvariantSubring.subtypeHom M U) = U.subtype