-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem generateMeasurableRec_omega1 (s : Set (Set α)) :
    generateMeasurableRec s (ω₁ : Ordinal.{v}) =
      ⋃ i < (ω₁ : Ordinal.{v}), generateMeasurableRec s i

Proof state:
α : Type u
s : Set (Set α)
⊢ generateMeasurableRec s (ω_ 1) = ⋃ i, ⋃ (_ : i < ω_ 1), generateMeasurableRec s i

Tactic:
apply (iUnion₂_subset fun i h => generateMeasurableRec_mono s h.le).antisymm'

Result:
α : Type u
s : Set (Set α)
⊢ generateMeasurableRec s (ω_ 1) ⊆ ⋃ i, ⋃ (_ : i < ω_ 1), generateMeasurableRec s i

Proof state:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i

Tactic:
refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht

Result:
case refine_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ t ∈ s, ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i

case refine_2
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∃ i, ∃ (_ : i < ω_ 1), ∅ ∈ generateMeasurableRec s i

case refine_3
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (u : Set α),
    (∃ i, ∃ (_ : i < ω_ 1), u ∈ generateMeasurableRec s i) →
      (∃ j < ω_ 1, u ∈ generateMeasurableRec s j) → ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (f : ℕ → Set α),
    (∀ (n : ℕ),
        (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j) →
      ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Proof state:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
I : ℕ → Ordinal.{v}
hI : ∀ (n : ℕ), I n < ω_ 1 ∧ f n ∈ generateMeasurableRec s (I n)
⊢ ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
refine ⟨_, Ordinal.lsub_lt_ord_lift ?_ fun n => (hI n).1,
  iUnion_mem_generateMeasurableRec fun n => ⟨_, Ordinal.lt_lsub I n, (hI n).2⟩⟩

Result:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
I : ℕ → Ordinal.{v}
hI : ∀ (n : ℕ), I n < ω_ 1 ∧ f n ∈ generateMeasurableRec s (I n)
⊢ Cardinal.lift.{v, 0} #ℕ < (ω_ 1).cof

Proof state:
case refine_1
α : Type u
s : Set (Set α)
t✝ : Set α
ht✝ : t✝ ∈ generateMeasurableRec s (ω_ 1)
t : Set α
ht : t ∈ s
⊢ ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i

Tactic:
exact ⟨0, omega_pos 1, self_subset_generateMeasurableRec s 0 ht⟩

Result:
no goals

Proof state:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (f : ℕ → Set α),
    (∀ (n : ℕ),
        (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j) →
      ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
intro f H

Result:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
⊢ ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Proof state:
case refine_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ t ∈ s, ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i

Tactic:
intro t ht

Result:
case refine_1
α : Type u
s : Set (Set α)
t✝ : Set α
ht✝ : t✝ ∈ generateMeasurableRec s (ω_ 1)
t : Set α
ht : t ∈ s
⊢ ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i

Proof state:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
I : ℕ → Ordinal.{v}
hI : ∀ (n : ℕ), I n < ω_ 1 ∧ f n ∈ generateMeasurableRec s (I n)
⊢ Cardinal.lift.{v, 0} #ℕ < (ω_ 1).cof

Tactic:
rw [mk_nat, lift_aleph0, isRegular_aleph_one.cof_omega_eq]

Result:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
I : ℕ → Ordinal.{v}
hI : ∀ (n : ℕ), I n < ω_ 1 ∧ f n ∈ generateMeasurableRec s (I n)
⊢ ℵ₀ < ℵ_ 1

Proof state:
α : Type u
s : Set (Set α)
⊢ generateMeasurableRec s (ω_ 1) ⊆ ⋃ i, ⋃ (_ : i < ω_ 1), generateMeasurableRec s i

Tactic:
intro t ht

Result:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ t ∈ ⋃ i, ⋃ (_ : i < ω_ 1), generateMeasurableRec s i

Proof state:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
I : ℕ → Ordinal.{v}
hI : ∀ (n : ℕ), ∃ (_ : I n < ω_ 1), f n ∈ generateMeasurableRec s (I n)
⊢ ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
simp_rw [exists_prop] at hI

Result:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
I : ℕ → Ordinal.{v}
hI : ∀ (n : ℕ), I n < ω_ 1 ∧ f n ∈ generateMeasurableRec s (I n)
⊢ ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Proof state:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
⊢ ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
choose I hI using fun n => (H n).1

Result:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
I : ℕ → Ordinal.{v}
hI : ∀ (n : ℕ), ∃ (_ : I n < ω_ 1), f n ∈ generateMeasurableRec s (I n)
⊢ ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Proof state:
case refine_3
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (u : Set α),
    (∃ i, ∃ (_ : i < ω_ 1), u ∈ generateMeasurableRec s i) →
      (∃ j < ω_ 1, u ∈ generateMeasurableRec s j) → ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

Tactic:
rintro u - ⟨j, hj, hj'⟩

Result:
case refine_3.intro.intro
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
u : Set α
j : Ordinal.{v}
hj : j < ω_ 1
hj' : u ∈ generateMeasurableRec s j
⊢ ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

Proof state:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
I : ℕ → Ordinal.{v}
hI : ∀ (n : ℕ), I n < ω_ 1 ∧ f n ∈ generateMeasurableRec s (I n)
⊢ ℵ₀ < ℵ_ 1

Tactic:
exact aleph0_lt_aleph_one

Result:
no goals

Proof state:
case refine_3.intro.intro
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
u : Set α
j : Ordinal.{v}
hj : j < ω_ 1
hj' : u ∈ generateMeasurableRec s j
⊢ ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

Tactic:
exact ⟨_, (isLimit_omega 1).succ_lt hj,
  compl_mem_generateMeasurableRec (Order.lt_succ j) hj'⟩

Result:
no goals

Proof state:
case refine_2
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∃ i, ∃ (_ : i < ω_ 1), ∅ ∈ generateMeasurableRec s i

Tactic:
exact ⟨0, omega_pos 1, empty_mem_generateMeasurableRec s 0⟩

Result:
no goals