∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : NonUnitalNonAssocSemiring A} {inst_2 : Module R A}
  {toNonUnitalSubsemiring : NonUnitalSubsemiring A}
  {smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier}
  {toNonUnitalSubsemiring_1 : NonUnitalSubsemiring A}
  {smul_mem'_1 : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring_1.carrier → c • x ∈ toNonUnitalSubsemiring_1.carrier},
  { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, smul_mem' := smul_mem'_1 } →
    toNonUnitalSubsemiring = toNonUnitalSubsemiring_1