∀ {K : Type u} [inst : Field K] [inst_1 : SizeOf K] (toSubring : Subring K)
  (mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier),
  sizeOf { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' } = 1 + sizeOf toSubring