-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem generateMeasurable_eq_rec (s : Set (Set α)) :
    { t | GenerateMeasurable s t } = generateMeasurableRec s ω₁

Proof state:
case iUnion
α : Type u
s : Set (Set α)
t : Set α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (ω_ 1)
⊢ ⋃ i, f i ∈ generateMeasurableRec s (ω_ 1)

Tactic:
simp_rw [generateMeasurableRec_omega1, mem_iUnion₂, exists_prop] at IH

Result:
case iUnion
α : Type u
s : Set (Set α)
t : Set α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), ∃ i < ω_ 1, f n ∈ generateMeasurableRec s i
⊢ ⋃ i, f i ∈ generateMeasurableRec s (ω_ 1)

Proof state:
case iUnion
α : Type u
s : Set (Set α)
t : Set α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), ∃ i < ω_ 1, f n ∈ generateMeasurableRec s i
⊢ ⋃ i, f i ∈ generateMeasurableRec s (ω_ 1)

Tactic:
exact iUnion_mem_generateMeasurableRec IH

Result:
no goals

Proof state:
case compl
α : Type u
s : Set (Set α)
t u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ generateMeasurableRec s (ω_ 1)
⊢ uᶜ ∈ generateMeasurableRec s (ω_ 1)

Tactic:
rw [generateMeasurableRec_omega1, mem_iUnion₂] at IH

Result:
case compl
α : Type u
s : Set (Set α)
t u : Set α
a✝ : GenerateMeasurable s u
IH : ∃ i, ∃ (_ : i < ω_ 1), u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ generateMeasurableRec s (ω_ 1)

Proof state:
case compl.intro.intro
α : Type u
s : Set (Set α)
t u : Set α
a✝ : GenerateMeasurable s u
i : Ordinal.{u_1}
hi : i < ω_ 1
hi' : u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ generateMeasurableRec s (ω_ 1)

Tactic:
exact generateMeasurableRec_mono _ ((isLimit_omega 1).succ_lt hi).le
  (compl_mem_generateMeasurableRec (Order.lt_succ i) hi')

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
⊢ {t | GenerateMeasurable s t} = generateMeasurableRec s (ω_ 1)

Tactic:
apply (generateMeasurableRec_subset s _).antisymm'

Result:
α : Type u
s : Set (Set α)
⊢ {t | GenerateMeasurable s t} ⊆ generateMeasurableRec s (ω_ 1)

Proof state:
case basic
α : Type u
s : Set (Set α)
t u : Set α
hu : u ∈ s
⊢ u ∈ generateMeasurableRec s (ω_ 1)

Tactic:
exact self_subset_generateMeasurableRec s _ hu

Result:
no goals

Proof state:
case compl
α : Type u
s : Set (Set α)
t u : Set α
a✝ : GenerateMeasurable s u
IH : ∃ i, ∃ (_ : i < ω_ 1), u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ generateMeasurableRec s (ω_ 1)

Tactic:
obtain ⟨i, hi, hi'⟩ := IH

Result:
case compl.intro.intro
α : Type u
s : Set (Set α)
t u : Set α
a✝ : GenerateMeasurable s u
i : Ordinal.{u_1}
hi : i < ω_ 1
hi' : u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ generateMeasurableRec s (ω_ 1)

Proof state:
case empty
α : Type u
s : Set (Set α)
t : Set α
⊢ ∅ ∈ generateMeasurableRec s (ω_ 1)

Tactic:
exact empty_mem_generateMeasurableRec s _

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
⊢ {t | GenerateMeasurable s t} ⊆ generateMeasurableRec s (ω_ 1)

Tactic:
intro t ht

Result:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ {t | GenerateMeasurable s t}
⊢ t ∈ generateMeasurableRec s (ω_ 1)

Proof state:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ {t | GenerateMeasurable s t}
⊢ t ∈ generateMeasurableRec s (ω_ 1)

Tactic:
induction' ht with u hu u _ IH f _ IH

Result:
case basic
α : Type u
s : Set (Set α)
t u : Set α
hu : u ∈ s
⊢ u ∈ generateMeasurableRec s (ω_ 1)

case empty
α : Type u
s : Set (Set α)
t : Set α
⊢ ∅ ∈ generateMeasurableRec s (ω_ 1)

case compl
α : Type u
s : Set (Set α)
t u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ generateMeasurableRec s (ω_ 1)
⊢ uᶜ ∈ generateMeasurableRec s (ω_ 1)

case iUnion
α : Type u
s : Set (Set α)
t : Set α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (ω_ 1)
⊢ ⋃ i, f i ∈ generateMeasurableRec s (ω_ 1)