awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
union : ∀ a ∈ Au ∪ Av, a.Finite
union₁ : ∀ a ∈ Au ∪ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
refine ⟨Au ∪ Av, Au_fin.union Av_fin, ?_, ?_, by rw [u_eq, v_eq, ← biUnion_union]⟩
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
⊢ a.Finite

Tactic:
mem_Au a ha
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
⊢ a.Finite

Tactic:
exact mem_Au a ha
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
⊢ a.Finite

Tactic:
mem_Av a ha
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
⊢ a.Finite

Tactic:
exact mem_Av a ha
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht_1 : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
hAu a ha t ht
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht_1 : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
exact hAu a ha t ht
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht_1 : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
hAv a ha t ht
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht_1 : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
exact hAv a ha t ht
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
apply : Set.Countable.{u_1} (α := Set α) {s : Set α | sᶜ ∈ 𝒜}
⊢ ℬ.Countable

Tactic:
apply h.union

Premises used: Set.Countable.union
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
h₁ : ∀ (s : Set α), s ∈ compl '' 𝒜 ↔ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ 𝒜} s
⊢ compl '' 𝒜 = {s : Set α | sᶜ ∈ 𝒜}

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
s : Set α
h_1 : ∃ x ∈ 𝒜, xᶜ = s
x : Set α
x_mem : x ∈ 𝒜
hx : xᶜ = s
⊢ sᶜ ∈ 𝒜

Tactic:
simp [← hx, x_mem]
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
s : Set α
hs : sᶜ ∈ 𝒜
⊢ sᶜᶜ = s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
s : Set α
⊢ s ∈ compl '' 𝒜 ↔ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ 𝒜} s

Tactic:
simpa using ⟨fun ⟨x, x_mem, hx⟩ ↦ by simp [← hx, x_mem], fun hs ↦ ⟨sᶜ, hs, by simp⟩⟩
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
⊢ compl '' 𝒜 = {s : Set α | sᶜ ∈ 𝒜}

Tactic:
have : compl '' 𝒜 = {s | sᶜ ∈ 𝒜} := by
      ext s
      simpa using ⟨fun ⟨x, x_mem, hx⟩ ↦ by simp [← hx, x_mem], fun hs ↦ ⟨sᶜ, hs, by simp⟩⟩
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
this : compl '' 𝒜 = {s : Set α | sᶜ ∈ 𝒜}
⊢ Set.Countable.{u_1} (α := Set α) {s : Set α | sᶜ ∈ 𝒜}

Tactic:
this ▸ h.image compl

Premises used: Compl.compl, Eq.rec, Set.Countable.image
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
this : compl '' 𝒜 = {s : Set α | sᶜ ∈ 𝒜}
⊢ Set.Countable.{u_1} (α := Set α) {s : Set α | sᶜ ∈ 𝒜}

Tactic:
exact this ▸ h.image compl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
⊢ ℬ.Countable

Tactic:
have count_ℬ : ℬ.Countable := by
    apply h.union
    have : compl '' 𝒜 = {s | sᶜ ∈ 𝒜} := by
      ext s
      simpa using ⟨fun ⟨x, x_mem, hx⟩ ↦ by simp [← hx, x_mem], fun hs ↦ ⟨sᶜ, hs, by simp⟩⟩
    exact this ▸ h.image compl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
⊢ 𝒞.Countable

Tactic:
have count_𝒞 : 𝒞.Countable := countable_setOf_finite_subset (countable_coe_iff.1 count_ℬ)
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
⊢ 𝒟.Countable

Tactic:
have count_𝒟 : 𝒟.Countable := countable_setOf_finite_subset (countable_coe_iff.1 count_𝒞)
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
s : Set α
s_mem : s ∈ generateSetAlgebra 𝒜
rcases :
  ∀ (A : Set (Set (Set α))) (A_fin : A.Finite) (mem_A : ∀ a ∈ A, a.Finite) (hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜)
    (s_mem : ⋃ a ∈ A, ⋂ t ∈ a, t ∈ generateSetAlgebra 𝒜), ⋃ a ∈ A, ⋂ t ∈ a, t ∈ f '' 𝒟
⊢ s ∈ f '' 𝒟

Tactic:
rcases mem_generateSetAlgebra_elim s_mem with ⟨A, A_fin, mem_A, hA, rfl⟩

Premises used: MeasureTheory.mem_generateSetAlgebra_elim, rfl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
s_mem : ⋃ a ∈ A, ⋂ t ∈ a, t ∈ generateSetAlgebra 𝒜
⊢ ⋃ a ∈ A, ⋂ t ∈ a, t ∈ f '' 𝒟

Tactic:
⟨A, ⟨A_fin, fun a ha ↦ ⟨mem_A a ha, hA a ha⟩⟩, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
s_mem : ⋃ a ∈ A, ⋂ t ∈ a, t ∈ generateSetAlgebra 𝒜
⊢ ⋃ a ∈ A, ⋂ t ∈ a, t ∈ f '' 𝒟

Tactic:
exact ⟨A, ⟨A_fin, fun a ha ↦ ⟨mem_A a ha, hA a ha⟩⟩, rfl⟩
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
⊢ generateSetAlgebra 𝒜 ⊆ f '' 𝒟

Tactic:
have : generateSetAlgebra 𝒜 ⊆ f '' 𝒟 := by
    intro s s_mem
    rcases mem_generateSetAlgebra_elim s_mem with ⟨A, A_fin, mem_A, hA, rfl⟩
    exact ⟨A, ⟨A_fin, fun a ha ↦ ⟨mem_A a ha, hA a ha⟩⟩, rfl⟩
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
this : generateSetAlgebra 𝒜 ⊆ f '' 𝒟
⊢ (generateSetAlgebra 𝒜).Countable

Tactic:
(count_𝒟.image f).mono this

Premises used: Set.Countable.image, Set.Countable.mono
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
this : generateSetAlgebra 𝒜 ⊆ f '' 𝒟
⊢ (generateSetAlgebra 𝒜).Countable

Tactic:
exact (count_𝒟.image f).mono this

Premises used: Set.Countable.image, Set.Countable.mono
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
⊢ IsPiSystem C

Tactic:
fun s hs t ht _ ↦ hC.inter_mem s hs t ht

Premises used: IsPiSystem, MeasureTheory.IsSetSemiring.inter_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
obtain :
  ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
    (hst : s \ t = ⋃₀ (↑I : Set (Set α))), ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C

Tactic:
obtain ⟨I, hIC, hI, hst⟩ := hC.diff_eq_sUnion' s hs t ht

Premises used: MeasureTheory.IsSetSemiring.diff_eq_sUnion'
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C

Tactic:
⟨.ofErase I (supIndep_iff_pairwiseDisjoint.mpr hI) ?_, ?_⟩

Premises used: Iff.mpr, Finset.supIndep_iff_pairwiseDisjoint, Finpartition.ofErase, Exists.intro
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
refine_1 : I.sup id = s \ t
refine_2 : (↑((Finpartition.ofErase (a := s \ t) I ⋯ ⋯).parts (a := s \ t)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C

Tactic:
refine ⟨.ofErase I (supIndep_iff_pairwiseDisjoint.mpr hI) ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
refine_1 : sSup (↑I : Set (Set α)) = s \ t
refine_1₁ : ⋃₀ (↑I : Set (Set α)) = s \ t
refine_1₂ refine_1₃ : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑I : Set (Set α))
⊢ I.sup id = s \ t

Tactic:
rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]

Premises used: Set.sSup_eq_sUnion, Finset.sup_id_eq_sSup
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
refine_2 : (↑(I.erase ⊥) : Set (Set α)) ⊆ C
refine_2₁ : (↑I : Set (Set α)) ⊆ C
refine_2₂ refine_2₃ : C ⊆ C
⊢ (↑((Finpartition.ofErase (a := s \ t) I ⋯ ⋯).parts (a := s \ t)) : Set (Set α)) ⊆ C

Tactic:
grw [Finpartition.ofErase_parts, Finset.erase_subset, hIC]

Premises used: Finpartition.ofErase_parts, Finset.erase_subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
obtain :
  ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
    (hst : s \ t = ⋃₀ (↑I : Set (Set α))), ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
refine_1 :
  ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
    (hst : s \ t = ⋃₀ (↑I : Set (Set α))), I.sup id = s \ t
refine_2 refine_2₁ :
  ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
    (hst : s \ t = ⋃₀ (↑I : Set (Set α))),
    (↑((Finpartition.ofErase (a := s \ t) I ⋯ ⋯).parts (a := s \ t)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C

Tactic:
classical
  obtain ⟨I, hIC, hI, hst⟩ := hC.diff_eq_sUnion' s hs t ht
  refine ⟨.ofErase I (supIndep_iff_pairwiseDisjoint.mpr hI) ?_, ?_⟩
  · rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]
  · grw [Finpartition.ofErase_parts, Finset.erase_subset, hIC]

Premises used: Finpartition.ofErase_parts, MeasureTheory.IsSetSemiring.diff_eq_sUnion', Set.sSup_eq_sUnion, Finset.sup_id_eq_sSup, Finset.erase_subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
hS : S.Nonempty
hSC : (↑S : Set (Set α)) ⊆ C
rw : ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup' hS id)), (↑(P.parts (a := S.sup' hS id)) : Set (Set α)) ⊆ C

Tactic:
rw [sup'_eq_sup]

Premises used: Finset.sup'_eq_sup
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
hSC : (↑∅ : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (α := Set α) ⊥), (↑(P.parts (a := ⊥)) : Set (Set α)) ⊆ C

Tactic:
⟨.empty _, hSC⟩

Premises used: Finpartition.empty, Exists.intro
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
hSC : (↑∅ : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (α := Set α) ⊥), (↑(P.parts (a := ⊥)) : Set (Set α)) ⊆ C

Tactic:
exact ⟨.empty _, hSC⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : (↑(insert s S) : Set (Set α)) ⊆ C
⊢ s ∈ C ∧ (↑S : Set (Set α)) ⊆ C

Tactic:
rw [coe_insert, insert_subset_iff] at hSC

Premises used: Set.insert_subset_iff, Finset.coe_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : s ∈ C ∧ (↑S : Set (Set α)) ⊆ C
⊢ s ∈ C

Tactic:
obtain ⟨hsC, hSC⟩ := hSC
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : s ∈ C ∧ (↑S : Set (Set α)) ⊆ C
hsC : s ∈ C
⊢ (↑S : Set (Set α)) ⊆ C

Tactic:
obtain ⟨hsC, hSC⟩ := hSC
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
insert :
  ∀ (P : Finpartition (S.sup id)) (hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C),
    ∃ (P : Finpartition ((Insert.insert s S).sup id)), (↑(P.parts (a := (Insert.insert s S).sup id)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition ((Insert.insert s S).sup id)), (↑(P.parts (a := (Insert.insert s S).sup id)) : Set (Set α)) ⊆ C

Tactic:
obtain ⟨P, hP⟩ := ih hSC
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
insert : ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition ((Insert.insert s S).sup id)), (↑(P.parts (a := (Insert.insert s S).sup id)) : Set (Set α)) ⊆ C

Tactic:
rw [sup_insert, sup_comm, id]

Premises used: Finset.sup_insert, id, sup_comm
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
insert :
  ⊥ ∉ S → ∀ (hsC : ⊥ ∈ C), ∃ (P : Finpartition (S.sup id ⊔ ⊥)), (↑(P.parts (a := S.sup id ⊔ ⊥)) : Set (Set α)) ⊆ C
insert₁ : ∀ (hs : s ≠ ⊥), ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C

Tactic:
rcases eq_or_ne s ⊥ with rfl | hs

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
h : ⊥ ∉ S
hsC : ⊥ ∈ C
insert : ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup id ⊔ ⊥)), (↑(P.parts (a := S.sup id ⊔ ⊥)) : Set (Set α)) ⊆ C

Tactic:
rw [sup_bot_eq]

Premises used: sup_bot_eq
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
h : ⊥ ∉ S
hsC : ⊥ ∈ C
⊢ ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C

Tactic:
⟨P, hP⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
h : ⊥ ∉ S
hsC : ⊥ ∈ C
⊢ ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C

Tactic:
exact ⟨P, hP⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
simp_rw :
  ∀ (t : Set α),
    (∃ d ∈ P.parts (a := S.sup id), ¬d ≤ s ∧ d \ s = t) →
      ∃ (Q : Finpartition t), (↑(Q.parts (a := t)) : Set (Set α)) ⊆ C
⊢ ∀ t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s),
    ∃ (Q : Finpartition t), (↑(Q.parts (a := t)) : Set (Set α)) ⊆ C

Tactic:
simp_rw [Finpartition.mem_avoid]

Premises used: Finpartition.mem_avoid
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
t : Set α
ht : t ∈ P.parts (a := S.sup id)
⊢ ∃ (Q : Finpartition (t \ s)), (↑(Q.parts (a := t \ s)) : Set (Set α)) ⊆ C

Tactic:
hC.exists_finpartition_diff (hP ht) hsC

Premises used: setOf, MeasureTheory.IsSetSemiring.exists_finpartition_diff