awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ (m' : MeasurableSpace α), CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m
have refine_1 : CountablyGenerated α
Tactic: refine ⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
refine_1 : CountablyGenerated α
⊢ ∃ (m' : MeasurableSpace α), CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m
have refine_2 : SeparatesPoints α
Tactic: refine ⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
w : Set (Set α)
⊢ CountablyGenerated α
have h : b.Countable ∧ generateFrom b = generateFrom b
Tactic: use b
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ SeparatesPoints α
have refine_2 : ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
Tactic: rw [@separatesPoints_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
⊢ Measurable (mapNatBool α)
have rw : ∀ (a : ℕ), Measurable (β := Bool) fun (x : α) ↦ mapNatBool α x a
Tactic: rw [measurable_pi_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
⊢ ∀ (a : ℕ), Measurable (β := Bool) fun (x : α) ↦ mapNatBool α x a
have refine : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (preimage (β := Bool) (fun (x : α) ↦ mapNatBool α x n) {true})
Tactic: refine fun n ↦ measurable_to_bool ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ MeasurableSet.{u_1} (α := α) (preimage (β := Bool) (fun (x : α) ↦ mapNatBool α x n) {true})
have simp : MeasurableSet (natGeneratingSequence α n)
Tactic: simp only [preimage, mem_singleton_iff, mapNatBool,
    Bool.decide_iff, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y
have rw : CountablyGenerated α → SeparatesPoints α → ∀ ⦃x y : α⦄ (hxy : mapNatBool α x = mapNatBool α y), x = y
Tactic: rw [← generateFrom_natGeneratingSequence α] at *
Cleared hypotheses: inst_2, x, y, hxy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : CountablyGenerated α
inst_3 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
⊢ x = y
have a : ∀ s ∈ range (natGeneratingSequence α), x ∈ s ↔ y ∈ s
Tactic: apply separating_of_generateFrom (range (natGeneratingSequence _))
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : CountablyGenerated α
inst_3 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ x ∈ natGeneratingSequence α n ↔ y ∈ natGeneratingSequence α n
have a : decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)
Tactic: rw [← decide_eq_decide]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : CountablyGenerated α
inst_3 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
a : decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)
⊢ x ∈ natGeneratingSequence α n ↔ y ∈ natGeneratingSequence α n
have rw : Decidable (x ∈ natGeneratingSequence α n)
Tactic: rw [← decide_eq_decide]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : CountablyGenerated α
inst_3 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
a : decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)
rw : Decidable (x ∈ natGeneratingSequence α n)
⊢ x ∈ natGeneratingSequence α n ↔ y ∈ natGeneratingSequence α n
have rw₁ : Decidable (y ∈ natGeneratingSequence α n)
Tactic: rw [← decide_eq_decide]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
⊢ ∃ (s : Set (ℕ → Bool)), Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))
have measurable_invFun : autoParam
  (Measurable (α := (↑(range (mapNatBool α)) : Type)) (β := α)
    (⇑(Equiv.ofInjective (mapNatBool α) sorry).symm : (a : (↑(range (mapNatBool α)) : Type)) → α))
  MeasurableEquiv.measurable_invFun._autoParam
Tactic: use range (mapNatBool α), Equiv.ofInjective _ <|
    injective_mapNatBool _,
    Measurable.subtype_mk <| measurable_mapNatBool _
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
⊢ autoParam
    (Measurable (α := (↑(range (mapNatBool α)) : Type)) (β := α)
      (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α))
    MeasurableEquiv.measurable_invFun._autoParam
have measurable_invFun : autoParam
  (Measurable (α := (↑(range (mapNatBool α)) : Type)) (β := α)
    (⇑(Equiv.ofInjective (mapNatBool α) sorry).symm : (a : (↑(range (mapNatBool α)) : Type)) → α))
  MeasurableEquiv.measurable_invFun._autoParam
Tactic: simp_rw +instances [← generateFrom_natGeneratingSequence α]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
⊢ autoParam
    (Measurable (α := (↑(range (mapNatBool α)) : Type)) (β := α)
      (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α))
    MeasurableEquiv.measurable_invFun._autoParam
have measurable_invFun : ∀ t ∈ range (natGeneratingSequence α),
  MeasurableSet (α := (↑(range (mapNatBool α)) : Type))
    ((⇑(Equiv.ofInjective (mapNatBool α) sorry).symm : (a : (↑(range (mapNatBool α)) : Type)) → α) ⁻¹' t)
Tactic: apply measurable_generateFrom
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (α := (↑(range (mapNatBool α)) : Type))
    ((⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α) ⁻¹'
      natGeneratingSequence α n)
have measurable_invFun : MeasurableSet (α := (↑(range (mapNatBool α)) : Type))
  ((⇑(Equiv.ofInjective (mapNatBool α) sorry) : (a : α) → (↑(range (mapNatBool α)) : Type)) '' natGeneratingSequence α n)
Tactic: rw [← Equiv.image_eq_preimage_symm _ _]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (α := (↑(range (mapNatBool α)) : Type))
    ((⇑(Equiv.ofInjective (mapNatBool α) ⋯) : (a : α) → (↑(range (mapNatBool α)) : Type)) '' natGeneratingSequence α n)
have measurable_invFun : Eq (α := Set { x : ℕ → Bool // x ∈ range (mapNatBool α) })
  (Subtype.val (p := fun (x : ℕ → Bool) ↦ x ∈ range (mapNatBool α)) ⁻¹' {y : ℕ → Bool | y n = true})
  ((⇑(Equiv.ofInjective (mapNatBool α) sorry) : (a : α) → (↑(range (mapNatBool α)) : Type)) '' natGeneratingSequence α n)
Tactic: refine ⟨{y | y n}, by measurability, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
n : ℕ
⊢ Eq (α := Set { x : ℕ → Bool // x ∈ range (mapNatBool α) })
    (Subtype.val (p := fun (x : ℕ → Bool) ↦ x ∈ range (mapNatBool α)) ⁻¹' {y : ℕ → Bool | y n = true})
    ((⇑(Equiv.ofInjective (mapNatBool α) ⋯) : (a : α) → (↑(range (mapNatBool α)) : Type)) '' natGeneratingSequence α n)
have measurable_invFun : preimage (β := { x : ℕ → Bool // x ∈ range (mapNatBool α) })
    (⇑(Equiv.ofInjective (mapNatBool α) sorry) : (a : α) → { x : ℕ → Bool // x ∈ range (mapNatBool α) })
    (Subtype.val (p := fun (x : ℕ → Bool) ↦ x ∈ range (mapNatBool α)) ⁻¹' {y : ℕ → Bool | y n = true}) =
  natGeneratingSequence α n
Tactic: rw [← Equiv.preimage_eq_iff_eq_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
⊢ ∃ (f : α → ℕ → Bool), Measurable f ∧ Injective f
have rcases : ∀ (m' : MeasurableSpace α),
  CountablyGenerated α → SeparatesPoints α → ∀ (m'le : m' ≤ inst), ∃ (f : α → ℕ → Bool), Measurable f ∧ Injective f
Tactic: rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
m' : MeasurableSpace α
left : CountablyGenerated α
left_1 : SeparatesPoints α
m'le : m' ≤ inst
⊢ ∃ (f : α → ℕ → Bool), Measurable f ∧ Injective f
have refine : Measurable (mapNatBool α)
Tactic: refine ⟨mapNatBool α, ?_, injective_mapNatBool _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
⊢ MeasurableSingletonClass α
have rcases : ∀ (f : α → ℕ → Bool) (fmeas : Measurable f) (finj : Injective f), MeasurableSingletonClass α
Tactic: rcases measurable_injection_nat_bool_of_countablySeparated α with ⟨f, fmeas, finj⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
⊢ MeasurableSingletonClass α
have refine : ∀ (x : α), MeasurableSet (α := α) {x}
Tactic: refine ⟨fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (α := α) {x}
have rw : MeasurableSet (f ⁻¹' {f x})
Tactic: rw [← finj.preimage_image {x}, image_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet s
have rw : MeasurableSet (s \ t n ∪ s ∩ t n)
Tactic: rw [← diff_union_inter s (t n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n ∪ s ∩ t n)
have refine_1 : MeasurableSet (s \ t n)
Tactic: refine MeasurableSet.union ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
refine_1 : MeasurableSet (s \ t n)
⊢ MeasurableSet (s \ t n ∪ s ∩ t n)
have refine_2 : MeasurableSet (s ∩ t n)
Tactic: refine MeasurableSet.union ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n)
have refine_1 : s \ 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 α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s ∩ t n)
have refine_2 : s ∩ 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 α
n : ℕ
s : Set α
⊢ MeasurableSet s ↔ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
have refine_1 : ∀ (h : MeasurableSet s), ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
Tactic: refine ⟨fun h ↦ ?_, fun ⟨S, hS_subset, hS_eq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
refine_1 :
  ∀ (h : MeasurableSet s), ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
⊢ MeasurableSet s ↔ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ s = ⋃₀ (↑S : Set (Set α))
have refine_2 : (∃ (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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨S, hS_subset, hS_eq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
ht : 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 α))
have refine_1 : ∀ (S : Finset (Set α)) (hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n),
  MeasurableSet (⋃₀ (↑S : Set (Set α))) →
    ∃ (S_1 : Finset (Set α)),
      (↑S_1 : Set (Set α)) ⊆ memPartition t n ∧ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑S_1 : Set (Set α))
Tactic: obtain ⟨S, hS_subset, rfl⟩ := hu
Cleared hypotheses: u, ht, hu
-- 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 α)))
⊢ ∃ (S_1 : Finset (Set α)), (↑S_1 : Set (Set α)) ⊆ memPartition t n ∧ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑S_1 : Set (Set α))
have refine_1 : (↑((memPartition t n).toFinset \ S) : Set (Set α)) ⊆ memPartition t n
Tactic: refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩
-- 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: refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩
-- 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 α)))
⊢ (↑((memPartition t n).toFinset \ S) : Set (Set α)) ⊆ memPartition t n
have refine_1 : memPartition t n \ (↑S : Set (Set α)) ⊆ memPartition t n
Tactic: simp only [Finset.coe_sdiff, coe_toFinset]
-- 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 α)))
⊢ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑((memPartition t n).toFinset \ S) : Set (Set α))
have refine_1 : (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (memPartition t n \ (↑S : Set (Set α)))
Tactic: simp only [Finset.coe_sdiff, coe_toFinset]
-- 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 α)))
⊢ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (memPartition t n \ (↑S : Set (Set α)))
have refine_1 : Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))
Tactic: refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm
-- 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 : Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))
⊢ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (memPartition t n \ (↑S : Set (Set α)))
have refine_1₁ : Codisjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))
Tactic: refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm
-- 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 α)))
⊢ Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))
have refine_1 : ∀ (u : Set α) (huS : u ∈ (↑S : Set (Set α))), Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) u
Tactic: refine Set.disjoint_sUnion_right.mpr fun u huS => ?_
-- 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 α)))
u : Set α
huS : u ∈ (↑S : Set (Set α))
⊢ Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) u
have refine_1 : ∀ (v : Set α) (huV : v ∈ memPartition t n \ (↑S : Set (Set α))), Disjoint v u
Tactic: refine Set.disjoint_sUnion_left.mpr fun v huV => ?_
-- 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 α)))
u : Set α
huS : u ∈ (↑S : Set (Set α))
v : Set α
huV : v ∈ memPartition t n \ (↑S : Set (Set α))
⊢ Disjoint v u
have refine_1 : v ≠ u
Tactic: refine disjoint_memPartition t n (mem_of_mem_diff huV) (hS_subset huS) ?_
-- 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 α)))
⊢ Codisjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))
have refine_1 : ⋃₀ (memPartition t n \ (↑S : Set (Set α))) ⊔ ⋃₀ (↑S : Set (Set α)) = ⊤
Tactic: rw [codisjoint_iff]
-- 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 α)))
⊢ ⋃₀ (memPartition t n \ (↑S : Set (Set α))) ∪ ⋃₀ (↑S : Set (Set α)) = univ
have refine_1 : ⋃₀ (memPartition t n \ (↑S : Set (Set α))) ∪ ⋃₀ (↑S : Set (Set α)) = ⋃₀ memPartition t n
Tactic: 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 α
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
⊢ ⋃₀ (memPartition t n \ (↑S : Set (Set α))) ∪ ⋃₀ (↑S : Set (Set α)) = univ
have refine_1₁ : ⋃₀ (↑S : Set (Set α)) ∪ ⋃₀ (memPartition t n \ (↑S : Set (Set α))) = ⋃₀ memPartition t n
Tactic: 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 α
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
⊢ ⋃₀ (memPartition t n \ (↑S : Set (Set α))) ∪ ⋃₀ (↑S : Set (Set α)) = univ
have refine_1₂ : ⋃₀ ((↑S : Set (Set α)) ∪ memPartition t n \ (↑S : Set (Set α))) = ⋃₀ memPartition t n
Tactic: 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 α
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
⊢ ⋃₀ (memPartition t n \ (↑S : Set (Set α))) ∪ ⋃₀ (↑S : Set (Set α)) = univ
have refine_1₃ : ⋃₀ memPartition t n = ⋃₀ memPartition t n
Tactic: 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 α
S : Finset (Set α)
hS_subset : (↑S : Set (Set α)) ⊆ memPartition t n
ht : MeasurableSet (⋃₀ (↑S : Set (Set α)))
⊢ ∃ (S_1 : Finset (Set α)), (↑S_1 : Set (Set α)) ⊆ memPartition t n ∧ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑S_1 : Set (Set α))
have refine_1 : (↑((memPartition t n).toFinset \ S) : Set (Set α)) ⊆ memPartition t n
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]