awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ \ s₂)ᶜ
have simp : d.Has (s₁ᶜ ∪ s₂)
Tactic: simp only [diff_eq, compl_inter, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
C : Set (Set α)
s : Set α
⊢ GenerateHas C sᶜ ↔ GenerateHas C s
have refine : GenerateHas C sᶜ → GenerateHas C s
Tactic: refine ⟨?_, GenerateHas.compl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ GenerateHas C s
have h₁ : s = sᶜᶜ
Tactic: convert! GenerateHas.compl h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)
f : ℕ → Set α
hf : ∀ (i : ℕ), d.Has (f i)
⊢ d.Has (⋃ (i : ℕ), f i)
have rw : d.Has (⋃ (i : ℕ), disjointed f i)
Tactic: rw [← iUnion_disjointed]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
x : α
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
have pos : ∀ (h : x ∈ s), x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
x : α
pos : ∀ (h : x ∈ s), x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
have neg : ∀ (h : x ∉ s), x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
⊢ d.Has (tᶜ ∩ s)
have this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
Tactic: have : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ := Set.ext fun x => by by_cases h : x ∈ s <;> simp [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
⊢ d.Has (tᶜ ∩ s)
have simp_rw : d.Has ((t ∩ s)ᶜ \ sᶜ)
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ d.Has ((⋃ (i : ℕ), f i) ∩ s)
have rw : d.Has (⋃ (i : ℕ), f i ∩ s)
Tactic: rw [iUnion_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ d.Has (⋃ (i : ℕ), f i ∩ s)
have refine : Pairwise (α := ℕ) (Function.onFun.{1, u_3 + 1, 1} (β := Set α) Disjoint fun (i : ℕ) ↦ f i ∩ s)
Tactic: refine d.has_iUnion_nat ?_ hf
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s
have rw : MeasurableSet = DynkinSystem.GenerateHas s
Tactic: rw [h_eq, DynkinSystem.generateFrom_eq h_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
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) ⋯
⊢ ∀ (t : Set α) (ht : MeasurableSet t), C t ht
have eq : MeasurableSet = DynkinSystem.GenerateHas s
Tactic: have eq : MeasurableSet = DynkinSystem.GenerateHas s := by
    rw [h_eq, DynkinSystem.generateFrom_eq h_inter]
    rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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 : MeasurableSet t), C t ht
have suffices : ∀ (t : Set α) (ht : DynkinSystem.GenerateHas s t), C t sorry
Tactic: suffices ∀ t (ht : DynkinSystem.GenerateHas s t), C t (eq ▸ ht) from
    fun t ht ↦ this t (eq ▸ ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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 ∅ ⋯
⊢ C t ⋯
have compl₁ : ∀ {u : Set α} (hu : DynkinSystem.GenerateHas s u) (ihu : C u sorry), C uᶜ sorry
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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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ᶜ ⋯
⊢ C t ⋯
have iUnion₁ : ∀ {f : ℕ → Set α} (hfd : Pairwise (Disjoint on f)) (hf : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i))
  (ihf : ∀ (i : ℕ), C (f i) sorry), C (⋃ (i : ℕ), f i) sorry
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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
⊢ ⋂ i ∈ S, s i ∈ 𝒜
have pos : ∀ (h : S = ∅), ⋂ i ∈ S, s i ∈ 𝒜
Tactic: by_cases! h : S = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
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 ∈ 𝒜
⊢ ⋂ i ∈ S, s i ∈ 𝒜
have neg : ∀ (h : S.Nonempty), ⋂ i ∈ S, s i ∈ 𝒜
Tactic: by_cases! h : S = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ ⋂ i ∈ S, s i ∈ 𝒜
have pos : univ ∈ 𝒜
Tactic: rw [h, ← Finset.set_biInter_coe, Finset.coe_empty, biInter_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
⊢ generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜
have refine : ∀ (s : Set α) (ms : MeasurableSet s), MeasurableSet s
Tactic: refine le_antisymm (fun s ms ↦ ?_) (generateFrom_mono self_subset_generateSetAlgebra)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht : t ∈ generateSetAlgebra 𝒜
⊢ MeasurableSet t
have hC : ∀ (u : Set α) (u_mem : u ∈ 𝒜), MeasurableSet u
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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht : t ∈ generateSetAlgebra 𝒜
hC : ∀ (u : Set α) (u_mem : u ∈ 𝒜), MeasurableSet u
⊢ MeasurableSet t
have hC₁ : MeasurableSet.{u_1} (α := α) ∅
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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht : t ∈ generateSetAlgebra 𝒜
hC : ∀ (u : Set α) (u_mem : u ∈ 𝒜), MeasurableSet u
hC₁ : MeasurableSet.{u_1} (α := α) ∅
⊢ MeasurableSet t
have hC₂ : ∀ (u : Set α), generateSetAlgebra 𝒜 u → ∀ (mu : MeasurableSet u), MeasurableSet uᶜ
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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
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ᶜ
⊢ MeasurableSet t
have hC₃ : ∀ (u v : Set α),
  generateSetAlgebra 𝒜 u →
    generateSetAlgebra 𝒜 v → ∀ (mu : MeasurableSet u) (mv : MeasurableSet v), MeasurableSet (u ∪ v)
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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
ms : MeasurableSet s
⊢ MeasurableSet s
have hC : ∀ (t : Set α) (ht : t ∈ generateSetAlgebra 𝒜) (h : MeasurableSet t), MeasurableSet t
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
Cleared hypotheses: ms
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
ms : MeasurableSet s
hC : ∀ (t : Set α) (ht : t ∈ generateSetAlgebra 𝒜) (h : MeasurableSet t), MeasurableSet t
⊢ MeasurableSet s
have empty : MeasurableSet.{u_1} (α := α) ∅
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
Cleared hypotheses: ms
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
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} (α := α) ∅
⊢ MeasurableSet s
have compl : ∀ (t : Set α), MeasurableSet t → ∀ (ht : MeasurableSet t), MeasurableSet tᶜ
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
Cleared hypotheses: ms
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
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ᶜ
⊢ MeasurableSet s
have iUnion : ∀ (t : ℕ → Set α),
  (∀ (n : ℕ), MeasurableSet (t n)) →
    ∀ (ht : ∀ (n : ℕ), MeasurableSet (t n)), MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), t i)
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
Cleared hypotheses: ms
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ generateSetAlgebra ℬ
have base : ∀ (t : Set α) (t_mem : t ∈ 𝒜), t ∈ 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
base : ∀ (t : Set α) (t_mem : t ∈ 𝒜), t ∈ generateSetAlgebra ℬ
⊢ s ∈ generateSetAlgebra ℬ
have empty : ∅ ∈ 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
base : ∀ (t : Set α) (t_mem : t ∈ 𝒜), t ∈ generateSetAlgebra ℬ
empty : ∅ ∈ generateSetAlgebra ℬ
⊢ s ∈ generateSetAlgebra ℬ
have compl : ∀ (t : Set α), generateSetAlgebra 𝒜 t → ∀ (t_mem : t ∈ generateSetAlgebra ℬ), tᶜ ∈ 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
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 ℬ
⊢ s ∈ generateSetAlgebra ℬ
have union : ∀ (t u : Set α),
  generateSetAlgebra 𝒜 t →
    generateSetAlgebra 𝒜 u →
      ∀ (t_mem : t ∈ generateSetAlgebra ℬ) (u_mem : u ∈ generateSetAlgebra ℬ), t ∪ u ∈ 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ ℬ
have base : ∀ (t : Set α) (t_mem : t ∈ 𝒜), t ∈ ℬ
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
base : ∀ (t : Set α) (t_mem : t ∈ 𝒜), t ∈ ℬ
⊢ s ∈ ℬ
have empty : ∅ ∈ ℬ
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
base : ∀ (t : Set α) (t_mem : t ∈ 𝒜), t ∈ ℬ
empty : ∅ ∈ ℬ
⊢ s ∈ ℬ
have compl : ∀ (t : Set α), generateSetAlgebra 𝒜 t → ∀ (t_mem : t ∈ ℬ), tᶜ ∈ ℬ
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
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ᶜ ∈ ℬ
⊢ s ∈ ℬ
have union : ∀ (t u : Set α), generateSetAlgebra 𝒜 t → generateSetAlgebra 𝒜 u → ∀ (t_mem : t ∈ ℬ) (u_mem : u ∈ ℬ), t ∪ u ∈ ℬ
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t
have base : ∀ (a : Set (Set α)) (ha : Membership.mem (γ := Set (Set (Set α))) {{u}} a) (t : Set α) (ht : t ∈ a), t ∈ 𝒜 ∨ 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
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
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
have 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ᶜ ∈ 𝒜
Tactic: rw [eq_of_mem_singleton ha, ha, eq_of_mem_singleton ht, ht] at *
Cleared hypotheses: u_mem, a, ha, t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
u_ind :
  ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t
have compl : ∀ (A : Set (Set (Set α))) (A_fin : A.Finite) (mem_A : ∀ a ∈ A, a.Finite) (hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜)
  (u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t),
  ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t
Tactic: rcases u_ind with ⟨A, A_fin, mem_A, hA, u_eq⟩
Cleared hypotheses: u_ind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (hypothesis)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t
have this : Finite.{u_1 + 1} (↑A : Type u_1)
Tactic: have := finite_coe_iff.2 A_fin
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (hypothesis)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this : Finite.{u_1 + 1} (↑A : Type u_1)
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t
have this₁ : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
Tactic: have := fun a : A ↦ finite_coe_iff.2 <| mem_A a.1 a.2
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t
have compl : ∀ (a : Set (Set α))
  (ha :
    Membership.mem (γ := Set (Set (Set α)))
      {x : Set (Set α) |
        ∃ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
          {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} = x}
      a)
  (t : Set α) (ht : t ∈ a), t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
Tactic: refine ⟨{{(f a).1ᶜ | a : A} | f : (Π a : A, ↑a)}, finite_coe_iff.1 inferInstance,
      fun a ⟨f, hf⟩ ↦ hf ▸ finite_coe_iff.1 inferInstance, fun a ha t ht ↦ ?_, ?_⟩