-- 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_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 s

Tactic:
rw [hS_eq, sUnion_eq_biUnion]

Result:
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)

Proof state:
case refine_1.hC
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
hu : u ∈ memPartition t n
ht✝ : MeasurableSet u
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ u = ⋃₀ ↑S

Tactic:
exact ⟨{u}, by simp [hu], by simp⟩

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)
⊢ ⋃ n, ↑(S n) ⊆ memPartition t n

Tactic:
simp only [iUnion_subset_iff]

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)
⊢ ∀ (i : ℕ), ↑(S i) ⊆ memPartition t n

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
hu : u ∈ memPartition t n
ht✝ : MeasurableSet u
⊢ u = ⋃₀ ↑{u}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ MeasurableSet s ↔ ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨S, hS_subset, hS_eq⟩ ↦ ?_⟩

Result:
case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : MeasurableSet s
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S

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 s

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
hu : u ∈ memPartition t n
ht✝ : MeasurableSet u
⊢ ↑{u} ⊆ memPartition t n

Tactic:
simp [hu]

Result:
no goals

Proof state:
case refine_1.compl
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
ht✝ : MeasurableSet u
hu : ∃ S, ↑S ⊆ memPartition t n ∧ u = ⋃₀ ↑S
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ uᶜ = ⋃₀ ↑S

Tactic:
obtain ⟨S, hS_subset, rfl⟩ := hu

Result:
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

Proof state:
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)

Tactic:
simp only [Finset.coe_sdiff, coe_toFinset]

Result:
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 \ ↑S)

Proof state:
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 \ ↑S)

Tactic:
refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm

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)
⊢ Disjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)

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)

Proof state:
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

Tactic:
exact measurableSet_generateFrom (hS_subset ht)

Result:
no goals

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)
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S

Tactic:
have : Fintype (⋃ n, (S n : Set (Set α))) := by
  refine (Finite.subset (finite_memPartition t n) ?_).fintype
  simp only [iUnion_subset_iff]
  exact hS_subset

Result:
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

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

Tactic:
choose S hS_subset hS_eq using h

Result:
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)
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S

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).toFinset \ S) ⊆ memPartition t n

Tactic:
simp only [Finset.coe_sdiff, coe_toFinset]

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 \ ↑S ⊆ memPartition t n

Proof state:
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

Tactic:
simp only [coe_toFinset, sUnion_iUnion, hS_eq]

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
v : Set α
huV : v ∈ memPartition t n \ ↑S
⊢ Disjoint v u

Tactic:
refine disjoint_memPartition t n (mem_of_mem_diff huV) (hS_subset 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
v : Set α
huV : v ∈ memPartition t n \ ↑S
⊢ v ≠ u

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
v : Set α
huV : v ∈ memPartition t n \ ↑S
⊢ v ≠ u

Tactic:
exact ne_of_mem_of_not_mem huS (not_mem_of_mem_diff huV) |>.symm

Result:
no goals

Proof state:
case refine_1.empty
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ∅ = ⋃₀ ↑S

Tactic:
exact ⟨∅, by simp, by simp⟩

Result:
no goals