awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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
⊢ ∃ (S_1 : Finset (Set α)), (↑S_1 : Set (Set α)) ⊆ memPartition t n ∧ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑S_1 : Set (Set α))
have refine_1₁ : (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑((memPartition t n).toFinset \ S) : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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 α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))
have 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 α))
Tactic: choose S hS_subset hS_eq using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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 α))
⊢ Fintype (↑(⋃ (n : ℕ), (↑(S n) : Set (Set α))) : Type u_1)
have refine : ⋃ (n : ℕ), (↑(S n) : Set (Set α)) ⊆ memPartition t n
Tactic: refine (Finite.subset (finite_memPartition t n) ?_).fintype
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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 α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))
have 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 α))
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
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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 α))
have refine_1 : (↑(toFinset (⋃ (n : ℕ), (↑(S n) : Set (Set α)))) : Set (Set α)) ⊆ memPartition t n
Tactic: refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ⋃ (i : ℕ), f i = ⋃₀ (↑S : Set (Set α))
have refine_1₁ : ⋃ (i : ℕ), f i = ⋃₀ (↑(toFinset (⋃ (n : ℕ), (↑(S n) : Set (Set α)))) : Set (Set α))
Tactic: refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : MeasurableSet s
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
have refine_1 : ∀ (u : Set α) (hu : u ∈ memPartition t n),
  MeasurableSet u → ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ u = ⋃₀ (↑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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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 α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
have refine_1₁ : ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ∅ = ⋃₀ (↑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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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 α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
have 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 α))
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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 α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
have 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 α))
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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 s
have refine_2 : MeasurableSet.{u_1} (α := α) (⋃ i ∈ (↑S : Set (Set α)), i)
Tactic: rw [hS_eq, sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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)
have refine_2 : (↑S : Set (Set α)).Countable
Tactic: refine MeasurableSet.biUnion ?_ (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ (↑S : Set (Set α)), i)
have refine_2₁ : ∀ (t_1 : Set α) (ht : t_1 ∈ (↑S : Set (Set α))), MeasurableSet t_1
Tactic: refine MeasurableSet.biUnion ?_ (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ t n = ⋃ u ∈ memPartition t n, u ∩ t n
have simp_rw : t n = (⋃ i ∈ memPartition t n, i) ∩ t n
Tactic: simp_rw [← iUnion_inter, ← sUnion_eq_biUnion, sUnion_memPartition, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
simp_rw : t n = (⋃ i ∈ memPartition t n, i) ∩ t n
⊢ t n = ⋃ u ∈ memPartition t n, u ∩ t n
have simp_rw₁ : t n = ⋃₀ memPartition t n ∩ t n
Tactic: simp_rw [← iUnion_inter, ← sUnion_eq_biUnion, sUnion_memPartition, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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
⊢ t n = ⋃ u ∈ memPartition t n, u ∩ t n
have simp_rw₂ : t n = univ ∩ t n
Tactic: simp_rw [← iUnion_inter, ← sUnion_eq_biUnion, sUnion_memPartition, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ MeasurableSet (t n)
have this : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
⊢ MeasurableSet (t n)
have rw : MeasurableSet.{u_1} (α := α) (⋃ u ∈ memPartition t n, u ∩ t n)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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)
have refine : ∀ (v : Set α) (hv : v ∈ memPartition t n), MeasurableSet (v ∩ t n)
Tactic: refine MeasurableSet.biUnion (finite_memPartition _ _).countable (fun v hv ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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)
have refine : v ∩ t n ∈ memPartition t (n + 1)
Tactic: refine measurableSet_generateFrom ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
⊢ generateFrom (⋃ (n : ℕ), memPartition t n) = generateFrom (range t)
have refine_1 : ∀ (u : Set α) (hu : Membership.mem (γ := Set (Set α)) (⋃ (n : ℕ), memPartition t n) u), MeasurableSet u
Tactic: refine le_antisymm (generateFrom_le fun u hu ↦ ?_) (generateFrom_le fun u hu ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
refine_1 : ∀ (u : Set α) (hu : Membership.mem (γ := Set (Set α)) (⋃ (n : ℕ), memPartition t n) u), MeasurableSet u
⊢ generateFrom (⋃ (n : ℕ), memPartition t n) = generateFrom (range t)
have refine_2 : ∀ (u : Set α) (hu : u ∈ range t), MeasurableSet u
Tactic: refine le_antisymm (generateFrom_le fun u hu ↦ ?_) (generateFrom_le fun u hu ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hu : Membership.mem (γ := Set (Set α)) (⋃ (n : ℕ), memPartition t n) u
⊢ MeasurableSet u
have hu₁ : ∃ (i : ℕ), u ∈ memPartition t i
Tactic: simp only [mem_iUnion] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ (i : ℕ), u ∈ memPartition t i
⊢ MeasurableSet u
have refine_1 : ∀ (n : ℕ) (hun : u ∈ memPartition t n), MeasurableSet u
Tactic: obtain ⟨n, hun⟩ := hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u ∈ memPartition t 0
⊢ MeasurableSet u
have hun₁ : u = univ
Tactic: simp only [memPartition_zero, mem_singleton_iff] at hun
Cleared hypotheses: hun
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet u
have refine_1 : MeasurableSet.{u_1} (α := α) univ
Tactic: rw [hun]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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
⊢ MeasurableSet u
have refine_1 : ∀ (v : Set α) (hv : v ∈ memPartition t n) (huv : u = v ∩ t n ∨ u = v \ t n), MeasurableSet u
Tactic: obtain ⟨v, hv, huv⟩ := hun
Cleared hypotheses: hun
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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
⊢ MeasurableSet u
have refine_1 : MeasurableSet (v ∩ t n)
Tactic: rcases huv with rfl | rfl
Cleared hypotheses: u, huv
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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)
⊢ MeasurableSet u
have refine_1₁ : MeasurableSet (v \ t n)
Tactic: rcases huv with rfl | rfl
Cleared hypotheses: u, huv
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
n : ℕ
hun : u ∈ memPartition t n
⊢ MeasurableSet u
have refine_1 : ∀ (u : Set α) (hun : u ∈ memPartition t 0), 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⟩)
Cleared hypotheses: u, n, hun
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
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
⊢ MeasurableSet u
have refine_1₁ : ∀ (n : ℕ) (ih : ∀ (u : Set α) (hun : u ∈ memPartition t n), MeasurableSet u) (u : Set α)
  (hun : u ∈ memPartition t (n + 1)), 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⟩)
Cleared hypotheses: u, n, hun
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ range t
⊢ MeasurableSet u
have hu₁ : ∃ (y : ℕ), t y = u
Tactic: simp only [mem_range] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ (y : ℕ), t y = u
⊢ MeasurableSet u
have refine_2 : ∀ (n : ℕ), MeasurableSet (t n)
Tactic: obtain ⟨n, rfl⟩ := hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
| generateFrom (range t)
have rw : generateFrom (⋃ (n : ℕ), memPartition t n)
Tactic: rw [← generateFrom_iUnion_memPartition t]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (range t)
have conv_rhs : generateFrom (memPartition t n) ≤ generateFrom (⋃ (n : ℕ), memPartition t n)
Tactic: conv_rhs => rw [← generateFrom_iUnion_memPartition t]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ generateFrom (⋃ (n : ℕ), memPartition t n) ≤ m
have refine : ∀ t_1 ∈ range t, MeasurableSet t_1
Tactic: refine (generateFrom_iUnion_memPartition t).trans_le (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
inst : CountablyGenerated α
⊢ generateFrom (⋃ (n : ℕ), countablePartition α n) = m
have rw : generateFrom (⋃ (n : ℕ), memPartition (enumerateCountable (s := countableGeneratingSet α) sorry ∅) n) = m
Tactic: rw [countablePartition, generateFrom_iUnion_memPartition,
    range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]