-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma measurableSet_generateFrom_memPartition_iff (t : ℕ → Set α) (n : ℕ) (s : Set α) :
    MeasurableSet[generateFrom (memPartition t n)] s
      ↔ ∃ S : Finset (Set α), ↑S ⊆ memPartition t n ∧ s = ⋃₀ S

Proof state:
case refine_1.iUnion
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S

Tactic:
refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩

Result:
case refine_1.iUnion.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ↑(⋃ n, ↑(S n)).toFinset ⊆ memPartition t n

case refine_1.iUnion.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ⋃ i, f i = ⋃₀ ↑(⋃ n, ↑(S n)).toFinset

Proof state:
case refine_1.iUnion.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ∀ (i : ℕ), ↑(S i) ⊆ memPartition t n

Tactic:
exact hS_subset

Result:
no goals

Proof state:
case refine_1.compl.intro.intro.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ memPartition t n \ ↑S ⊆ memPartition t n

Tactic:
exact diff_subset

Result:
no goals

Proof state:
case refine_2.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ (↑S).Countable

Tactic:
exact S.countable_toSet

Result:
no goals

Proof state:
case refine_1.iUnion.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ↑(⋃ n, ↑(S n)).toFinset ⊆ memPartition t n

Tactic:
simp only [coe_toFinset, iUnion_subset_iff]

Result:
case refine_1.iUnion.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ∀ (i : ℕ), ↑(S i) ⊆ memPartition t n

Proof state:
case refine_1.compl.intro.intro.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ⋃₀ (memPartition t n \ ↑S) ∪ ⋃₀ ↑S = univ

Tactic:
rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_diff_cancel hS_subset]

Result:
no goals

Proof state:
case refine_1.compl.intro.intro
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ∃ S_1, ↑S_1 ⊆ memPartition t n ∧ (⋃₀ ↑S)ᶜ = ⋃₀ ↑S_1

Tactic:
refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩

Result:
case refine_1.compl.intro.intro.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ↑((memPartition t n).toFinset \ S) ⊆ memPartition t n

case refine_1.compl.intro.intro.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ (⋃₀ ↑S)ᶜ = ⋃₀ ↑((memPartition t n).toFinset \ S)

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ ↑∅ ⊆ memPartition t n

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.compl.intro.intro.refine_2.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
u : Set α
huS : u ∈ ↑S
⊢ Disjoint (⋃₀ (memPartition t n \ ↑S)) u

Tactic:
refine Set.disjoint_sUnion_left.mpr fun v huV => ?_

Result:
case refine_1.compl.intro.intro.refine_2.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
u : Set α
huS : u ∈ ↑S
v : Set α
huV : v ∈ memPartition t n \ ↑S
⊢ Disjoint v u

Proof state:
case refine_1.compl.intro.intro.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ⋃₀ (memPartition t n \ ↑S) ⊔ ⋃₀ ↑S = ⊤

Tactic:
simp only [sup_eq_union, top_eq_univ]

Result:
case refine_1.compl.intro.intro.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ⋃₀ (memPartition t n \ ↑S) ∪ ⋃₀ ↑S = univ

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ ∅ = ⋃₀ ↑∅

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.compl.intro.intro.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ Codisjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)

Tactic:
rw [codisjoint_iff]

Result:
case refine_1.compl.intro.intro.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ⋃₀ (memPartition t n \ ↑S) ⊔ ⋃₀ ↑S = ⊤

Proof state:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet (⋃ i ∈ ↑S, i)

Tactic:
refine MeasurableSet.biUnion ?_ (fun t ht ↦ ?_)

Result:
case refine_2.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ (↑S).Countable

case refine_2.refine_2
α : Type u_1
t✝ : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t✝ n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t✝ n
hS_eq : s = ⋃₀ ↑S
t : Set α
ht : t ∈ ↑S
⊢ MeasurableSet t

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
⊢ ∀ (i : ℕ), ↑(S i) ⊆ memPartition t n

Tactic:
exact hS_subset

Result:
no goals

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
⊢ Fintype ↑(⋃ n, ↑(S n))

Tactic:
refine (Finite.subset (finite_memPartition t n) ?_).fintype

Result:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
⊢ ⋃ n, ↑(S n) ⊆ memPartition t n

Proof state:
case refine_1.compl.intro.intro.refine_2.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ Disjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)

Tactic:
refine Set.disjoint_sUnion_right.mpr fun u huS => ?_

Result:
case refine_1.compl.intro.intro.refine_2.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
u : Set α
huS : u ∈ ↑S
⊢ Disjoint (⋃₀ (memPartition t n \ ↑S)) u