Proving set equality in class

Stream: new members

[Marmare314]

Hello, I am trying to formalize some basic Neyman-Pearson theory in lean. I came up with the following basic
definitions.

class StatisticalSpace (Ω : Type*) extends MeasurableSpace Ω where
  DistributionAssumption' : Set (ProbabilityMeasure Ω)

def DistributionAssumption (Ω : Type*) [hS : StatisticalSpace Ω] :=
  {P : ProbabilityMeasure Ω // P ∈ hS.DistributionAssumption'}

What I got stuck at is defining a specific statistical space with exactly two distributions:

class SimpleStatisticalSpace (Ω : Type*) extends StatisticalSpace Ω where
  P₀ : ProbabilityMeasure Ω
  P₁ : ProbabilityMeasure Ω
  unique : P₀ ≠ P₁
  DistributionAssumption' := {P₀, P₁}
  DistributionAssumption'_def  : DistributionAssumption' = {P₀, P₁} := sorry

I'm not sure if its possible to prove DistributionAssumption'_def . The proof does not have to be a part of
the class of course, but I need some way to access P0 and P1 as DistributionAssumption \Omega.
Maybe a class is not the best choice here?

Something that was adding to my confusion about this is that none of the following report any errors/warnings:

structure MyClass where
  MySet : Set ℕ := {0, 1}
  MySet_def : MySet = {0, 1} := by rfl

structure MyClass' where
  MySet : Set ℕ := {0, 1}
  MySet_def : MySet = {0, 1} := by sorry

structure MyClass'' where
  MySet : Set ℕ := {0, 1}
  MySet_def : MySet = {0, 1} := by rewrite []

I assume that a proof term is expected here, but there should still be an error (maybe my lean version is outdated).