awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t u : Set α
hu : u ∈ s
⊢ C u ⋯

Tactic:
exact basic u hu
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
⊢ C ∅ ⋯

Tactic:
empty
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
⊢ C ∅ ⋯

Tactic:
exact empty
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t u : Set α
hu : DynkinSystem.GenerateHas s u
ihu : C u ⋯
⊢ C uᶜ ⋯

Tactic:
compl _ (eq ▸ hu) ihu
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t u : Set α
hu : DynkinSystem.GenerateHas s u
ihu : C u ⋯
⊢ C uᶜ ⋯

Tactic:
exact compl _ (eq ▸ hu) ihu
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i)
ihf : ∀ (i : ℕ), C (f i) ⋯
⊢ C (⋃ (i : ℕ), f i) ⋯

Tactic:
iUnion f hfd (eq ▸ hf) ihf

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i)
ihf : ∀ (i : ℕ), C (f i) ⋯
⊢ C (⋃ (i : ℕ), f i) ⋯

Tactic:
exact iUnion f hfd (eq ▸ hf) ihf

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht : DynkinSystem.GenerateHas s t
basic₁ : ∀ (u : Set α) (hu : u ∈ s), C u ⋯
empty₁ : C ∅ ⋯
compl₁ : ∀ {u : Set α} (hu : DynkinSystem.GenerateHas s u) (ihu : C u ⋯), C uᶜ ⋯
iUnion₁ :
  ∀ {f : ℕ → Set α} (hfd : Pairwise (Disjoint on f)) (hf : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i))
    (ihf : ∀ (i : ℕ), C (f i) ⋯), C (⋃ (i : ℕ), f i) ⋯
⊢ C t ⋯

Tactic:
induction ht with
  | basic u hu => exact basic u hu
  | empty => exact empty
  | @compl u hu ihu => exact compl _ (eq ▸ hu) ihu
  | @iUnion f hfd hf ihf => exact iUnion f hfd (eq ▸ hf) ihf
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h𝒜 : IsSetAlgebra 𝒜
⊢ univ ∈ 𝒜

Tactic:
compl_empty ▸ h𝒜.compl_mem h𝒜.empty_mem

Premises used: MeasureTheory.IsSetAlgebra.compl_mem, Eq.rec, Set.compl_empty, MeasureTheory.IsSetAlgebra.empty_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
h𝒜 : IsSetAlgebra 𝒜
s_mem : s ∈ 𝒜
t_mem : t ∈ 𝒜
⊢ s ∩ t ∈ 𝒜

Tactic:
inter_eq_compl_compl_union_compl .. ▸
    h𝒜.compl_mem (h𝒜.union_mem (h𝒜.compl_mem s_mem) (h𝒜.compl_mem t_mem))

Premises used: MeasureTheory.IsSetAlgebra.compl_mem, Set.inter_eq_compl_compl_union_compl, Eq.rec, MeasureTheory.IsSetAlgebra.union_mem, Eq.symm
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
h𝒜 : IsSetAlgebra 𝒜
s_mem : s ∈ 𝒜
t_mem : t ∈ 𝒜
⊢ s \ t ∈ 𝒜

Tactic:
h𝒜.inter_mem s_mem (h𝒜.compl_mem t_mem)

Premises used: MeasureTheory.IsSetAlgebra.compl_mem, Set.Mem, Set.diff, setOf, MeasureTheory.IsSetAlgebra.inter_mem, Not
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
⊢ ⋃ i ∈ S, s i ∈ 𝒜

Tactic:
h𝒜.isSetRing.biUnion_mem S hs

Premises used: MeasureTheory.IsSetAlgebra.isSetRing, MeasureTheory.IsSetRing.biUnion_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
pos : ∀ (h : S = ∅), ⋂ i ∈ S, s i ∈ 𝒜
neg : ∀ (h : S.Nonempty), ⋂ i ∈ S, s i ∈ 𝒜
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
by_cases! h : S = ∅
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
pos : univ ∈ 𝒜
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
rw [h, ← Finset.set_biInter_coe, Finset.coe_empty, biInter_empty]

Premises used: Finset.coe_empty, Finset.set_biInter_coe, Set.biInter_empty
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ univ ∈ 𝒜

Tactic:
h𝒜.univ_mem

Premises used: MeasureTheory.IsSetAlgebra.univ_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ univ ∈ 𝒜

Tactic:
exact h𝒜.univ_mem

Premises used: MeasureTheory.IsSetAlgebra.univ_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S.Nonempty
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
h𝒜.isSetRing.biInter_mem S h hs

Premises used: MeasureTheory.IsSetRing.biInter_mem, MeasureTheory.IsSetAlgebra.isSetRing
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S.Nonempty
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
exact h𝒜.isSetRing.biInter_mem S h hs

Premises used: MeasureTheory.IsSetRing.biInter_mem, MeasureTheory.IsSetAlgebra.isSetRing
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
⊢ 𝒜 ⊆ generateSetAlgebra 𝒜

Tactic:
fun _ ↦ generateSetAlgebra.base _

Premises used: MeasureTheory.generateSetAlgebra.base, Set.Mem, Set.Subset
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
⊢ generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜

Tactic:
le_antisymm (fun s ms ↦ ?_) (generateFrom_mono self_subset_generateSetAlgebra)

Premises used: MeasurableSpace.generateFrom_mono, MeasureTheory.self_subset_generateSetAlgebra, le_antisymm
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
refine : ∀ (s : Set α) (ms : MeasurableSet s), MeasurableSet s
⊢ generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜

Tactic:
refine le_antisymm (fun s ms ↦ ?_) (generateFrom_mono self_subset_generateSetAlgebra)

Premises used: MeasurableSpace.generateFrom_mono, MeasureTheory.self_subset_generateSetAlgebra, le_antisymm
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t u : Set α
u_mem : u ∈ 𝒜
⊢ MeasurableSet u

Tactic:
measurableSet_generateFrom u_mem

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t u : Set α
u_mem : u ∈ 𝒜
⊢ MeasurableSet u

Tactic:
exact measurableSet_generateFrom u_mem

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
@MeasurableSet.empty _ (generateFrom 𝒜)

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
exact @MeasurableSet.empty _ (generateFrom 𝒜)

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t u : Set α
hs : generateSetAlgebra 𝒜 u
mu : MeasurableSet u
⊢ MeasurableSet uᶜ

Tactic:
mu.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t u : Set α
hs : generateSetAlgebra 𝒜 u
mu : MeasurableSet u
⊢ MeasurableSet uᶜ

Tactic:
exact mu.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
mu : MeasurableSet u
mv : MeasurableSet v
⊢ MeasurableSet (u ∪ v)

Tactic:
MeasurableSet.union mu mv

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
mu : MeasurableSet u
mv : MeasurableSet v
⊢ MeasurableSet (u ∪ v)

Tactic:
exact MeasurableSet.union mu mv

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht : t ∈ generateSetAlgebra 𝒜
hC : ∀ (u : Set α) (u_mem : u ∈ 𝒜), MeasurableSet u
hC₁ : MeasurableSet.{u_1} (α := α) ∅
hC₂ : ∀ (u : Set α), generateSetAlgebra 𝒜 u → ∀ (mu : MeasurableSet u), MeasurableSet uᶜ
hC₃ :
  ∀ (u v : Set α),
    generateSetAlgebra 𝒜 u →
      generateSetAlgebra 𝒜 v → ∀ (mu : MeasurableSet u) (mv : MeasurableSet v), MeasurableSet (u ∪ v)
⊢ MeasurableSet t

Tactic:
induction ht with
    | base u u_mem => exact measurableSet_generateFrom u_mem
    | empty => exact @MeasurableSet.empty _ (generateFrom 𝒜)
    | compl u _ mu => exact mu.compl
    | union u v _ _ mu mv => exact MeasurableSet.union mu mv

Premises used: MeasurableSet.empty, Compl.compl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
MeasurableSpace.measurableSet_empty _

Premises used: MeasurableSet, MeasurableSpace.measurableSet_empty
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
exact MeasurableSpace.measurableSet_empty _

Premises used: MeasurableSpace.measurableSet_empty
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht_1 : MeasurableSet t
ht : MeasurableSet t
⊢ MeasurableSet tᶜ

Tactic:
ht.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht_1 : MeasurableSet t
ht : MeasurableSet t
⊢ MeasurableSet tᶜ

Tactic:
exact ht.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
t : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (t n)
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), t i)

Tactic:
.iUnion ht

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
t : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (t n)
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), t i)

Tactic:
exact .iUnion ht
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
ms : MeasurableSet s
hC : ∀ (t : Set α) (ht : t ∈ generateSetAlgebra 𝒜) (h : MeasurableSet t), MeasurableSet t
empty : MeasurableSet.{u_1} (α := α) ∅
compl : ∀ (t : Set α), MeasurableSet t → ∀ (ht : MeasurableSet t), MeasurableSet tᶜ
iUnion :
  ∀ (t : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (t n)) →
      ∀ (ht : ∀ (n : ℕ), MeasurableSet (t n)), MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), t i)
⊢ MeasurableSet s

Tactic:
induction s, ms using generateFrom_induction with
  | hC t ht h =>
    clear h
    induction ht with
    | base u u_mem => exact measurableSet_generateFrom u_mem
    | empty => exact @MeasurableSet.empty _ (generateFrom 𝒜)
    | compl u _ mu => exact mu.compl
    | union u v _ _ mu mv => exact MeasurableSet.union mu mv
  | empty => exact MeasurableSpace.measurableSet_empty _
  | compl t _ ht => exact ht.compl
  | iUnion t _ ht => exact .iUnion ht

Premises used: MeasurableSet.empty, Compl.compl, MeasurableSpace.measurableSet_empty, Set.iUnion
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t : Set α
t_mem : t ∈ 𝒜
⊢ t ∈ generateSetAlgebra ℬ

Tactic:
self_subset_generateSetAlgebra (h t_mem)

Premises used: MeasureTheory.self_subset_generateSetAlgebra
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t : Set α
t_mem : t ∈ 𝒜
⊢ t ∈ generateSetAlgebra ℬ

Tactic:
exact self_subset_generateSetAlgebra (h t_mem)

Premises used: MeasureTheory.self_subset_generateSetAlgebra
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
⊢ ∅ ∈ generateSetAlgebra ℬ

Tactic:
isSetAlgebra_generateSetAlgebra.empty_mem

Premises used: MeasureTheory.isSetAlgebra_generateSetAlgebra, MeasureTheory.IsSetAlgebra.empty_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
⊢ ∅ ∈ generateSetAlgebra ℬ

Tactic:
exact isSetAlgebra_generateSetAlgebra.empty_mem

Premises used: MeasureTheory.isSetAlgebra_generateSetAlgebra, MeasureTheory.IsSetAlgebra.empty_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t : Set α
hs : generateSetAlgebra 𝒜 t
t_mem : t ∈ generateSetAlgebra ℬ
⊢ tᶜ ∈ generateSetAlgebra ℬ

Tactic:
isSetAlgebra_generateSetAlgebra.compl_mem t_mem

Premises used: MeasureTheory.IsSetAlgebra.compl_mem, MeasureTheory.isSetAlgebra_generateSetAlgebra
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t : Set α
hs : generateSetAlgebra 𝒜 t
t_mem : t ∈ generateSetAlgebra ℬ
⊢ tᶜ ∈ generateSetAlgebra ℬ

Tactic:
exact isSetAlgebra_generateSetAlgebra.compl_mem t_mem

Premises used: MeasureTheory.IsSetAlgebra.compl_mem, MeasureTheory.isSetAlgebra_generateSetAlgebra
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t u : Set α
hs : generateSetAlgebra 𝒜 t
ht : generateSetAlgebra 𝒜 u
t_mem : t ∈ generateSetAlgebra ℬ
u_mem : u ∈ generateSetAlgebra ℬ
⊢ t ∪ u ∈ generateSetAlgebra ℬ

Tactic:
isSetAlgebra_generateSetAlgebra.union_mem t_mem u_mem

Premises used: MeasureTheory.isSetAlgebra_generateSetAlgebra, MeasureTheory.IsSetAlgebra.union_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t u : Set α
hs : generateSetAlgebra 𝒜 t
ht : generateSetAlgebra 𝒜 u
t_mem : t ∈ generateSetAlgebra ℬ
u_mem : u ∈ generateSetAlgebra ℬ
⊢ t ∪ u ∈ generateSetAlgebra ℬ

Tactic:
exact isSetAlgebra_generateSetAlgebra.union_mem t_mem u_mem

Premises used: MeasureTheory.isSetAlgebra_generateSetAlgebra, MeasureTheory.IsSetAlgebra.union_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
base : ∀ (t : Set α) (t_mem : t ∈ 𝒜), t ∈ generateSetAlgebra ℬ
empty : ∅ ∈ generateSetAlgebra ℬ
compl : ∀ (t : Set α), generateSetAlgebra 𝒜 t → ∀ (t_mem : t ∈ generateSetAlgebra ℬ), tᶜ ∈ generateSetAlgebra ℬ
union :
  ∀ (t u : Set α),
    generateSetAlgebra 𝒜 t →
      generateSetAlgebra 𝒜 u →
        ∀ (t_mem : t ∈ generateSetAlgebra ℬ) (u_mem : u ∈ generateSetAlgebra ℬ), t ∪ u ∈ generateSetAlgebra ℬ
⊢ s ∈ generateSetAlgebra ℬ

Tactic:
induction hs with
  | base t t_mem => exact self_subset_generateSetAlgebra (h t_mem)
  | empty => exact isSetAlgebra_generateSetAlgebra.empty_mem
  | compl t _ t_mem => exact isSetAlgebra_generateSetAlgebra.compl_mem t_mem
  | union t u _ _ t_mem u_mem => exact isSetAlgebra_generateSetAlgebra.union_mem t_mem u_mem

Premises used: Compl.compl, MeasureTheory.isSetAlgebra_generateSetAlgebra, MeasureTheory.IsSetAlgebra.empty_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t : Set α
t_mem : t ∈ 𝒜
⊢ t ∈ ℬ

Tactic:
h t_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t : Set α
t_mem : t ∈ 𝒜
⊢ t ∈ ℬ

Tactic:
exact h t_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
⊢ ∅ ∈ ℬ

Tactic:
hℬ.empty_mem

Premises used: MeasureTheory.IsSetAlgebra.empty_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
⊢ ∅ ∈ ℬ

Tactic:
exact hℬ.empty_mem

Premises used: MeasureTheory.IsSetAlgebra.empty_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t : Set α
hs : generateSetAlgebra 𝒜 t
t_mem : t ∈ ℬ
⊢ tᶜ ∈ ℬ

Tactic:
hℬ.compl_mem t_mem

Premises used: MeasureTheory.IsSetAlgebra.compl_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t : Set α
hs : generateSetAlgebra 𝒜 t
t_mem : t ∈ ℬ
⊢ tᶜ ∈ ℬ

Tactic:
exact hℬ.compl_mem t_mem

Premises used: MeasureTheory.IsSetAlgebra.compl_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t u : Set α
hs : generateSetAlgebra 𝒜 t
ht : generateSetAlgebra 𝒜 u
t_mem : t ∈ ℬ
u_mem : u ∈ ℬ
⊢ t ∪ u ∈ ℬ

Tactic:
hℬ.union_mem t_mem u_mem

Premises used: MeasureTheory.IsSetAlgebra.union_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t u : Set α
hs : generateSetAlgebra 𝒜 t
ht : generateSetAlgebra 𝒜 u
t_mem : t ∈ ℬ
u_mem : u ∈ ℬ
⊢ t ∪ u ∈ ℬ

Tactic:
exact hℬ.union_mem t_mem u_mem

Premises used: MeasureTheory.IsSetAlgebra.union_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
base : ∀ (t : Set α) (t_mem : t ∈ 𝒜), t ∈ ℬ
empty : ∅ ∈ ℬ
compl : ∀ (t : Set α), generateSetAlgebra 𝒜 t → ∀ (t_mem : t ∈ ℬ), tᶜ ∈ ℬ
union : ∀ (t u : Set α), generateSetAlgebra 𝒜 t → generateSetAlgebra 𝒜 u → ∀ (t_mem : t ∈ ℬ) (u_mem : u ∈ ℬ), t ∪ u ∈ ℬ
⊢ s ∈ ℬ

Tactic:
induction hs with
  | base t t_mem => exact h t_mem
  | empty => exact hℬ.empty_mem
  | compl t _ t_mem => exact hℬ.compl_mem t_mem
  | union t u _ _ t_mem u_mem => exact hℬ.union_mem t_mem u_mem

Premises used: Compl.compl, MeasureTheory.IsSetAlgebra.empty_mem
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h𝒜 : IsSetAlgebra 𝒜
⊢ generateSetAlgebra 𝒜 ⊆ 𝒜

Tactic:
h𝒜.generateSetAlgebra_subset subset_rfl

Premises used: MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset, subset_rfl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
h𝒜 : IsSetAlgebra 𝒜
⊢ generateSetAlgebra 𝒜 = 𝒜

Tactic:
Subset.antisymm h𝒜.generateSetAlgebra_subset_self self_subset_generateSetAlgebra

Premises used: Set.Subset.antisymm, MeasureTheory.self_subset_generateSetAlgebra, MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset_self
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
⊢ u = ⋃ (a : Set (Set α)), ⋃ (_ : Membership.mem (γ := Set (Set (Set α))) {{u}} a), ⋂ t ∈ a, t

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
base :
  ∀ (a : Set (Set α)) (ha : Membership.mem (γ := Set (Set (Set α))) {{u}} a) (t : Set α) (ht : t ∈ a), t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
refine ⟨{{u}}, finite_singleton {u},
      fun a ha ↦ eq_of_mem_singleton ha ▸ finite_singleton u,
      fun a ha t ht ↦ ?_, by simp⟩
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
a : Set (Set α)
ha : Membership.mem (γ := Set (Set (Set α))) {{u}} a
t : Set α
ht : t ∈ a
base :
  ∀ (u_mem : u ∈ 𝒜) (a : Set (Set α)) (ha : Membership.mem (γ := Set (Set (Set α))) {{u}} {u}) (t : Set α)
    (ht : Membership.mem (γ := Set (Set α)) {u} u), u ∈ 𝒜 ∨ uᶜ ∈ 𝒜
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
rw [eq_of_mem_singleton ha, ha, eq_of_mem_singleton ht, ht] at *

Premises used: Set.eq_of_mem_singleton
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
a : Set (Set α)
ha : Membership.mem (γ := Set (Set (Set α))) {{u}} {u}
t : Set α
ht : Membership.mem (γ := Set (Set α)) {u} u
⊢ u ∈ 𝒜 ∨ uᶜ ∈ 𝒜

Tactic:
Or.inl u_mem

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
a : Set (Set α)
ha : Membership.mem (γ := Set (Set (Set α))) {{u}} {u}
t : Set α
ht : Membership.mem (γ := Set (Set α)) {u} u
⊢ u ∈ 𝒜 ∨ uᶜ ∈ 𝒜

Tactic:
exact Or.inl u_mem

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
⊢ Eq.{u_1 + 1} (α := Set α) ∅ (⋃ (a : Set (Set α)), ⋃ (_ : Membership.mem (γ := Set (Set (Set α))) ∅ a), ⋂ t ∈ a, t)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SetAlgebra
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧
      (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ Eq.{u_1 + 1} (α := Set α) ∅ (⋃ a ∈ A, ⋂ t ∈ a, t)

Tactic:
exact ⟨∅, finite_empty, fun _ h ↦ (notMem_empty _ h).elim,
    fun _ ha _ _ ↦ (notMem_empty _ ha).elim, by simp⟩