awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Measurable (α := (x : (i : ι) × κ i) → X (x.fst (β := fun (i : ι) ↦ κ i)) (x.snd (β := fun (i : ι) ↦ κ i))) (β :=
    (a : ι) → (b : κ a) → X a b)
    (⇑(Equiv.piCurry (β := κ) X) : (a : (x : (i : ι) × κ i) → X x.fst x.snd) → (a : ι) → (b : κ a) → X a b)

Tactic:
measurable_sigmaCurry

Premises used: measurable_sigmaCurry, Sigma.curry
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Measurable (α := (a : ι) → (b : κ a) → X a b) (β :=
    (x : (i : ι) × κ i) → X (x.fst (β := fun (i : ι) ↦ κ i)) (x.snd (β := fun (i : ι) ↦ κ i)))
    (⇑(Equiv.piCurry (β := κ) X).symm : (a : (a : ι) → (b : κ a) → X a b) → (x : (i : ι) × κ i) → X x.fst x.snd)

Tactic:
measurable_sigmaUncurry

Premises used: measurable_sigmaUncurry, Sigma.uncurry
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableEq β
f g : α → β
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x = g x}

Tactic:
measurableSet_diagonal.preimage (hf.prodMk hg)

Premises used: MeasurableSet.preimage, Set.Mem, setOf, Measurable.prodMk, Set.diagonal, MeasurableEq.measurableSet_diagonal, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableEq β
f g : α → β
hf : Measurable f
hg : Measurable g
⊢ Measurable (β := Prop) fun (x : α) ↦ f x = g x

Tactic:
measurableSet_setOf.mp (measurableSet_eq_fun hf hg)

Premises used: measurableSet_setOf, measurableSet_eq_fun, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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 α
measurableSet_singleton : ∀ (x : α), MeasurableSet (α := α) {x}
⊢ MeasurableSingletonClass α

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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 α
measurableSet_singleton : ∀ (x : α), Measurable (β := Prop) fun (n : α) ↦ n = x
⊢ ∀ (x : α), MeasurableSet (α := α) {x}

Tactic:
simp_rw [← setOf_eq_eq_singleton, measurableSet_setOf]

Premises used: Set.setOf_eq_eq_singleton, measurableSet_setOf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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 : α), Measurable (β := Prop) fun (n : α) ↦ n = x

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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 : MeasurableSet (diagonal α)
⊢ MeasurableEq α

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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 : MeasurableSet.{u_1} (α := α × α) (⋃ (i : α), {(i, i)})
⊢ MeasurableSet (diagonal α)

Tactic:
simp_rw [← Set.range_diag, Set.range_eq_iUnion]

Premises used: Set.range_diag, Set.range_eq_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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.{u_1} (α := α × α) (⋃ (i : α), {(i, i)})

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
h : CountablyGenerated α
⊢ (countableGeneratingSet α).Countable

Tactic:
Countable.insert _ h.isCountablyGenerated.choose_spec.1

Premises used: Exists.choose_spec, MeasurableSpace.CountablyGenerated.isCountablyGenerated, MeasurableSpace.countableGeneratingSet, And.left, Set.Countable.insert
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
⊢ generateFrom (countableGeneratingSet α) = m

Tactic:
(generateFrom_insert_empty _).trans <| h.isCountablyGenerated.choose_spec.2.symm

Premises used: Exists.choose_spec, MeasurableSpace.CountablyGenerated.isCountablyGenerated, MeasurableSpace.countableGeneratingSet, And.right, MeasurableSpace.generateFrom_insert_empty, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
⊢ ∅ ∈ countableGeneratingSet α

Tactic:
mem_insert _ _

Premises used: Set.Mem, MeasurableSpace.countableGeneratingSet, Set.mem_insert
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
⊢ (countableGeneratingSet α).Nonempty

Tactic:
⟨∅, mem_insert _ _⟩

Premises used: Set.Nonempty, Exists.intro, Set.mem_insert, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
s : Set α
hs : s ∈ countableGeneratingSet α
rw : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [← generateFrom_countableGeneratingSet (α := α)]

Premises used: MeasurableSpace.generateFrom_countableGeneratingSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
s : Set α
hs : s ∈ countableGeneratingSet α
⊢ MeasurableSet s

Tactic:
measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
s : Set α
hs : s ∈ countableGeneratingSet α
⊢ MeasurableSet s

Tactic:
exact measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_3
m : MeasurableSpace α
inst : CountablyGenerated α
rw : generateFrom (range (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅)) = m
rw₁ : generateFrom (countableGeneratingSet α) = m
rw₂ rw₃ : m = m
⊢ generateFrom (range (natGeneratingSequence α)) = m

Tactic:
rw [natGeneratingSequence, range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]

Premises used: Set.range_enumerateCountable_of_mem, MeasurableSpace.empty_mem_countableGeneratingSet, MeasurableSpace.generateFrom_countableGeneratingSet, MeasurableSpace.natGeneratingSequence
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ MeasurableSet (natGeneratingSequence α n)

Tactic:
measurableSet_countableGeneratingSet <| Set.enumerateCountable_mem _
    empty_mem_countableGeneratingSet n

Premises used: MeasurableSpace.measurableSet_countableGeneratingSet, Set.enumerateCountable_mem, MeasurableSpace.empty_mem_countableGeneratingSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
h : CountablyGenerated β
f : α → β
rcases : ∀ (b : Set (Set β)) (hbc : b.Countable), CountablyGenerated α
⊢ CountablyGenerated α

Tactic:
rcases h with ⟨⟨b, hbc, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
rw : CountablyGenerated α
⊢ CountablyGenerated α

Tactic:
rw [comap_generateFrom]

Premises used: MeasurableSpace.comap_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
this : MeasurableSpace α := generateFrom (preimage f '' b)
⊢ CountablyGenerated α

Tactic:
⟨_, hbc.image _, rfl⟩

Premises used: Set.Countable.image, MeasurableSpace.CountablyGenerated.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
this : MeasurableSpace α := generateFrom (preimage f '' b)
⊢ CountablyGenerated α

Tactic:
exact ⟨_, hbc.image _, rfl⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
m₁ m₂ : MeasurableSpace β
h₁ : CountablyGenerated β
h₂ : CountablyGenerated β
rcases : ∀ (b₁ : Set (Set β)) (hb₁c : b₁.Countable), CountablyGenerated β
⊢ CountablyGenerated β

Tactic:
rcases h₁ with ⟨⟨b₁, hb₁c, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
m₂ : MeasurableSpace β
h₂ : CountablyGenerated β
b₁ : Set (Set β)
hb₁c : b₁.Countable
rcases : ∀ (b₂ : Set (Set β)) (hb₂c : b₂.Countable), CountablyGenerated β
⊢ CountablyGenerated β

Tactic:
rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
b₁ : Set (Set β)
hb₁c : b₁.Countable
b₂ : Set (Set β)
hb₂c : b₂.Countable
⊢ CountablyGenerated β

Tactic:
@mk _ (_ ⊔ _) ⟨_, hb₁c.union hb₂c, generateFrom_sup_generateFrom⟩

Premises used: MeasurableSpace.generateFrom_sup_generateFrom, Set.Countable.union, MeasurableSpace.CountablyGenerated.mk, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
b₁ : Set (Set β)
hb₁c : b₁.Countable
b₂ : Set (Set β)
hb₂c : b₂.Countable
⊢ CountablyGenerated β

Tactic:
exact @mk _ (_ ⊔ _) ⟨_, hb₁c.union hb₂c, generateFrom_sup_generateFrom⟩

Premises used: MeasurableSpace.generateFrom_sup_generateFrom, Set.Countable.union, MeasurableSpace.CountablyGenerated.mk, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
⊢ ∃ (b : Set (Set α)), b.Countable ∧ inst = generateFrom b

Tactic:
⟨⋃ y, {measurableAtom y}, countable_iUnion (fun i ↦ countable_singleton _), ?_⟩

Premises used: Set.countable_iUnion, measurableAtom, And.intro, Exists.intro, Set.countable_singleton, Singleton.singleton, Set.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
refine : inst = generateFrom (⋃ (y : α), {measurableAtom y})
⊢ ∃ (b : Set (Set α)), b.Countable ∧ inst = generateFrom b

Tactic:
refine ⟨⋃ y, {measurableAtom y}, countable_iUnion (fun i ↦ countable_singleton _), ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
⊢ ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (⋃ (y : α), {measurableAtom y}) t → MeasurableSet t

Tactic:
simp [MeasurableSet.measurableAtom_of_countable]

Premises used: MeasurableSet.measurableAtom_of_countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
refine : inst ≤ generateFrom (⋃ (y : α), {measurableAtom y})
⊢ inst = generateFrom (⋃ (y : α), {measurableAtom y})

Tactic:
refine le_antisymm ?_ (generateFrom_le (by simp [MeasurableSet.measurableAtom_of_countable]))

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
h₁ : s ⊆ ⋃ y ∈ s, measurableAtom y
h₂ : ⋃ y ∈ s, measurableAtom y ⊆ s
⊢ s = ⋃ y ∈ s, measurableAtom y

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ x ∈ measurableAtom x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ Membership.mem (γ := Set α) (⋃ y ∈ s, measurableAtom y) x

Tactic:
simpa using ⟨x, hx, by simp⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
h₂ : ∀ (i : α) (i_1 : i ∈ s), measurableAtom i ⊆ s
⊢ ⋃ y ∈ s, measurableAtom y ⊆ s

Tactic:
simp only [iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ measurableAtom x ⊆ s

Tactic:
measurableAtom_subset hs hx

Premises used: measurableAtom_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ measurableAtom x ⊆ s

Tactic:
exact measurableAtom_subset hs hx

Premises used: measurableAtom_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
⊢ 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
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
this : s = ⋃ y ∈ s, measurableAtom y
rw : MeasurableSet.{u_1} (α := α) (⋃ y ∈ s, measurableAtom y)
⊢ MeasurableSet s

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
s : Set α
hs : MeasurableSet s
this : s = ⋃ y ∈ s, measurableAtom y
apply : ∀ (x : α) (_hx : x ∈ s), MeasurableSet (measurableAtom x)
⊢ MeasurableSet.{u_1} (α := α) (⋃ y ∈ s, measurableAtom y)

Tactic:
apply MeasurableSet.biUnion (to_countable s) (fun x _hx ↦ ?_)

Premises used: Set.to_countable, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
ht : Membership.mem (γ := Set (Set α)) (⋃ (y : α), {measurableAtom y}) (measurableAtom x)
⊢ MeasurableSet (measurableAtom x)

Tactic:
apply measurableSet_generateFrom

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
⊢ Membership.mem (γ := Set (Set α)) (⋃ (y : α), {measurableAtom y}) (measurableAtom x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
p : α → Prop
⊢ CountablyGenerated.{u_1} { x : α // p x }

Tactic:
.comap _

Premises used: MeasurableSpace.CountablyGenerated.comap
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
inst_2 : MeasurableSpace β
inst_3 : CountablyGenerated β
⊢ CountablyGenerated (α × β)

Tactic:
.sup (.comap Prod.fst) (.comap Prod.snd)

Premises used: MeasurableSpace.CountablyGenerated.comap, setOf, Prod.fst, MeasurableSpace.CountablyGenerated.sup, Prod.snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
hs : SeparatesPoints α
x y : α
h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s
⊢ x = y

Tactic:
hs.separates _ _ h

Premises used: MeasurableSpace.SeparatesPoints.separates
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
x y : α
h : x ≠ y
contrapose! : ∀ (h : ∀ (s : Set α) (_ : MeasurableSet s) (_ : x ∈ s), y ∈ s), x = y
⊢ ∃ (s : Set α), MeasurableSet s ∧ x ∈ s ∧ y ∉ s

Tactic:
contrapose! h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
x y : α
h : ∀ (s : Set α) (_ : MeasurableSet s) (_ : x ∈ s), y ∈ s
⊢ x = y

Tactic:
separatesPoints_def h

Premises used: MeasurableSpace.separatesPoints_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : SeparatesPoints α
x y : α
h : ∀ (s : Set α) (_ : MeasurableSet s) (_ : x ∈ s), y ∈ s
⊢ x = y

Tactic:
exact separatesPoints_def h

Premises used: MeasurableSpace.separatesPoints_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ SeparatesPoints α ↔ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y

Tactic:
⟨fun h ↦ fun _ _ hxy ↦ h.separates _ _ fun _ hs xs ↦ (hxy _ hs).mp xs,
    fun h ↦ ⟨fun _ _ hxy ↦ h _ _ fun _ hs ↦
    ⟨fun xs ↦ hxy _ hs xs, not_imp_not.mp fun xs ↦ hxy _ hs.compl xs⟩⟩⟩

Premises used: MeasurableSpace.SeparatesPoints.separates, Compl.compl, MeasurableSet.compl, Iff.intro, Iff.mp, MeasurableSpace.SeparatesPoints.mk, not_imp_not
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ s ∈ S, x ∈ s ↔ y ∈ s
⊢ ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)

Tactic:
rw [← forall_generateFrom_mem_iff_mem_iff] at hxy

Premises used: MeasurableSpace.forall_generateFrom_mem_iff_mem_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y

Tactic:
separatesPoints_def <| fun _ hs ↦ (hxy _ hs).mp

Premises used: Iff.mp, MeasurableSpace.separatesPoints_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y

Tactic:
exact separatesPoints_def <| fun _ hs ↦ (hxy _ hs).mp

Premises used: Iff.mp, MeasurableSpace.separatesPoints_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m m' : MeasurableSpace α
hsep : SeparatesPoints α
h : m ≤ m'
⊢ SeparatesPoints α

Tactic:
@SeparatesPoints.mk _ m' fun _ _ hxy ↦
    @SeparatesPoints.separates _ m hsep _ _ fun _ hs ↦ hxy _ (h _ hs)

Premises used: MeasurableSpace.SeparatesPoints.separates, MeasurableSpace.SeparatesPoints.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Nonempty β
inst_2 : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
by_contra! : ∀ (h : f a₁ ≠ f a₂), False
⊢ f a₁ = f a₂

Tactic:
by_contra! h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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₂
obtain : ∀ (s : Set β) (hs : MeasurableSet s) (hx : f a₁ ∈ s) (hy : f a₂ ∉ s), False
⊢ False

Tactic:
obtain ⟨s, hs, hx, hy⟩ := 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 : 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
inr : ∀ (h' : f ⁻¹' s = univ), False
⊢ False

Tactic:
obtain h' | h' := MeasurableSpace.measurableSet_bot_iff.mp (hf hs)

Premises used: MeasurableSpace.measurableSet_bot_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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 = ∅
⊢ ¬?_mvar.12512

Tactic:
hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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 = ∅
inl : f a₁ ∉ s
⊢ False

Tactic:
absurd hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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 = ∅
⊢ f a₁ ∉ s

Tactic:
simp [← mem_preimage, h']

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
inr : f a₂ ∈ s
⊢ False

Tactic:
absurd hy
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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
⊢ f a₂ ∈ s

Tactic:
simp [← mem_preimage, h']

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
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₂

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']
-- 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₂
inl : ∀ (h' : IsEmpty α), ∃ (c : β), f = fun (x : α) ↦ c
inr : ∀ (h' : Nonempty α), ∃ (c : β), f = fun (x : α) ↦ c
⊢ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
obtain h' | h' := isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- 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' : IsEmpty α
⊢ ∀ (x : α), f x = Classical.ofNonempty

Tactic:
simp
-- 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' : IsEmpty α
w : β
h₁ : f = fun (x : α) ↦ Classical.ofNonempty
⊢ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
use (Classical.ofNonempty : β), funext (by simp)

Premises used: Classical.ofNonempty, funext