case inl
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i ≤ i
⊢ x ∈ generateMeasurableRec s i

case inr
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x ∈ generateMeasurableRec s j
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
⊢ x ∈ generateMeasurableRec s j
rcases eq_or_lt_of_le h with (rfl | h)
no goals
case inl
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i ≤ i
⊢ x ∈ generateMeasurableRec s i
exact hx
case h.e'_4
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x = ⋃ (n : ℕ), x
case inr
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x ∈ generateMeasurableRec s j
convert iUnion_mem_generateMeasurableRec fun _ => ⟨i, h, hx⟩
no goals
case h.e'_4
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x = ⋃ (n : ℕ), x
exact (iUnion_const x).symm