-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma generateFrom_iUnion_memPartition (t : ℕ → Set α) :
    generateFrom (⋃ n, memPartition t n) = generateFrom (range t)

Proof state:
α : Type u_1
t : ℕ → Set α
⊢ generateFrom (⋃ n, memPartition t n) = generateFrom (range t)

Tactic:
refine le_antisymm (generateFrom_le fun u hu ↦ ?_) (generateFrom_le fun u hu ↦ ?_)

Result:
case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ ⋃ n, memPartition t n
⊢ MeasurableSet u

case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ range t
⊢ MeasurableSet u

Proof state:
case refine_1.intro.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u ∈ memPartition t 0
⊢ MeasurableSet u

Tactic:
simp only [memPartition_zero, mem_insert_iff, mem_singleton_iff] at hun

Result:
case refine_1.intro.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet u

Proof state:
case refine_1.intro.succ
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
u : Set α
hun : ∃ u_1 ∈ memPartition t n, u = u_1 ∩ t n ∨ u = u_1 \ t n
⊢ MeasurableSet u

Tactic:
obtain ⟨v, hv, huv⟩ := hun

Result:
case refine_1.intro.succ.intro.intro
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
u v : Set α
hv : v ∈ memPartition t n
huv : u = v ∩ t n ∨ u = v \ t n
⊢ MeasurableSet u

Proof state:
case refine_1.intro.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet u

Tactic:
rw [hun]

Result:
case refine_1.intro.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet univ

Proof state:
case refine_1.intro.succ
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
u : Set α
hun : u ∈ memPartition t (n + 1)
⊢ MeasurableSet u

Tactic:
simp only [memPartition_succ, mem_setOf_eq] at hun

Result:
case refine_1.intro.succ
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
u : Set α
hun : ∃ u_1 ∈ memPartition t n, u = u_1 ∩ t n ∨ u = u_1 \ t n
⊢ MeasurableSet u

Proof state:
case refine_2.intro
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ MeasurableSet (t n)

Tactic:
exact generateFrom_mono (subset_iUnion _ _) _ (measurableSet_generateFrom_memPartition t n)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ range t
⊢ MeasurableSet u

Tactic:
simp only [iUnion_singleton_eq_range, mem_range] at hu

Result:
case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ y, t y = u
⊢ MeasurableSet u

Proof state:
case refine_1.intro.succ.intro.intro.inl
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v ∩ t n)

Tactic:
exact (ih v hv).inter (measurableSet_generateFrom ⟨n, rfl⟩)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ y, t y = u
⊢ MeasurableSet u

Tactic:
obtain ⟨n, rfl⟩ := hu

Result:
case refine_2.intro
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ MeasurableSet (t n)

Proof state:
case refine_1.intro.succ.intro.intro
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
u v : Set α
hv : v ∈ memPartition t n
huv : u = v ∩ t n ∨ u = v \ t n
⊢ MeasurableSet u

Tactic:
rcases huv with rfl | rfl

Result:
case refine_1.intro.succ.intro.intro.inl
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v ∩ t n)

case refine_1.intro.succ.intro.intro.inr
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v \ t n)

Proof state:
case refine_1.intro.succ.intro.intro.inr
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v \ t n)

Tactic:
exact (ih v hv).diff (measurableSet_generateFrom ⟨n, rfl⟩)

Result:
no goals

Proof state:
case refine_1.intro.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet univ

Tactic:
exact MeasurableSet.univ

Result:
no goals

Proof state:
case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ i, u ∈ memPartition t i
⊢ MeasurableSet u

Tactic:
obtain ⟨n, hun⟩ := hu

Result:
case refine_1.intro
α : Type u_1
t : ℕ → Set α
u : Set α
n : ℕ
hun : u ∈ memPartition t n
⊢ MeasurableSet u

Proof state:
case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ ⋃ n, memPartition t n
⊢ MeasurableSet u

Tactic:
simp only [mem_iUnion] at hu

Result:
case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ i, u ∈ memPartition t i
⊢ MeasurableSet u