∀ {M : Type u_3} [inst : Mul M] (carrier : Set M) (mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier)
  (carrier_1 : Set M) (mul_mem'_1 : ∀ {a b : M}, a ∈ carrier_1 → b ∈ carrier_1 → a * b ∈ carrier_1),
  ({ carrier := carrier, mul_mem' := mul_mem' } = { carrier := carrier_1, mul_mem' := mul_mem'_1 }) =
    (carrier = carrier_1)