awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
measurable_invFun :
  autoParam
    (Measurable (α := (↑(range (mapNatBool α)) : Type)) (β := α)
      (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α))
    MeasurableEquiv.measurable_invFun._autoParam
⊢ ∃ (s : Set (ℕ → Bool)), Nonempty.{max 1 (u_1 + 1)} (α ≃ᵐ (↑s : Type))

Tactic:
use range (mapNatBool α), Equiv.ofInjective _ <|
    injective_mapNatBool _,
    Measurable.subtype_mk <| measurable_mapNatBool _

Premises used: Measurable.subtype_mk, Equiv.ofInjective, Set.range, MeasurableSpace.measurable_mapNatBool, MeasurableSpace.injective_mapNatBool, MeasurableSpace.mapNatBool
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
measurable_invFun :
  autoParam
    (Measurable (α := (↑(range (mapNatBool α)) : Type)) (β := α)
      (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α))
    MeasurableEquiv.measurable_invFun._autoParam
⊢ autoParam
    (Measurable (α := (↑(range (mapNatBool α)) : Type)) (β := α)
      (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α))
    MeasurableEquiv.measurable_invFun._autoParam

Tactic:
simp_rw +instances [← generateFrom_natGeneratingSequence α]

Premises used: MeasurableSpace.generateFrom_natGeneratingSequence
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
measurable_invFun :
  ∀ t ∈ range (natGeneratingSequence α),
    MeasurableSet (α := (↑(range (mapNatBool α)) : Type))
      ((⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α) ⁻¹' t)
⊢ autoParam
    (Measurable (α := (↑(range (mapNatBool α)) : Type)) (β := α)
      (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α))
    MeasurableEquiv.measurable_invFun._autoParam

Tactic:
apply measurable_generateFrom

Premises used: measurable_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
n : ℕ
measurable_invFun :
  MeasurableSet (α := (↑(range (mapNatBool α)) : Type))
    ((⇑(Equiv.ofInjective (mapNatBool α) ⋯) : (a : α) → (↑(range (mapNatBool α)) : Type)) '' natGeneratingSequence α n)
⊢ MeasurableSet (α := (↑(range (mapNatBool α)) : Type))
    ((⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm : (a : (↑(range (mapNatBool α)) : Type)) → α) ⁻¹'
      natGeneratingSequence α n)

Tactic:
rw [← Equiv.image_eq_preimage_symm _ _]

Premises used: Equiv.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (α := ℕ → Bool) {y : ℕ → Bool | y n = true}

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
n : ℕ
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 α) ⋯) : (a : α) → (↑(range (mapNatBool α)) : Type)) '' natGeneratingSequence α n)
⊢ MeasurableSet (α := (↑(range (mapNatBool α)) : Type))
    ((⇑(Equiv.ofInjective (mapNatBool α) ⋯) : (a : α) → (↑(range (mapNatBool α)) : Type)) '' natGeneratingSequence α n)

Tactic:
refine ⟨{y | y n}, by measurability, ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
n : ℕ
measurable_invFun :
  preimage (β := { x : ℕ → Bool // x ∈ range (mapNatBool α) })
      (⇑(Equiv.ofInjective (mapNatBool α) ⋯) : (a : α) → { x : ℕ → Bool // x ∈ range (mapNatBool α) })
      (Subtype.val (p := fun (x : ℕ → Bool) ↦ x ∈ range (mapNatBool α)) ⁻¹' {y : ℕ → Bool | y n = true}) =
    natGeneratingSequence α 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)

Tactic:
rw [← Equiv.preimage_eq_iff_eq_image]

Premises used: Equiv.preimage_eq_iff_eq_image
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
n : ℕ
⊢ preimage (β := { x : ℕ → Bool // x ∈ range (mapNatBool α) })
      (⇑(Equiv.ofInjective (mapNatBool α) ⋯) : (a : α) → { x : ℕ → Bool // x ∈ range (mapNatBool α) })
      (Subtype.val (p := fun (x : ℕ → Bool) ↦ x ∈ range (mapNatBool α)) ⁻¹' {y : ℕ → Bool | y n = true}) =
    natGeneratingSequence α n

Tactic:
simp [mapNatBool]

Premises used: MeasurableSpace.mapNatBool
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
rcases :
  ∀ (m' : MeasurableSpace α),
    CountablyGenerated α → SeparatesPoints α → ∀ (m'le : m' ≤ inst), ∃ (f : α → ℕ → Bool), Measurable f ∧ Injective f
⊢ ∃ (f : α → ℕ → Bool), Measurable f ∧ Injective f

Tactic:
rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩

Premises used: MeasurableSpace.exists_countablyGenerated_le_of_countablySeparated
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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

Tactic:
⟨mapNatBool α, ?_, injective_mapNatBool _⟩

Premises used: And.intro, Exists.intro, MeasurableSpace.injective_mapNatBool, MeasurableSpace.mapNatBool
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
m' : MeasurableSpace α
left : CountablyGenerated α
left_1 : SeparatesPoints α
m'le : m' ≤ inst
refine : Measurable (mapNatBool α)
⊢ ∃ (f : α → ℕ → Bool), Measurable f ∧ Injective f

Tactic:
refine ⟨mapNatBool α, ?_, injective_mapNatBool _⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
m' : MeasurableSpace α
left : CountablyGenerated α
left_1 : SeparatesPoints α
m'le : m' ≤ inst
⊢ Measurable (mapNatBool α)

Tactic:
(measurable_mapNatBool _).mono m'le le_rfl

Premises used: le_rfl, MeasurableSpace.measurable_mapNatBool, Measurable.mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
m' : MeasurableSpace α
left : CountablyGenerated α
left_1 : SeparatesPoints α
m'le : m' ≤ inst
⊢ Measurable (mapNatBool α)

Tactic:
exact (measurable_mapNatBool _).mono m'le le_rfl

Premises used: le_rfl, MeasurableSpace.measurable_mapNatBool, Measurable.mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
rcases : ∀ (f : α → ℕ → Bool) (fmeas : Measurable f) (finj : Injective f), MeasurableSingletonClass α
⊢ MeasurableSingletonClass α

Tactic:
rcases measurable_injection_nat_bool_of_countablySeparated α with ⟨f, fmeas, finj⟩

Premises used: MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
⊢ MeasurableSingletonClass α

Tactic:
⟨fun x ↦ ?_⟩

Premises used: MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
refine : ∀ (x : α), MeasurableSet (α := α) {x}
⊢ MeasurableSingletonClass α

Tactic:
refine ⟨fun x ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
rw : MeasurableSet (f ⁻¹' {f x})
⊢ MeasurableSet (α := α) {x}

Tactic:
rw [← finj.preimage_image {x}, image_singleton]

Premises used: Set.image_singleton, Function.Injective.preimage_image, Singleton.singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' {f x})

Tactic:
fmeas <| MeasurableSet.singleton _

Premises used: MeasurableSet.singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' {f x})

Tactic:
exact fmeas <| MeasurableSet.singleton _

Premises used: MeasurableSet.singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
rw : MeasurableSet (s \ t n ∪ s ∩ t n)
⊢ MeasurableSet s

Tactic:
rw [← diff_union_inter s (t n)]

Premises used: Set.diff_union_inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n ∪ s ∩ t n)

Tactic:
MeasurableSet.union ?_ ?_

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
refine_1 : MeasurableSet (s \ t n)
refine_2 : MeasurableSet (s ∩ t n)
⊢ MeasurableSet (s \ t n ∪ s ∩ t n)

Tactic:
refine MeasurableSet.union ?_ ?_

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n)

Tactic:
measurableSet_generateFrom ?_

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
refine_1 : s \ t n ∈ memPartition t (n + 1)
⊢ MeasurableSet (s \ t n)

Tactic:
refine measurableSet_generateFrom ?_

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s \ t n = s ∩ t n ∨ s \ t n = s \ t n

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n} (s \ t n)

Tactic:
exact ⟨s, hs, by simp⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s ∩ t n)

Tactic:
measurableSet_generateFrom ?_

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
refine_2 : s ∩ t n ∈ memPartition t (n + 1)
⊢ MeasurableSet (s ∩ t n)

Tactic:
refine measurableSet_generateFrom ?_

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n = s ∩ t n ∨ s ∩ t n = s \ t n

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n} (s ∩ t n)

Tactic:
exact ⟨s, hs, by simp⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (memPartition t (n + 1))

Tactic:
generateFrom_le (fun _ hs ↦ measurableSet_succ_memPartition t n hs)

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

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

Premises used: MeasurableSet, _private.0.MeasurableSpace.measurableSet_generateFrom_memPartition_iff.match_1, Iff.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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 α))
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
⊢ 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⟩ ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
hu : u ∈ memPartition t n
ht : MeasurableSet u
⊢ (↑{u} : Set (Set α)) ⊆ memPartition t n

Tactic:
simp [hu]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
hu : u ∈ memPartition t n
ht : MeasurableSet u
⊢ u = ⋃₀ (↑{u} : Set (Set α))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
hu : u ∈ memPartition t n
ht : MeasurableSet u
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ u = ⋃₀ (↑S : Set (Set α))

Tactic:
exact ⟨{u}, by simp [hu], by simp⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ (↑∅ : Set (Set α)) ⊆ memPartition t n

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ ∅ = ⋃₀ (↑∅ : Set (Set α))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ ∅ = ⋃₀ (↑S : Set (Set α))

Tactic:
exact ⟨∅, by simp, by simp⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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 α))
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 α))
⊢ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ memPartition t n ∧ uᶜ = ⋃₀ (↑S : Set (Set α))

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

Premises used: rfl
-- 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 α)))
⊢ ∃ (S_1 : Finset (Set α)), (↑S_1 : Set (Set α)) ⊆ memPartition t n ∧ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑S_1 : Set (Set α))

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

Premises used: memPartition, Set.toFinset, SDiff.sdiff, And.intro, Exists.intro
-- 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₁ : (⋃₀ (↑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:
refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩
-- 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 α)) ⊆ memPartition t n
⊢ (↑((memPartition t n).toFinset \ S) : Set (Set α)) ⊆ memPartition t n

Tactic:
simp only [Finset.coe_sdiff, coe_toFinset]

Premises used: Finset.coe_sdiff, Set.coe_toFinset
-- 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 α)))
⊢ memPartition t n \ (↑S : Set (Set α)) ⊆ memPartition t n

Tactic:
diff_subset

Premises used: Set.diff_subset
-- 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 α)))
⊢ memPartition t n \ (↑S : Set (Set α)) ⊆ memPartition t n

Tactic:
exact diff_subset

Premises used: Set.diff_subset
-- 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 : (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (memPartition t n \ (↑S : Set (Set α)))
⊢ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (↑((memPartition t n).toFinset \ S) : Set (Set α))

Tactic:
simp only [Finset.coe_sdiff, coe_toFinset]

Premises used: Finset.coe_sdiff, Set.coe_toFinset
-- 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 α)))
⊢ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (memPartition t n \ (↑S : Set (Set α)))

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

Premises used: IsCompl.mk, Eq.symm, IsCompl.eq_compl
-- 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 : Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))
refine_1₁ : Codisjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))
⊢ (⋃₀ (↑S : Set (Set α)))ᶜ = ⋃₀ (memPartition t n \ (↑S : Set (Set α)))

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

Premises used: IsCompl.mk, Eq.symm, IsCompl.eq_compl
-- 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 α)))
⊢ Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))

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

Premises used: Iff.mpr, Set.disjoint_sUnion_right
-- 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 : ∀ (u : Set α) (huS : u ∈ (↑S : Set (Set α))), Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) u
⊢ Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))

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

Premises used: Iff.mpr, Set.disjoint_sUnion_right
-- 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 α)))
u : Set α
huS : u ∈ (↑S : Set (Set α))
⊢ Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) u

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

Premises used: Iff.mpr, Set.disjoint_sUnion_left
-- 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 α)))
u : Set α
huS : u ∈ (↑S : Set (Set α))
refine_1 : ∀ (v : Set α) (huV : v ∈ memPartition t n \ (↑S : Set (Set α))), Disjoint v u
⊢ Disjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) u

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

Premises used: Iff.mpr, Set.disjoint_sUnion_left
-- 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 α)))
u : Set α
huS : u ∈ (↑S : Set (Set α))
v : Set α
huV : v ∈ memPartition t n \ (↑S : Set (Set α))
⊢ Disjoint v u

Tactic:
disjoint_memPartition t n (mem_of_mem_diff huV) (hS_subset huS) ?_

Premises used: Set.mem_of_mem_diff, disjoint_memPartition
-- 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 α)))
u : Set α
huS : u ∈ (↑S : Set (Set α))
v : Set α
huV : v ∈ memPartition t n \ (↑S : Set (Set α))
refine_1 : v ≠ u
⊢ Disjoint v u

Tactic:
refine disjoint_memPartition t n (mem_of_mem_diff huV) (hS_subset huS) ?_

Premises used: Set.mem_of_mem_diff, disjoint_memPartition
-- 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 α)))
u : Set α
huS : u ∈ (↑S : Set (Set α))
v : Set α
huV : v ∈ memPartition t n \ (↑S : Set (Set α))
⊢ v ≠ u

Tactic:
ne_of_mem_of_not_mem huS (notMem_of_mem_diff huV) |>.symm

Premises used: Ne.symm, ne_of_mem_of_not_mem, Set.notMem_of_mem_diff
-- 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 α)))
u : Set α
huS : u ∈ (↑S : Set (Set α))
v : Set α
huV : v ∈ memPartition t n \ (↑S : Set (Set α))
⊢ v ≠ u

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

Premises used: Ne.symm, ne_of_mem_of_not_mem, Set.notMem_of_mem_diff
-- 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 α)) = ⊤
⊢ Codisjoint (⋃₀ (memPartition t n \ (↑S : Set (Set α)))) (⋃₀ (↑S : Set (Set α)))

Tactic:
rw [codisjoint_iff]

Premises used: codisjoint_iff