Ae mem version Space of realizable

theorem ae_mem_versionSpace_of_realizable    [MeasurableSpace α] [MeasurableSpace β]    {C : ConceptClass α β} {c : α → β} (hc : c ∈ C) (hcm : Measurable c)    (hG : MeasurableSet {p : α × β | p.2 = c p.1})    (P : Measure α) [IsProbabilityMeasure P] (m : ℕ) :    ∀ᵐ S : LabeledSample α β m      ∂(Measure.pi (fun _ : Fin m => P.map (fun x => (x, c x)))),      c ∈ VersionSpace C S := by  have hφ : Measurable (fun x : α => (x, c x)) := by fun_prop  haveI : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) :=    Measure.isProbabilityMeasure_map hφ.aemeasurable  rw [ae_iff]  have hsub : {S : Fin m → α × β | ¬ c ∈ VersionSpace C S} ⊆      (Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1}))ᶜ := by    intro S hS hcontra    exact hS ⟨hc, by simp_all⟩  have hcompl : (Measure.pi (fun _ : Fin m => P.map (fun x : α => (x, c x))))      ((Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1}))ᶜ) = 0 := by    rw [prob_compl_eq_one_sub (MeasurableSet.univ_pi fun _ => hG),        pi_map_graph_eq_one hcm P hG, tsub_self]  exact measure_mono_null hsub hcompl