awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
inst : CountablyGenerated α
rw : generateFrom (⋃ (n : ℕ), memPartition (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅) n) = m
⊢ generateFrom (⋃ (n : ℕ), countablePartition α n) = m
have rw₁ : generateFrom (range (enumerateCountable (s := countableGeneratingSet α) sorry ∅)) = m
Tactic: rw [countablePartition, generateFrom_iUnion_memPartition,
    range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
inst : CountablyGenerated α
rw : generateFrom (⋃ (n : ℕ), memPartition (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅) n) = m
rw₁ : generateFrom (range (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅)) = m
⊢ generateFrom (⋃ (n : ℕ), countablePartition α n) = m
have rw₂ : generateFrom (countableGeneratingSet α) = m
Tactic: rw [countablePartition, generateFrom_iUnion_memPartition,
    range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
inst : CountablyGenerated α
rw : generateFrom (⋃ (n : ℕ), memPartition (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅) n) = m
rw₁ : generateFrom (range (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅)) = m
rw₂ : generateFrom (countableGeneratingSet α) = m
⊢ generateFrom (⋃ (n : ℕ), countablePartition α n) = m
have rw₃ : m = m
Tactic: rw [countablePartition, generateFrom_iUnion_memPartition,
    range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hα : CountableOrCountablyGenerated α γ
hβ : CountableOrCountablyGenerated β γ
⊢ CountableOrCountablyGenerated (α × β) γ
have inl : ∀ (hα : Countable α), CountableOrCountablyGenerated (α × β) γ
Tactic: rcases hα with (hα | hα)
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hα : CountableOrCountablyGenerated α γ
hβ : CountableOrCountablyGenerated β γ
inl : ∀ (hα : Countable α), CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated (α × β) γ
have inr : ∀ (hα : CountablyGenerated γ), CountableOrCountablyGenerated (α × β) γ
Tactic: rcases hα with (hα | hα)
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : Countable α
⊢ CountableOrCountablyGenerated (α × β) γ
have inl : ∀ (hβ : Countable β), CountableOrCountablyGenerated (α × β) γ
Tactic: rcases hβ with (hβ | hβ)
Cleared hypotheses: hβ
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : Countable α
inl : ∀ (hβ : Countable β), CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated (α × β) γ
have inl₁ : ∀ (hβ : CountablyGenerated γ), CountableOrCountablyGenerated (α × β) γ
Tactic: rcases hβ with (hβ | hβ)
Cleared hypotheses: hβ
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ
have inr : ∀ (hβ : Countable β), CountableOrCountablyGenerated (α × β) γ
Tactic: rcases hβ with (hβ | hβ)
Cleared hypotheses: hβ
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : CountablyGenerated γ
inr : ∀ (hβ : Countable β), CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated (α × β) γ
have inr₁ : ∀ (hβ : CountablyGenerated γ), CountableOrCountablyGenerated (α × β) γ
Tactic: rcases hβ with (hβ | hβ)
Cleared hypotheses: hβ
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty β
h : CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated α γ
have inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated α γ
Tactic: rcases h.countableOrCountablyGenerated with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty β
h : CountableOrCountablyGenerated (α × β) γ
inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated α γ
⊢ CountableOrCountablyGenerated α γ
have inr : ∀ (h : CountablyGenerated γ), CountableOrCountablyGenerated α γ
Tactic: rcases h.countableOrCountablyGenerated with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty β
h_1 : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated α γ
have this : Countable α
Tactic: have := countable_left_of_prod_of_nonempty h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty α
h : CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated β γ
have inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated β γ
Tactic: rcases h.countableOrCountablyGenerated with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty α
h : CountableOrCountablyGenerated (α × β) γ
inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated β γ
⊢ CountableOrCountablyGenerated β γ
have inr : ∀ (h : CountablyGenerated γ), CountableOrCountablyGenerated β γ
Tactic: rcases h.countableOrCountablyGenerated with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty α
h_1 : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated β γ
have this : Countable β
Tactic: have := countable_right_of_prod_of_nonempty h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
h : CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated (β × α) γ
have inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated (β × α) γ
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
h : CountableOrCountablyGenerated (α × β) γ
inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated (β × α) γ
⊢ CountableOrCountablyGenerated (β × α) γ
have inr : ∀ (h : CountablyGenerated γ), CountableOrCountablyGenerated (β × α) γ
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
have inl : IsEmpty ι → MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
inl : IsEmpty ι → MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
have inr : Nonempty ι → MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h_1 : Nonempty ι
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
have inr : ∀ (e : ℕ → ι) (he : Surjective e), MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
Tactic: rcases exists_surjective_nat ι with ⟨e, he⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h_1 : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
have inr : MeasurableSet.{u_1} (α := α) (⋃ (x : ℕ), f (e x))
Tactic: rw [← iUnion_congr_of_surjective _ he (fun _ => rfl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ b ∈ s, f b)
have rw : MeasurableSet.{u_1} (α := α) (⋃ (x : (↑s : Type u_2)), f (↑x : β))
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (x : (↑s : Type u_2)), f (↑x : β))
have this : Countable.{u_2 + 1} (↑s : Type u_2)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃₀ s)
have rw : MeasurableSet.{u_1} (α := α) (⋃ i ∈ s, i)
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (b : ι), f b)ᶜ
have rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (f i)ᶜ)
Tactic: rw [compl_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋂ b ∈ s, f b)ᶜ
have rw : MeasurableSet.{u_1} (α := α) (⋃ i ∈ s, (f i)ᶜ)
Tactic: rw [compl_iInter₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂₀ s)
have rw : MeasurableSet.{u_1} (α := α) (⋂ i ∈ s, i)
Tactic: rw [sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∪ s₂)
have rw : MeasurableSet.{u_1} (α := α) (⋃ (b : Bool), bif b then s₁ else s₂)
Tactic: rw [union_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)
have rw : MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ
Tactic: rw [inter_eq_compl_compl_union_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ⇨ s₂)
have rw : MeasurableSet (s₂ ⊔ s₁ᶜ)
Tactic: rw [himp_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
i : Bool
⊢ MeasurableSet (bif i then s₁ else s₂)
have false : MeasurableSet (bif false then s₁ else s₂)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
i : Bool
false : MeasurableSet (bif Bool.false then s₁ else s₂)
⊢ MeasurableSet (bif i then s₁ else s₂)
have true : MeasurableSet (bif true then s₁ else s₂)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : Prop
⊢ MeasurableSet.{u_1} (α := α) {_a : α | p}
have pos : p → MeasurableSet.{u_1} (α := α) {_a : α | p}
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : Prop
pos : p → MeasurableSet.{u_1} (α := α) {_a : α | p}
⊢ MeasurableSet.{u_1} (α := α) {_a : α | p}
have neg : ¬p → MeasurableSet.{u_1} (α := α) {_a : α | p}
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
⊢ MeasurableSet.{u_1} (α := α) {x : α | p x → q x}
have h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x → q x} ({x : α | p x}ᶜ ∪ {x : α | q x})
Tactic: have h_eq : {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x} := by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x → q x} ({x : α | p x}ᶜ ∪ {x : α | q x})
⊢ MeasurableSet.{u_1} (α := α) {x : α | p x → q x}
have rw : MeasurableSet.{u_1} (α := α) ({x : α | p x}ᶜ ∪ {x : α | q x})
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | p x ↔ q x} ({x : α | p x → q x} ∩ {x : α | q x → p x})
have h : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | p x ↔ q x} x ↔
    Membership.mem (γ := Set α) ({x : α | p x → q x} ∩ {x : α | q x → p x}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
⊢ MeasurableSet.{u_1} (α := α) {x : α | p x ↔ q x}
have h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x ↔ q x} ({x : α | p x → q x} ∩ {x : α | q x → p x})
Tactic: have h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x} := by ext; simp; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x ↔ q x} ({x : α | p x → q x} ∩ {x : α | q x → p x})
⊢ MeasurableSet.{u_1} (α := α) {x : α | p x ↔ q x}
have rw : MeasurableSet.{u_1} (α := α) ({x : α | p x → q x} ∩ {x : α | q x → p x})
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet s
have rw : MeasurableSet.{u_1} (α := α) (⋃ x ∈ s, {x})
Tactic: rw [← biUnion_of_singleton s]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s : Set α
hs : MeasurableSet s
⊢ p s hs
have basic : ∀ (u : Set α) (a : u ∈ C), p u sorry
Tactic: induction hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s : Set α
hs : MeasurableSet s
basic : ∀ (u : Set α) (a : u ∈ C), p u ⋯
empty₁ : p ∅ ⋯
⊢ p s hs
have compl₁ : ∀ (t : Set α) (a : GenerateMeasurable C t), p t a → p tᶜ sorry
Tactic: induction hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s : Set α
hs : MeasurableSet s
basic : ∀ (u : Set α) (a : u ∈ C), p u ⋯
empty₁ : p ∅ ⋯
compl₁ : ∀ (t : Set α) (a : GenerateMeasurable C t), p t a → p tᶜ ⋯
⊢ p s hs
have iUnion₁ : ∀ (f : ℕ → Set α) (a : ∀ (n : ℕ), GenerateMeasurable C (f n)), (∀ (n : ℕ), p (f n) sorry) → p (⋃ (i : ℕ), f i) sorry
Tactic: induction hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ s ∈ S, x ∈ s ↔ y ∈ s
have refine : ∀ (H : ∀ s ∈ S, x ∈ s ↔ y ∈ s) (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
Tactic: refine ⟨fun H s hs ↦ H s (.basic s hs), fun H s ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)
have hC : ∀ t ∈ S, ∀ (ht : MeasurableSet t), x ∈ t ↔ y ∈ t
Tactic: apply generateFrom_induction
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
hC : ∀ t ∈ S, ∀ (ht : MeasurableSet t), x ∈ t ↔ y ∈ t
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)
have empty : Membership.mem (γ := Set α) ∅ x ↔ Membership.mem (γ := Set α) ∅ y
Tactic: apply generateFrom_induction
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
hC : ∀ t ∈ S, ∀ (ht : MeasurableSet t), x ∈ t ↔ y ∈ t
empty : Membership.mem (γ := Set α) ∅ x ↔ Membership.mem (γ := Set α) ∅ y
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)
have compl : ∀ (t : Set α) (ht : MeasurableSet t), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)
Tactic: apply generateFrom_induction
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
hC : ∀ t ∈ S, ∀ (ht : MeasurableSet t), x ∈ t ↔ y ∈ t
empty : Membership.mem (γ := Set α) ∅ x ↔ Membership.mem (γ := Set α) ∅ y
compl : ∀ (t : Set α) (ht : MeasurableSet t), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)
have iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)),
  (∀ (n : ℕ), x ∈ s n ↔ y ∈ s n) →
    (Membership.mem (γ := Set α) (⋃ (i : ℕ), s i) x ↔ Membership.mem (γ := Set α) (⋃ (i : ℕ), s i) y)
Tactic: apply generateFrom_induction
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
⊢ generateFrom (insert univ S) = generateFrom S
have rw : generateFrom ({univ} ∪ S) = generateFrom S
Tactic: rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_univ, bot_sup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : generateFrom ({univ} ∪ S) = generateFrom S
⊢ generateFrom (insert univ S) = generateFrom S
have rw₁ : generateFrom {univ} ⊔ generateFrom S = generateFrom S
Tactic: rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_univ, bot_sup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : generateFrom ({univ} ∪ S) = generateFrom S
rw₁ : generateFrom {univ} ⊔ generateFrom S = generateFrom S
⊢ generateFrom (insert univ S) = generateFrom S
have rw₂ : ⊥ ⊔ generateFrom S = generateFrom S
Tactic: rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_univ, bot_sup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : generateFrom ({univ} ∪ S) = generateFrom S
rw₁ : generateFrom {univ} ⊔ generateFrom S = generateFrom S
rw₂ : ⊥ ⊔ generateFrom S = generateFrom S
⊢ generateFrom (insert univ S) = generateFrom S
have rw₃ : generateFrom S = generateFrom S
Tactic: rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_univ, bot_sup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
⊢ generateFrom (insert ∅ S) = generateFrom S
have rw : generateFrom ({∅} ∪ S) = generateFrom S
Tactic: rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : generateFrom ({∅} ∪ S) = generateFrom S
⊢ generateFrom (insert ∅ S) = generateFrom S
have rw₁ : generateFrom {∅} ⊔ generateFrom S = generateFrom S
Tactic: rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : generateFrom ({∅} ∪ S) = generateFrom S
rw₁ : generateFrom {∅} ⊔ generateFrom S = generateFrom S
⊢ generateFrom (insert ∅ S) = generateFrom S
have rw₂ : ⊥ ⊔ generateFrom S = generateFrom S
Tactic: rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : generateFrom ({∅} ∪ S) = generateFrom S
rw₁ : generateFrom {∅} ⊔ generateFrom S = generateFrom S
rw₂ : ⊥ ⊔ generateFrom S = generateFrom S
⊢ generateFrom (insert ∅ S) = generateFrom S
have rw₃ : generateFrom S = generateFrom S
Tactic: rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
have rw : MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
Tactic: rw [iInf, measurableSet_sInf, forall_mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
rw : MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
⊢ MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
have rw₁ : (∀ m_1 ∈ range m, MeasurableSet s) ↔ ∀ (i : ι), MeasurableSet s
Tactic: rw [iInf, measurableSet_sInf, forall_mem_range]