case h
α : Type u
s : Set (Set α)
t : Set α
⊢ t ∈ {t | GenerateMeasurable s t} ↔ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
α : Type u
s : Set (Set α)
⊢ {t | GenerateMeasurable s t} = ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
ext t
case h.refine'_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ {t | GenerateMeasurable s t}
⊢ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i

case h.refine'_2
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ t ∈ {t | GenerateMeasurable s t}
case h
α : Type u
s : Set (Set α)
t : Set α
⊢ t ∈ {t | GenerateMeasurable s t} ↔ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
refine' ⟨fun ht => _, fun ht => _⟩
case h.refine'_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ {t | GenerateMeasurable s t}
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
⊢ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
case h.refine'_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ {t | GenerateMeasurable s t}
⊢ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
inhabit ω₁
case h.refine'_1.basic
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
hu : u ∈ s
⊢ u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i

case h.refine'_1.empty
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
⊢ ∅ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i

case h.refine'_1.compl
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i

case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ (⋃ (i : ℕ), f i) ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
case h.refine'_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ {t | GenerateMeasurable s t}
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
⊢ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
induction' ht with u hu u _ IH f _ IH
no goals
case h.refine'_1.basic
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
hu : u ∈ s
⊢ u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
exact mem_iUnion.2 ⟨default, self_subset_generateMeasurableRec s _ hu⟩
no goals
case h.refine'_1.empty
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
⊢ ∅ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
exact mem_iUnion.2 ⟨default, empty_mem_generateMeasurableRec s _⟩
case h.refine'_1.compl.intro
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
i : (Quotient.out (ord (aleph 1))).α
hi : u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
case h.refine'_1.compl
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
rcases mem_iUnion.1 IH with ⟨i, hi⟩
case h.refine'_1.compl.intro.intro
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
i : (Quotient.out (ord (aleph 1))).α
hi : u ∈ generateMeasurableRec s i
j : (Quotient.out (ord (aleph 1))).α
hj : i < j
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
case h.refine'_1.compl.intro
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
i : (Quotient.out (ord (aleph 1))).α
hi : u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
obtain ⟨j, hj⟩ := exists_gt i
no goals
case h.refine'_1.compl.intro.intro
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
i : (Quotient.out (ord (aleph 1))).α
hi : u ∈ generateMeasurableRec s i
j : (Quotient.out (ord (aleph 1))).α
hj : i < j
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
exact mem_iUnion.2 ⟨j, compl_mem_generateMeasurableRec hj hi⟩
case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
this : ∀ (n : ℕ), ∃ i, f n ∈ generateMeasurableRec s i
⊢ (⋃ (i : ℕ), f i) ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ (⋃ (i : ℕ), f i) ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
have : ∀ n, ∃ i, f n ∈ generateMeasurableRec s i := fun n => by simpa using IH n
case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
⊢ (⋃ (i : ℕ), f i) ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
this : ∀ (n : ℕ), ∃ i, f n ∈ generateMeasurableRec s i
⊢ (⋃ (i : ℕ), f i) ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
choose I hI using this
no goals
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
n : ℕ
⊢ ∃ i, f n ∈ generateMeasurableRec s i
simpa using IH n
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ (Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n)) < ord (aleph 1)
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ (Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n)) < Ordinal.type fun x x_1 => x < x_1
rw [Ordinal.type_lt]
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ lift (#ℕ) < Ordinal.cof (ord (aleph 1))
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ (Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n)) < ord (aleph 1)
refine' Ordinal.lsub_lt_ord_lift _ fun i => Ordinal.typein_lt_self _
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ ℵ₀ < aleph 1
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ lift (#ℕ) < Ordinal.cof (ord (aleph 1))
rw [mk_denumerable, lift_aleph0, isRegular_aleph_one.cof_eq]
no goals
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ ℵ₀ < aleph 1
exact aleph0_lt_aleph_one
no goals
case h.refine'_1.iUnion.refine'_2
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
n : ℕ
⊢ Ordinal.typein (fun x x_1 => x < x_1) (I n) < Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n)
apply Ordinal.lt_lsub fun n : ℕ => _
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
t : Set α
i : (Quotient.out (ord (aleph 1))).α
hx : t ∈ (fun i => generateMeasurableRec s i) i
⊢ t ∈ {t | GenerateMeasurable s t}
case h.refine'_2
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ t ∈ {t | GenerateMeasurable s t}
rcases ht with ⟨t, ⟨i, rfl⟩, hx⟩
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) i → t ∈ {t | GenerateMeasurable s t}
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
t : Set α
i : (Quotient.out (ord (aleph 1))).α
hx : t ∈ (fun i => generateMeasurableRec s i) i
⊢ t ∈ {t | GenerateMeasurable s t}
revert t
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (x : (Quotient.out (ord (aleph 1))).α),
    (∀ (y : (Quotient.out (ord (aleph 1))).α),
        WellOrder.r (Quotient.out (ord (aleph 1))) y x →
          ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}) →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) x → t ∈ {t | GenerateMeasurable s t}
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) i → t ∈ {t | GenerateMeasurable s t}
apply (aleph 1).ord.out.wo.wf.induction i
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
ht : t ∈ (fun i => generateMeasurableRec s i) j
⊢ t ∈ {t | GenerateMeasurable s t}
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (x : (Quotient.out (ord (aleph 1))).α),
    (∀ (y : (Quotient.out (ord (aleph 1))).α),
        WellOrder.r (Quotient.out (ord (aleph 1))) y x →
          ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}) →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) x → t ∈ {t | GenerateMeasurable s t}
intro j H t ht
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
ht :
  t ∈
    let i := j;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
⊢ t ∈ {t | GenerateMeasurable s t}
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
ht : t ∈ (fun i => generateMeasurableRec s i) j
⊢ t ∈ {t | GenerateMeasurable s t}
unfold generateMeasurableRec at ht
case h.refine'_2.intro.intro.intro.inl.inl.inl
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
h : t ∈ s
⊢ t ∈ {t | GenerateMeasurable s t}

case h.refine'_2.intro.intro.intro.inl.inl.inr
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
⊢ ∅ ∈ {t | GenerateMeasurable s t}

case h.refine'_2.intro.intro.intro.inl.inr.intro.intro.intro.intro.intro.mk
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
u : Set α
k : (Quotient.out (ord (aleph 1))).α
hk : k ∈ Iio j
hu : u ∈ (fun j_1 => generateMeasurableRec s ↑j_1) { val := k, property := hk }
⊢ uᶜ ∈ {t | GenerateMeasurable s t}

case h.refine'_2.intro.intro.intro.inr.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
⊢ (fun f => ⋃ (n : ℕ), ↑(f n)) f ∈ {t | GenerateMeasurable s t}
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
ht :
  t ∈
    let i := j;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
⊢ t ∈ {t | GenerateMeasurable s t}
rcases ht with (((h | (rfl : t = ∅)) | ⟨u, ⟨-, ⟨⟨k, hk⟩, rfl⟩, hu⟩, rfl⟩) | ⟨f, rfl⟩)
no goals
case h.refine'_2.intro.intro.intro.inl.inl.inl
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
h : t ∈ s
⊢ t ∈ {t | GenerateMeasurable s t}
exact .basic t h
no goals
case h.refine'_2.intro.intro.intro.inl.inl.inr
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
⊢ ∅ ∈ {t | GenerateMeasurable s t}
exact .empty
no goals
case h.refine'_2.intro.intro.intro.inl.inr.intro.intro.intro.intro.intro.mk
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
u : Set α
k : (Quotient.out (ord (aleph 1))).α
hk : k ∈ Iio j
hu : u ∈ (fun j_1 => generateMeasurableRec s ↑j_1) { val := k, property := hk }
⊢ uᶜ ∈ {t | GenerateMeasurable s t}
exact .compl u (H k hk u hu)
case h.refine'_2.intro.intro.intro.inr.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
n : ℕ
⊢ GenerateMeasurable s ↑(f n)
case h.refine'_2.intro.intro.intro.inr.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
⊢ (fun f => ⋃ (n : ℕ), ↑(f n)) f ∈ {t | GenerateMeasurable s t}
refine .iUnion _ @fun n => ?_
case h.refine'_2.intro.intro.intro.inr.intro.intro.intro.intro.mk
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
n : ℕ
k : (Quotient.out (ord (aleph 1))).α
hk : k ∈ Iio j
hf : ↑(f n) ∈ (fun j_1 => generateMeasurableRec s ↑j_1) { val := k, property := hk }
⊢ GenerateMeasurable s ↑(f n)
case h.refine'_2.intro.intro.intro.inr.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
n : ℕ
⊢ GenerateMeasurable s ↑(f n)
obtain ⟨-, ⟨⟨k, hk⟩, rfl⟩, hf⟩ := (f n).prop
no goals
case h.refine'_2.intro.intro.intro.inr.intro.intro.intro.intro.mk
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
n : ℕ
k : (Quotient.out (ord (aleph 1))).α
hk : k ∈ Iio j
hf : ↑(f n) ∈ (fun j_1 => generateMeasurableRec s ↑j_1) { val := k, property := hk }
⊢ GenerateMeasurable s ↑(f n)
exact H k hk _ hf