awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n
ht : MeasurableSet (⋃₀ (↑S : Set (Set α)))
refine_1 : ⋃₀ (memPartition t n \ (↑S : Set (Set α))) ∪ ⋃₀ (↑S : Set (Set α)) = ⋃₀ memPartition t n
refine_1₁ : ⋃₀ (↑S : Set (Set α)) ∪ ⋃₀ (memPartition t n \ (↑S : Set (Set α))) = ⋃₀ memPartition t n
refine_1₂ : ⋃₀ ((↑S : Set (Set α)) ∪ memPartition t n \ (↑S : Set (Set α))) = ⋃₀ memPartition t n
refine_1₃ refine_1₄ : ⋃₀ memPartition t n = ⋃₀ memPartition t n
⊢ ⋃₀ (memPartition t n \ (↑S : Set (Set α))) ∪ ⋃₀ (↑S : Set (Set α)) = univ

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

Premises used: sUnion_memPartition, Set.union_comm, Set.union_diff_cancel, Set.sUnion_union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n
ht : MeasurableSet (⋃₀ (↑S : Set (Set α)))
refine_1 : (↑((memPartition t n).toFinset \ S) : Set (Set α)) ⊆ memPartition t n
refine_1₁ refine_1₂ : (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑((memPartition t n).toFinset \ S) : Set (Set α))
⊢ ∃ (S_1 : Finset (Set α)), (↑S_1 : Set (Set α)) ⊆ memPartition t n ∧ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑S_1 : Set (Set α))

Tactic:
classical
      refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩
      · simp only [Finset.coe_sdiff, coe_toFinset]
        exact diff_subset
      · simp only [Finset.coe_sdiff, coe_toFinset]
        refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm
        · refine Set.disjoint_sUnion_right.mpr fun u huS => ?_
          refine Set.disjoint_sUnion_left.mpr fun v huV => ?_
          refine disjoint_memPartition t n (mem_of_mem_diff huV) (hS_subset huS) ?_
          exact ne_of_mem_of_not_mem huS (notMem_of_mem_diff huV) |>.symm
        · rw [codisjoint_iff]
          simp only [sup_eq_union, top_eq_univ]
          rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_diff_cancel hS_subset]

Premises used: Iff.mpr, Set.diff_subset, sUnion_memPartition, Finset.coe_sdiff, codisjoint_iff, Set.disjoint_sUnion_left, Set.sup_eq_union, Set.union_comm, Set.top_eq_univ, Set.union_diff_cancel, Set.disjoint_sUnion_right, Set.sUnion_union, IsCompl.mk, Eq.symm, IsCompl.eq_compl, Set.coe_toFinset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
h : ∀ (n_1 : ℕ), ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ f n_1 = ⋃₀ (↑S : Set (Set α))
refine_1 :
  ∀ (S : (n : ℕ) → Finset (Set α)) (hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n)
    (hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))),
    ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))

Tactic:
choose S hS_subset hS_eq using h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
refine : ⋃ (n : ℕ), (↑(S n) : Set (Set α)) ⊆ memPartition t n
⊢ Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)

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

Premises used: finite_memPartition, Set.Finite.fintype, Set.Finite.subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
simp : ∀ (i : ℕ), (↑(S i) : Set (Set α)) ⊆ memPartition t n
⊢ ⋃ (n : ℕ), (↑(S n) : Set (Set α)) ⊆ memPartition t n

Tactic:
simp only [iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
⊢ ∀ (i : ℕ), (↑(S i) : Set (Set α)) ⊆ memPartition t n

Tactic:
hS_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
⊢ ∀ (i : ℕ), (↑(S i) : Set (Set α)) ⊆ memPartition t n

Tactic:
exact hS_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
refine_1 :
  ∀ (this : Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)),
    ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))

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
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
this : Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))

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

Premises used: Set.toFinset, SetLike.coe, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
this : Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)
refine_1 : (↑(toFinset (⋃ (n : ℕ), (↑(S n) : Set (Set α)))) : Set (Set α)) ⊆ memPartition t n
refine_1₁ : ⋃ (i : ℕ), f i = ⋃₀ (↑(toFinset (⋃ (n : ℕ), (↑(S n) : Set (Set α)))) : Set (Set α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))

Tactic:
refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
this : Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)
refine_1 : ∀ (i : ℕ), (↑(S i) : Set (Set α)) ⊆ memPartition t n
⊢ (↑(toFinset (⋃ (n : ℕ), (↑(S n) : Set (Set α)))) : Set (Set α)) ⊆ memPartition t n

Tactic:
simp only [coe_toFinset, iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff, Set.coe_toFinset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
this : Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)
⊢ ∀ (i : ℕ), (↑(S i) : Set (Set α)) ⊆ memPartition t n

Tactic:
hS_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
this : Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)
⊢ ∀ (i : ℕ), (↑(S i) : Set (Set α)) ⊆ memPartition t n

Tactic:
exact hS_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : (n : ℕ) → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), (↑(S n_1) : Set (Set α)) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ (↑(S n) : Set (Set α))
this : Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)
⊢ ⋃ (i : ℕ), f i = ⋃₀ (↑(toFinset (⋃ (n : ℕ), (↑(S n) : Set (Set α)))) : Set (Set α))

Tactic:
simp only [coe_toFinset, sUnion_iUnion, hS_eq]

Premises used: Set.sUnion_iUnion, Set.coe_toFinset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : MeasurableSet s
refine_1 :
  ∀ (u : Set α) (hu : u ∈ memPartition t n),
    MeasurableSet u → ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ u = ⋃₀ (↑S : Set (Set α))
refine_1₁ : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ∅ = ⋃₀ (↑S : Set (Set α))
refine_1₂ :
  ∀ (u : Set α),
    MeasurableSet u →
      ∀ (hu : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ u = ⋃₀ (↑S : Set (Set α))),
        ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ uᶜ = ⋃₀ (↑S : Set (Set α))
refine_1₃ :
  ∀ (f : ℕ → Set α),
    (∀ (n_1 : ℕ), MeasurableSet (f n_1)) →
      ∀
        (h :
          ∀ (n_1 : ℕ), ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ f n_1 = ⋃₀ (↑S : Set (Set α))),
        ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))

Tactic:
induction s, h using generateFrom_induction with
    | hC u hu _ => exact ⟨{u}, by simp [hu], by simp⟩
    | empty => exact ⟨∅, by simp, by simp⟩
    | compl u _ hu =>
      obtain ⟨S, hS_subset, rfl⟩ := hu
      classical
      refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩
      · simp only [Finset.coe_sdiff, coe_toFinset]
        exact diff_subset
      · simp only [Finset.coe_sdiff, coe_toFinset]
        refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm
        · refine Set.disjoint_sUnion_right.mpr fun u huS => ?_
          refine Set.disjoint_sUnion_left.mpr fun v huV => ?_
          refine disjoint_memPartition t n (mem_of_mem_diff huV) (hS_subset huS) ?_
          exact ne_of_mem_of_not_mem huS (notMem_of_mem_diff huV) |>.symm
        · rw [codisjoint_iff]
          simp only [sup_eq_union, top_eq_univ]
          rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_diff_cancel hS_subset]
    | iUnion f _ h =>
      choose S hS_subset hS_eq using h
      have : Fintype (⋃ n, (S n : Set (Set α))) := by
        refine (Finite.subset (finite_memPartition t n) ?_).fintype
        simp only [iUnion_subset_iff]
        exact hS_subset
      refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩
      · simp only [coe_toFinset, iUnion_subset_iff]
        exact hS_subset
      · simp only [coe_toFinset, sUnion_iUnion, hS_eq]

Premises used: Iff.mpr, Set.diff_subset, Set.iUnion_subset_iff, Compl.compl, sUnion_memPartition, Finset.coe_sdiff, codisjoint_iff, Set.disjoint_sUnion_left, Set.sup_eq_union, Set.union_comm, Set.top_eq_univ, Set.disjoint_sUnion_right, Set.sUnion_union, IsCompl.mk, Set.sUnion_iUnion, Eq.symm, Set.iUnion, IsCompl.eq_compl, rfl, Set.coe_toFinset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n
hS_eq : s = ⋃₀ (↑S : Set (Set α))
refine_2 : MeasurableSet.{u_1} (α := α) (⋃ i ∈ (↑S : Set (Set α)), i)
⊢ MeasurableSet s

Tactic:
rw [hS_eq, sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n
hS_eq : s = ⋃₀ (↑S : Set (Set α))
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ (↑S : Set (Set α)), i)

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

Premises used: MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n
hS_eq : s = ⋃₀ (↑S : Set (Set α))
refine_2 : (↑S : Set (Set α)).Countable
refine_2₁ : ∀ (t_1 : Set α) (ht : t_1 ∈ (↑S : Set (Set α))), MeasurableSet t_1
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ (↑S : Set (Set α)), i)

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

Premises used: MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n
hS_eq : s = ⋃₀ (↑S : Set (Set α))
⊢ (↑S : Set (Set α)).Countable

Tactic:
S.countable_toSet

Premises used: Finset.countable_toSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n
hS_eq : s = ⋃₀ (↑S : Set (Set α))
⊢ (↑S : Set (Set α)).Countable

Tactic:
exact S.countable_toSet

Premises used: Finset.countable_toSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t_1 : ℕ → Set α
n : ℕ
s : Set α
h : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t_1 n ∧ s = ⋃₀ (↑S : Set (Set α))
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t_1 n
hS_eq : s = ⋃₀ (↑S : Set (Set α))
t : Set α
ht : t ∈ (↑S : Set (Set α))
⊢ MeasurableSet t

Tactic:
measurableSet_generateFrom (hS_subset ht)

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t_1 : ℕ → Set α
n : ℕ
s : Set α
h : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t_1 n ∧ s = ⋃₀ (↑S : Set (Set α))
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t_1 n
hS_eq : s = ⋃₀ (↑S : Set (Set α))
t : Set α
ht : t ∈ (↑S : Set (Set α))
⊢ MeasurableSet t

Tactic:
exact measurableSet_generateFrom (hS_subset ht)

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
simp_rw : t n = (⋃ i ∈ memPartition t n, i) ∩ t n
simp_rw₁ : t n = ⋃₀ memPartition t n ∩ t n
simp_rw₂ : t n = univ ∩ t n
⊢ t n = ⋃ u ∈ memPartition t n, u ∩ t n

Tactic:
simp_rw [← iUnion_inter, ← sUnion_eq_biUnion, sUnion_memPartition, univ_inter]

Premises used: sUnion_memPartition, Set.univ_inter, Set.sUnion_eq_biUnion, Set.iUnion_inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ t n = ⋃ u ∈ memPartition t n, u ∩ t n

Tactic:
have : t n = ⋃ u ∈ memPartition t n, u ∩ t n := by
    simp_rw [← iUnion_inter, ← sUnion_eq_biUnion, sUnion_memPartition, univ_inter]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
rw : MeasurableSet.{u_1} (α := α) (⋃ u ∈ memPartition t n, u ∩ t n)
⊢ MeasurableSet (t n)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
⊢ MeasurableSet.{u_1} (α := α) (⋃ u ∈ memPartition t n, u ∩ t n)

Tactic:
MeasurableSet.biUnion (finite_memPartition _ _).countable (fun v hv ↦ ?_)

Premises used: finite_memPartition, MeasurableSet.biUnion, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
refine : ∀ (v : Set α) (hv : v ∈ memPartition t n), MeasurableSet (v ∩ t n)
⊢ MeasurableSet.{u_1} (α := α) (⋃ u ∈ memPartition t n, u ∩ t n)

Tactic:
refine MeasurableSet.biUnion (finite_memPartition _ _).countable (fun v hv ↦ ?_)

Premises used: finite_memPartition, MeasurableSet.biUnion, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v ∩ t n)

Tactic:
measurableSet_generateFrom ?_

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
refine : v ∩ t n ∈ memPartition t (n + 1)
⊢ MeasurableSet (v ∩ t n)

Tactic:
refine measurableSet_generateFrom ?_

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n} (v ∩ t n)

Tactic:
⟨v, hv, Or.inl rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n} (v ∩ t n)

Tactic:
exact ⟨v, hv, Or.inl rfl⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
⊢ generateFrom (⋃ (n : ℕ), memPartition t n) = generateFrom (range t)

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

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
refine_1 : ∀ (u : Set α) (hu : Membership.mem (γ := Set (Set α)) (⋃ (n : ℕ), memPartition t n) u), MeasurableSet u
refine_2 : ∀ (u : Set α) (hu : u ∈ range t), MeasurableSet u
⊢ generateFrom (⋃ (n : ℕ), memPartition t n) = generateFrom (range t)

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

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hu : Membership.mem (γ := Set (Set α)) (⋃ (n : ℕ), memPartition t n) u
⊢ ∃ (i : ℕ), u ∈ memPartition t i

Tactic:
simp only [mem_iUnion] at hu

Premises used: Set.mem_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ (i : ℕ), u ∈ memPartition t i
refine_1 : ∀ (n : ℕ) (hun : u ∈ memPartition t n), MeasurableSet u
⊢ MeasurableSet u

Tactic:
obtain ⟨n, hun⟩ := hu
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u ∈ memPartition t 0
⊢ u = univ

Tactic:
simp only [memPartition_zero, mem_singleton_iff] at hun

Premises used: memPartition_zero, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
refine_1 : MeasurableSet.{u_1} (α := α) univ
⊢ MeasurableSet u

Tactic:
rw [hun]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet.{u_1} (α := α) univ

Tactic:
MeasurableSet.univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet.{u_1} (α := α) univ

Tactic:
exact MeasurableSet.univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ (u : Set α) (hun : u ∈ memPartition t n), MeasurableSet u
u : Set α
hun : ∃ u_1 ∈ memPartition t n, u = u_1 ∩ t n ∨ u = u_1 \ t n
refine_1 : ∀ (v : Set α) (hv : v ∈ memPartition t n) (huv : u = v ∩ t n ∨ u = v \ t n), MeasurableSet u
⊢ MeasurableSet u

Tactic:
obtain ⟨v, hv, huv⟩ := hun
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ (u : Set α) (hun : u ∈ memPartition t n), MeasurableSet u
u v : Set α
hv : v ∈ memPartition t n
huv : u = v ∩ t n ∨ u = v \ t n
refine_1 : MeasurableSet (v ∩ t n)
refine_1₁ : MeasurableSet (v \ t n)
⊢ MeasurableSet u

Tactic:
rcases huv with rfl | rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ (u : Set α) (hun : u ∈ memPartition t n), MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v ∩ t n)

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

Premises used: MeasurableSpace.measurableSet_generateFrom, Exists.intro, rfl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ (u : Set α) (hun : 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⟩)

Premises used: MeasurableSpace.measurableSet_generateFrom, Exists.intro, rfl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ (u : Set α) (hun : u ∈ memPartition t n), MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v \ t n)

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

Premises used: MeasurableSet.diff, MeasurableSpace.measurableSet_generateFrom, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ (u : Set α) (hun : 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⟩)

Premises used: MeasurableSet.diff, MeasurableSpace.measurableSet_generateFrom, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
n : ℕ
hun : u ∈ memPartition t n
refine_1 : ∀ (u : Set α) (hun : u ∈ memPartition t 0), MeasurableSet u
refine_1₁ :
  ∀ (n : ℕ) (ih : ∀ (u : Set α) (hun : u ∈ memPartition t n), MeasurableSet u) (u : Set α)
    (hun : u ∈ memPartition t (n + 1)), MeasurableSet u
⊢ MeasurableSet u

Tactic:
induction n generalizing u with
    | zero =>
      simp only [memPartition_zero, mem_singleton_iff] at hun
      rw [hun]
      exact MeasurableSet.univ
    | succ n ih =>
      simp only [memPartition_succ, mem_setOf_eq] at hun
      obtain ⟨v, hv, huv⟩ := hun
      rcases huv with rfl | rfl
      · exact (ih v hv).inter (measurableSet_generateFrom ⟨n, rfl⟩)
      · exact (ih v hv).diff (measurableSet_generateFrom ⟨n, rfl⟩)

Premises used: memPartition_zero, Set.mem_setOf_eq, Set.mem_singleton_iff, memPartition_succ, rfl, MeasurableSet.univ