awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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 : β
h₁ : f = fun (x : α) ↦ f Classical.ofNonempty
⊢ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
use f (Classical.ofNonempty : α), funext (fun x ↦ h _ _)

Premises used: Classical.ofNonempty, funext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : HasCountableSeparatingOn α MeasurableSet univ
⊢ CountablySeparated α

Tactic:
⟨h⟩

Premises used: MeasurableSpace.CountablySeparated.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : CountablySeparated α
⊢ HasCountableSeparatingOn α MeasurableSet univ

Tactic:
h.countably_separated

Premises used: MeasurableSpace.CountablySeparated.countably_separated
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ CountablySeparated α ↔ HasCountableSeparatingOn α MeasurableSet univ

Tactic:
⟨fun h ↦ h.countably_separated, fun h ↦ ⟨h⟩⟩

Premises used: MeasurableSpace.CountablySeparated.mk, MeasurableSpace.CountablySeparated.countably_separated, Iff.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m m' : MeasurableSpace α
hsep : CountablySeparated α
h : m ≤ m'
simp_rw : ∀ (hsep : HasCountableSeparatingOn α MeasurableSet univ), HasCountableSeparatingOn α MeasurableSet univ
⊢ CountablySeparated α

Tactic:
simp_rw [countablySeparated_def] at *

Premises used: MeasurableSpace.countablySeparated_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
hsep : HasCountableSeparatingOn α MeasurableSet univ
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
⊢ HasCountableSeparatingOn α MeasurableSet univ

Tactic:
rcases hsep with ⟨S, Sct, Smeas, hS⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
left₁ : ∀ s ∈ S, MeasurableSet s
right :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn α MeasurableSet univ

Tactic:
use S, Sct, (fun s hs ↦ h _ <| Smeas _ hs), hS
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
rw : HasCountableSeparatingOn.{u_1} (↑s : Type u_1) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s
⊢ CountablySeparated.{u_1} (↑s : Type u_1) ↔ HasCountableSeparatingOn α MeasurableSet s

Tactic:
rw [countablySeparated_def]

Premises used: MeasurableSpace.countablySeparated_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ HasCountableSeparatingOn.{u_1} (↑s : Type u_1) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s

Tactic:
HasCountableSeparatingOn.subtype_iff

Premises used: MeasurableSet, HasCountableSeparatingOn.subtype_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ HasCountableSeparatingOn.{u_1} (↑s : Type u_1) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s

Tactic:
exact HasCountableSeparatingOn.subtype_iff

Premises used: HasCountableSeparatingOn.subtype_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : SeparatesPoints α
s : Set α
⊢ SeparatesPoints.{u_1} (↑s : Type u_1)

Tactic:
⟨fun _ _ hxy ↦ Subtype.val_injective <| h.1 _ _ fun _ ht ↦ hxy _ <| measurable_subtype_coe ht⟩

Premises used: measurable_subtype_coe, MeasurableSpace.SeparatesPoints.separates, Subtype.val_injective, Set.preimage, Subtype.val, MeasurableSpace.SeparatesPoints.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : CountablySeparated α
s : Set α
rw : HasCountableSeparatingOn α MeasurableSet s
⊢ CountablySeparated.{u_1} (↑s : Type u_1)

Tactic:
rw [CountablySeparated.subtype_iff]

Premises used: MeasurableSpace.CountablySeparated.subtype_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : CountablySeparated α
s : Set α
⊢ HasCountableSeparatingOn α MeasurableSet s

Tactic:
h.countably_separated.mono (fun s ↦ id) <| subset_univ _

Premises used: Set.subset_univ, HasCountableSeparatingOn.mono, id
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : CountablySeparated α
s : Set α
⊢ HasCountableSeparatingOn α MeasurableSet s

Tactic:
exact h.countably_separated.mono (fun s ↦ id) <| subset_univ _

Premises used: Set.subset_univ, HasCountableSeparatingOn.mono, id
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
⊢ SeparatesPoints α

Tactic:
⟨fun x y h ↦ ?_⟩

Premises used: MeasurableSpace.SeparatesPoints.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
refine : ∀ (x y : α) (h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s), x = y
⊢ SeparatesPoints α

Tactic:
refine ⟨fun x y h ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
x y : α
h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s
⊢ Membership.mem (γ := Set α) {x} x → Membership.mem (γ := Set α) {x} y

Tactic:
specialize h _ (MeasurableSet.singleton x)

Premises used: MeasurableSet.singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
⊢ y = x

Tactic:
simp_rw [mem_singleton_iff, forall_true_left] at h

Premises used: forall_true_left, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
x y : α
h : y = x
⊢ x = y

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
x y : α
h : y = x
⊢ x = y

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : SeparatesPoints α
x : α
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}
⊢ MeasurableSet (α := α) {x}

Tactic:
choose s hsm hxs hys using fun y (h : x ≠ y) ↦ exists_measurableSet_of_ne h

Premises used: MeasurableSpace.exists_measurableSet_of_ne
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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.{u_1} (α := α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1)

Tactic:
MeasurableSet.iInter fun y ↦ .iInter fun h ↦ hsm y h

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
h : Eq (α := Set α) {x} (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1)
⊢ MeasurableSet (α := α) {x}

Tactic:
convert! MeasurableSet.iInter fun y ↦ .iInter fun h ↦ hsm y h

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
h : ∀ (y : α), Membership.mem (γ := Set α) {x} y ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) y
⊢ Eq (α := Set α) {x} (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1)

Tactic:
ext y
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
h₁ :
  ∀ (h : x ≠ y), Membership.mem (γ := Set α) {x} y ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
⊢ Membership.mem (γ := Set α) {x} x ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) x

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
h₁ : ∃ (x_1 : α) (x : x ≠ x_1), y ∉ s x_1 x
⊢ Membership.mem (γ := Set α) {x} y ↔ Membership.mem (γ := Set α) (⋂ (b : α), ⋂ (b_1 : x ≠ b), s b b_1) y

Tactic:
simp only [mem_singleton_iff, h.symm, false_iff, mem_iInter, not_forall]

Premises used: Ne.symm, false_iff, Set.mem_iInter, Set.mem_singleton_iff, Classical.not_forall
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
⊢ ∃ (x_1 : α) (x : x ≠ x_1), y ∉ s x_1 x

Tactic:
⟨y, h, hys y h⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
⊢ ∃ (x_1 : α) (x : x ≠ x_1), y ∉ s x_1 x

Tactic:
exact ⟨y, h, hys y h⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
s : Set α
h : CountablySeparated.{u_1} (↑s : Type u_1)
⊢ HasCountableSeparatingOn α MeasurableSet s

Tactic:
CountablySeparated.subtype_iff.mp h

Premises used: MeasurableSpace.CountablySeparated.subtype_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
s : Set α
h : HasCountableSeparatingOn α MeasurableSet s
⊢ CountablySeparated.{u_1} (↑s : Type u_1)

Tactic:
CountablySeparated.subtype_iff.mpr h

Premises used: Iff.mpr, MeasurableSpace.CountablySeparated.subtype_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
h : CountablyGenerated α
inst_1 : SeparatesPoints α
rcases : ∀ (b : Set (Set α)) (hbc : b.Countable) (hb : inst = generateFrom b), CountablySeparated α
⊢ CountablySeparated α

Tactic:
rcases h with ⟨b, hbc, hb⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst = generateFrom b
⊢ CountablySeparated α

Tactic:
⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, ?_⟩⟩

Premises used: Eq.rec, MeasurableSpace.CountablySeparated.mk, MeasurableSpace.GenerateMeasurable.basic, And.intro, HasCountableSeparatingOn.mk, Exists.intro, Eq.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst = generateFrom b
refine :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ CountablySeparated α

Tactic:
refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, ?_⟩⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst = generateFrom b
⊢ SeparatesPoints α

Tactic:
rw [hb] at ‹SeparatesPoints _›

Premises used: MeasurableSpace.SeparatesPoints
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst_1 : MeasurableSpace α
inst_2 : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst_1 = generateFrom b
inst : SeparatesPoints α
⊢ b.Countable

Tactic:
rw [hb] at ‹SeparatesPoints _›

Premises used: MeasurableSpace.SeparatesPoints
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst_1 : MeasurableSpace α
inst_2 : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst_1 = generateFrom b
inst : SeparatesPoints α
hbc₁ : b.Countable
⊢ inst_1 = generateFrom b

Tactic:
rw [hb] at ‹SeparatesPoints _›

Premises used: MeasurableSpace.SeparatesPoints
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
b : Set (Set α)
inst_1 : SeparatesPoints α
hbc : b.Countable
hb : inst = generateFrom b
⊢ ∀ (x y : α), (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y

Tactic:
separating_of_generateFrom b

Premises used: MeasurableSpace.separating_of_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
b : Set (Set α)
inst_1 : SeparatesPoints α
hbc : b.Countable
hb : inst = generateFrom b
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
⊢ ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y

Tactic:
convert! separating_of_generateFrom b

Premises used: MeasurableSpace.separating_of_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
b : Set (Set α)
inst_1 : SeparatesPoints α
hbc : b.Countable
hb : inst = generateFrom b
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:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablySeparated α
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
⊢ ∃ (m' : MeasurableSpace α), CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m

Tactic:
rcases h with ⟨b, bct, hbm, hb⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
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:
⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩

Premises used: MeasurableSpace.generateFrom, And.intro, Exists.intro, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
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
refine_1 : CountablyGenerated α
refine_2 : SeparatesPoints α
⊢ ∃ (m' : MeasurableSpace α), CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m

Tactic:
refine ⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
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
w : Set (Set α)
h : b.Countable ∧ generateFrom b = generateFrom b
⊢ CountablyGenerated α

Tactic:
use b
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
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
refine_2 : ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
⊢ SeparatesPoints α

Tactic:
rw [@separatesPoints_iff]

Premises used: MeasurableSpace.separatesPoints_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
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
⊢ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y

Tactic:
fun x y hxy ↦ hb _ trivial _ trivial fun _ hs ↦ hxy _ <| measurableSet_generateFrom hs

Premises used: trivial, MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
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
⊢ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y

Tactic:
exact fun x y hxy ↦ hb _ trivial _ trivial fun _ hs ↦ hxy _ <| measurableSet_generateFrom hs

Premises used: trivial
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
rw : ∀ (a : ℕ), Measurable (β := Bool) fun (x : α) ↦ mapNatBool α x a
⊢ Measurable (mapNatBool α)

Tactic:
rw [measurable_pi_iff]

Premises used: measurable_pi_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
⊢ ∀ (a : ℕ), Measurable (β := Bool) fun (x : α) ↦ mapNatBool α x a

Tactic:
fun n ↦ measurable_to_bool ?_

Premises used: measurable_to_bool
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
refine : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (preimage (β := Bool) (fun (x : α) ↦ mapNatBool α x n) {true})
⊢ ∀ (a : ℕ), Measurable (β := Bool) fun (x : α) ↦ mapNatBool α x a

Tactic:
refine fun n ↦ measurable_to_bool ?_

Premises used: measurable_to_bool
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
simp : MeasurableSet (natGeneratingSequence α n)
⊢ MeasurableSet.{u_1} (α := α) (preimage (β := Bool) (fun (x : α) ↦ mapNatBool α x n) {true})

Tactic:
simp only [preimage, mem_singleton_iff, mapNatBool,
    Bool.decide_iff, setOf_mem_eq]

Premises used: Bool.decide_iff, Set.setOf_mem_eq, Set.mem_singleton_iff, Set.preimage, MeasurableSpace.mapNatBool
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ MeasurableSet (natGeneratingSequence α n)

Tactic:
apply measurableSet_natGeneratingSequence

Premises used: MeasurableSpace.measurableSet_natGeneratingSequence
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
rw : CountablyGenerated α → SeparatesPoints α → ∀ ⦃x y : α⦄ (hxy : mapNatBool α x = mapNatBool α y), x = y
⊢ x = y

Tactic:
rw [← generateFrom_natGeneratingSequence α] at *

Premises used: MeasurableSpace.generateFrom_natGeneratingSequence
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : CountablyGenerated α
inst_3 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
a : ∀ s ∈ range (natGeneratingSequence α), x ∈ s ↔ y ∈ s
⊢ x = y

Tactic:
apply separating_of_generateFrom (range (natGeneratingSequence _))

Premises used: MeasurableSpace.separating_of_generateFrom, Set.range, MeasurableSpace.natGeneratingSequence
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : CountablyGenerated α
inst_3 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
a : decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)
rw : Decidable (x ∈ natGeneratingSequence α n)
rw₁ : Decidable (y ∈ natGeneratingSequence α n)
⊢ x ∈ natGeneratingSequence α n ↔ y ∈ natGeneratingSequence α n

Tactic:
rw [← decide_eq_decide]

Premises used: decide_eq_decide
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : CountablyGenerated α
inst_3 : SeparatesPoints α
x y : α
hxy : mapNatBool α x = mapNatBool α y
n : ℕ
⊢ decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)

Tactic:
congr_fun hxy n

Premises used: congr_fun, MeasurableSpace.mapNatBool