∀ {R : Type u_1} {inst : CommRing R} {toSubsemiring : Subsemiring R}
  {mem_of_isSquare' :
    autoParam (∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) RingPreordering.mem_of_isSquare'._autoParam}
  {neg_one_notMem' : autoParam (-1 ∉ toSubsemiring.carrier) RingPreordering.neg_one_notMem'._autoParam}
  {toSubsemiring_1 : Subsemiring R}
  {mem_of_isSquare'_1 :
    autoParam (∀ {x : R}, IsSquare x → x ∈ toSubsemiring_1.carrier) RingPreordering.mem_of_isSquare'._autoParam}
  {neg_one_notMem'_1 : autoParam (-1 ∉ toSubsemiring_1.carrier) RingPreordering.neg_one_notMem'._autoParam},
  { toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare', neg_one_notMem' := neg_one_notMem' } =
      { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := mem_of_isSquare'_1,
        neg_one_notMem' := neg_one_notMem'_1 } →
    toSubsemiring = toSubsemiring_1