α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ s ⊆
    let i := i;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ s ⊆ generateMeasurableRec s i
unfold generateMeasurableRec
case h.h.h
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ s ⊆ s
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ s ⊆
    let i := i;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
apply_rules [subset_union_of_subset_left]
no goals
case h.h.h
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ s ⊆ s
exact subset_rfl