awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
x : Sigma κ
⊢ Measurable (β := X (x.fst (β := κ)) (x.snd (β := κ))) fun (c : (x : ι) → (y : κ x) → X x y) ↦
    Sigma.uncurry (β := κ) (γ := X) c x
have simp : Measurable (β := X (x.fst (β := κ)) (x.snd (β := κ))) fun (c : (x : ι) → (y : κ x) → X x y) ↦
  c (x.fst (β := κ)) (x.snd (β := κ))
Tactic: simp only [Sigma.uncurry]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst : MeasurableSpace α
inst_1 : MeasurableEq α
⊢ MeasurableSingletonClass α
have measurableSet_singleton : ∀ (x : α), MeasurableSet (α := α) {x}
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst : MeasurableSpace α
inst_1 : MeasurableEq α
⊢ ∀ (x : α), MeasurableSet (α := α) {x}
have measurableSet_singleton : ∀ (x : α), Measurable (β := Prop) fun (n : α) ↦ n = x
Tactic: simp_rw [← setOf_eq_eq_singleton, measurableSet_setOf]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : Countable α
⊢ MeasurableEq α
have measurableSet_diagonal : MeasurableSet (diagonal α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : Countable α
⊢ MeasurableSet (diagonal α)
have measurableSet_diagonal : MeasurableSet.{u_1} (α := α × α) (⋃ (i : α), {(i, i)})
Tactic: simp_rw [← Set.range_diag, Set.range_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
s : Set α
hs : s ∈ countableGeneratingSet α
⊢ MeasurableSet s
have rw : MeasurableSet s
Tactic: rw [← generateFrom_countableGeneratingSet (α := α)]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_3
m : MeasurableSpace α
inst : CountablyGenerated α
⊢ generateFrom (range (natGeneratingSequence α)) = m
have rw : generateFrom (range (enumerateCountable (s := countableGeneratingSet α) sorry ∅)) = m
Tactic: rw [natGeneratingSequence, 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 (range (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅)) = m
⊢ generateFrom (range (natGeneratingSequence α)) = m
have rw₁ : generateFrom (countableGeneratingSet α) = m
Tactic: rw [natGeneratingSequence, 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 (range (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅)) = m
rw₁ : generateFrom (countableGeneratingSet α) = m
⊢ generateFrom (range (natGeneratingSequence α)) = m
have rw₂ : m = m
Tactic: rw [natGeneratingSequence, range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
h : CountablyGenerated β
f : α → β
⊢ CountablyGenerated α
have rcases : ∀ (b : Set (Set β)) (hbc : b.Countable), CountablyGenerated α
Tactic: rcases h with ⟨⟨b, hbc, rfl⟩⟩
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
⊢ CountablyGenerated α
have rw : CountablyGenerated α
Tactic: rw [comap_generateFrom]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
β : Type u_2
m₁ m₂ : MeasurableSpace β
h₁ : CountablyGenerated β
h₂ : CountablyGenerated β
⊢ CountablyGenerated β
have rcases : ∀ (b₁ : Set (Set β)) (hb₁c : b₁.Countable), CountablyGenerated β
Tactic: rcases h₁ with ⟨⟨b₁, hb₁c, rfl⟩⟩
Cleared hypotheses: m₁, h₁
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
β : Type u_2
m₂ : MeasurableSpace β
h₂ : CountablyGenerated β
b₁ : Set (Set β)
hb₁c : b₁.Countable
⊢ CountablyGenerated β
have rcases : ∀ (b₂ : Set (Set β)) (hb₂c : b₂.Countable), CountablyGenerated β
Tactic: rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩
Cleared hypotheses: m₂, h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
⊢ ∃ (b : Set (Set α)), b.Countable ∧ inst = generateFrom b
have refine : inst = generateFrom (⋃ (y : α), {measurableAtom y})
Tactic: refine ⟨⋃ y, {measurableAtom y}, countable_iUnion (fun i ↦ countable_singleton _), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
⊢ inst = generateFrom (⋃ (y : α), {measurableAtom y})
have refine : inst ≤ generateFrom (⋃ (y : α), {measurableAtom y})
Tactic: refine le_antisymm ?_ (generateFrom_le (by simp [MeasurableSet.measurableAtom_of_countable]))
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
⊢ s = ⋃ y ∈ s, measurableAtom y
have h₁ : s ⊆ ⋃ y ∈ s, measurableAtom y
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
h₁ : s ⊆ ⋃ y ∈ s, measurableAtom y
⊢ s = ⋃ y ∈ s, measurableAtom y
have h₂ : ⋃ y ∈ s, measurableAtom y ⊆ s
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
⊢ ⋃ y ∈ s, measurableAtom y ⊆ s
have h₂ : ∀ (i : α) (i_1 : i ∈ s), measurableAtom i ⊆ s
Tactic: simp only [iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
have this : s = ⋃ y ∈ s, measurableAtom y
Tactic: have : s = ⋃ y ∈ s, measurableAtom y := by
      apply Subset.antisymm
      · intro x hx
        simpa using ⟨x, hx, by simp⟩
      · simp only [iUnion_subset_iff]
        intro x hx
        exact measurableAtom_subset hs hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
this : s = ⋃ y ∈ s, measurableAtom y
⊢ MeasurableSet s
have rw : MeasurableSet.{u_1} (α := α) (⋃ y ∈ s, measurableAtom y)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
this : s = ⋃ y ∈ s, measurableAtom y
⊢ MeasurableSet.{u_1} (α := α) (⋃ y ∈ s, measurableAtom y)
have apply : ∀ (x : α) (_hx : x ∈ s), MeasurableSet (measurableAtom x)
Tactic: apply MeasurableSet.biUnion (to_countable s) (fun x _hx ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
this : s = ⋃ y ∈ s, measurableAtom y
x : α
_hx : x ∈ s
⊢ MeasurableSet (measurableAtom x)
have ht : Membership.mem (γ := Set (Set α)) (⋃ (y : α), {measurableAtom y}) (measurableAtom x)
Tactic: apply measurableSet_generateFrom
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
x y : α
h : x ≠ y
⊢ ∃ (s : Set α), MeasurableSet s ∧ x ∈ s ∧ y ∉ s
have contrapose! : ∀ (h : ∀ (s : Set α) (_ : MeasurableSet s) (_ : x ∈ s), y ∈ s), x = y
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ s ∈ S, x ∈ s ↔ y ∈ s
⊢ x = y
have hxy₁ : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
Tactic: rw [← forall_generateFrom_mem_iff_mem_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
⊢ f a₁ = f a₂
have by_contra! : ∀ (h : f a₁ ≠ f a₂), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
⊢ False
have obtain : ∀ (s : Set β) (hs : MeasurableSet s) (hx : f a₁ ∈ s) (hy : f a₂ ∉ s), False
Tactic: obtain ⟨s, hs, hx, hy⟩ := exists_measurableSet_of_ne h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
⊢ False
have inl : ∀ (h' : f ⁻¹' s = ∅), False
Tactic: obtain h' | h' := MeasurableSpace.measurableSet_bot_iff.mp (hf hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
inl : ∀ (h' : f ⁻¹' s = ∅), False
⊢ False
have inr : ∀ (h' : f ⁻¹' s = univ), False
Tactic: obtain h' | h' := MeasurableSpace.measurableSet_bot_iff.mp (hf hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = ∅
⊢ False
have inl : f a₁ ∉ s
Tactic: absurd hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = univ
⊢ False
have inr : f a₂ ∈ s
Tactic: absurd hy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
⊢ ∃ (c : β), f = fun (x : α) ↦ c
have h : ∀ (a₁ a₂ : α), f a₁ = f a₂
Tactic: have h (a₁ : α) (a₂ : α) : f a₁ = f a₂ := by
    by_contra! h
    obtain ⟨s, hs, hx, hy⟩ := exists_measurableSet_of_ne h
    obtain h' | h' := MeasurableSpace.measurableSet_bot_iff.mp (hf hs)
    · absurd hx
      simp [← mem_preimage, h']
    · absurd hy
      simp [← mem_preimage, h']
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
h : ∀ (a₁ a₂ : α), f a₁ = f a₂
⊢ ∃ (c : β), f = fun (x : α) ↦ c
have inl : ∀ (h' : IsEmpty α), ∃ (c : β), f = fun (x : α) ↦ c
Tactic: obtain h' | h' := isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
h : ∀ (a₁ a₂ : α), f a₁ = f a₂
inl : ∀ (h' : IsEmpty α), ∃ (c : β), f = fun (x : α) ↦ c
⊢ ∃ (c : β), f = fun (x : α) ↦ c
have inr : ∀ (h' : Nonempty α), ∃ (c : β), f = fun (x : α) ↦ c
Tactic: obtain h' | h' := isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
h : ∀ (a₁ a₂ : α), f a₁ = f a₂
h' : IsEmpty α
⊢ ∃ (c : β), f = fun (x : α) ↦ c
have w : β
Tactic: use (Classical.ofNonempty : β), funext (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
h : ∀ (a₁ a₂ : α), f a₁ = f a₂
h' : IsEmpty α
w : β
⊢ ∃ (c : β), f = fun (x : α) ↦ c
have h₁ : f = fun (x : α) ↦ Classical.ofNonempty
Tactic: use (Classical.ofNonempty : β), funext (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
h : ∀ (a₁ a₂ : α), f a₁ = f a₂
h' : Nonempty α
⊢ ∃ (c : β), f = fun (x : α) ↦ c
have w : β
Tactic: use f (Classical.ofNonempty : α), funext (fun x ↦ h _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
h : ∀ (a₁ a₂ : α), f a₁ = f a₂
h' : Nonempty α
w : β
⊢ ∃ (c : β), f = fun (x : α) ↦ c
have h₁ : f = fun (x : α) ↦ f Classical.ofNonempty
Tactic: use f (Classical.ofNonempty : α), funext (fun x ↦ h _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m m' : MeasurableSpace α
hsep : CountablySeparated α
h : m ≤ m'
⊢ CountablySeparated α
have simp_rw : ∀ (hsep : HasCountableSeparatingOn α MeasurableSet univ), HasCountableSeparatingOn α MeasurableSet univ
Tactic: simp_rw [countablySeparated_def] at *
Cleared hypotheses: hsep
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
hsep : HasCountableSeparatingOn α MeasurableSet univ
⊢ HasCountableSeparatingOn α MeasurableSet univ
have rcases : ∀ (S : Set (Set α)) (Sct : S.Countable) (Smeas : ∀ s ∈ S, MeasurableSet s)
  (hS :
    ∀ (x : α),
      Membership.mem (γ := Set α) univ x →
        ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
  HasCountableSeparatingOn α MeasurableSet univ
Tactic: rcases hsep with ⟨S, Sct, Smeas, hS⟩
Cleared hypotheses: hsep
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
S : Set (Set α)
Sct : S.Countable
Smeas : ∀ s ∈ S, MeasurableSet s
hS :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
w : Set (Set α)
left : S.Countable
⊢ HasCountableSeparatingOn α MeasurableSet univ
have left₁ : ∀ s ∈ S, MeasurableSet s
Tactic: use S, Sct, (fun s hs ↦ h _ <| Smeas _ hs), hS
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ CountablySeparated.{u_1} (↑s : Type u_1) ↔ HasCountableSeparatingOn α MeasurableSet s
have rw : HasCountableSeparatingOn.{u_1} (↑s : Type u_1) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s
Tactic: rw [countablySeparated_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : CountablySeparated α
s : Set α
⊢ CountablySeparated.{u_1} (↑s : Type u_1)
have rw : HasCountableSeparatingOn α MeasurableSet s
Tactic: rw [CountablySeparated.subtype_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
⊢ SeparatesPoints α
have refine : ∀ (x y : α) (h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s), x = y
Tactic: refine ⟨fun x y h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
x y : α
h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s
⊢ x = y
have h₁ : Membership.mem (γ := Set α) {x} x → Membership.mem (γ := Set α) {x} y
Tactic: specialize h _ (MeasurableSet.singleton x)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
x y : α
h : Membership.mem (γ := Set α) {x} x → Membership.mem (γ := Set α) {x} y
⊢ x = y
have h₁ : y = x
Tactic: simp_rw [mem_singleton_iff, forall_true_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : SeparatesPoints α
x : α
⊢ MeasurableSet (α := α) {x}
have choose : ∀ (s : (y : α) → (h : x ≠ y) → Set α) (hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h))
  (hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h) (hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h), MeasurableSet (α := α) {x}
Tactic: choose s hsm hxs hys using fun y (h : x ≠ y) ↦ exists_measurableSet_of_ne h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : SeparatesPoints α
x : α
s : (y : α) → (h : x ≠ y) → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
⊢ MeasurableSet (α := α) {x}
have h : Eq (α := Set α) {x} (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1)
Tactic: convert! MeasurableSet.iInter fun y ↦ .iInter fun h ↦ hsm y h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : SeparatesPoints α
x : α
s : (y : α) → (h : x ≠ y) → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
⊢ Eq (α := Set α) {x} (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1)
have h : ∀ (y : α), Membership.mem (γ := Set α) {x} y ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : SeparatesPoints α
x : α
s : (y : α) → (h : x ≠ y) → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
⊢ Membership.mem (γ := Set α) {x} y ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) y
have h : Membership.mem (γ := Set α) {x} x ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) x
Tactic: rcases eq_or_ne x y with rfl | h
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : SeparatesPoints α
x : α
s : (y : α) → (h : x ≠ y) → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
h : Membership.mem (γ := Set α) {x} x ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) x
⊢ Membership.mem (γ := Set α) {x} y ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) y
have h₁ : ∀ (h : x ≠ y), Membership.mem (γ := Set α) {x} y ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) y
Tactic: rcases eq_or_ne x y with rfl | h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : SeparatesPoints α
x : α
s : (y : α) → (h : x ≠ y) → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
h : x ≠ y
⊢ Membership.mem (γ := Set α) {x} y ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) y
have h₁ : ∃ (x_1 : α) (x : x ≠ x_1), y ∉ s x_1 x
Tactic: simp only [mem_singleton_iff, h.symm, false_iff, mem_iInter, not_forall]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : CountablyGenerated α
inst_1 : SeparatesPoints α
⊢ CountablySeparated α
have rcases : ∀ (b : Set (Set α)) (hbc : b.Countable) (hb : inst = generateFrom b), CountablySeparated α
Tactic: rcases h with ⟨b, hbc, hb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst = generateFrom b
⊢ CountablySeparated α
have refine : ∀ (x : α),
  Membership.mem (γ := Set α) univ x → ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
Tactic: refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst = generateFrom b
⊢ ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
have inst : SeparatesPoints α
Tactic: rw [hb] at ‹SeparatesPoints _›
Cleared hypotheses: inst_1, hbc, hb
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
b : Set (Set α)
inst_1 : SeparatesPoints α
hbc : b.Countable
hb : inst = generateFrom b
⊢ ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
have h : ∀ (a : α),
  (Membership.mem (γ := Set α) univ a →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, a ∈ s ↔ y ∈ s) → a = y) ↔
    ∀ (y : α), (∀ s ∈ b, a ∈ s ↔ y ∈ s) → a = y
Tactic: convert! separating_of_generateFrom b
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablySeparated α
⊢ ∃ (m' : MeasurableSpace α), CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m
have rcases : ∀ (b : Set (Set α)) (bct : b.Countable) (hbm : ∀ s ∈ b, MeasurableSet s)
  (hb :
    ∀ (x : α),
      Membership.mem (γ := Set α) univ x →
        ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y),
  ∃ (m' : MeasurableSpace α), CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m
Tactic: rcases h with ⟨b, bct, hbm, hb⟩
Cleared hypotheses: h