awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous[_, inst] f
g : (ℕ → ℕ) → α
g_cont : Continuous[_, inst] g
h : Disjoint (range f) (range g)
⊢ MeasurablySeparable (range f) (range g)

Tactic:
exact measurablySeparable_range_of_disjoint f_cont g_cont h

Premises used: MeasureTheory.measurablySeparable_range_of_disjoint
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
rcases : ∀ (u : Set α) (hsu : s ⊆ u) (hdu : Disjoint sᶜ u) (hmu : MeasurableSet u), MeasurableSet s
⊢ MeasurableSet s

Tactic:
rcases hs.measurablySeparable hsc disjoint_compl_right with ⟨u, hsu, hdu, hmu⟩

Premises used: disjoint_compl_right, MeasureTheory.AnalyticSet.measurablySeparable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
u : Set α
hsu : s ⊆ u
hdu : Disjoint sᶜ u
hmu : MeasurableSet u
⊢ s = u

Tactic:
hsu.antisymm (disjoint_compl_left_iff_subset.1 hdu)

Premises used: Set.disjoint_compl_left_iff_subset, HasSubset.Subset.antisymm, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
u : Set α
hsu : s ⊆ u
hdu : Disjoint sᶜ u
hmu : MeasurableSet u
⊢ s ⊆ s

Tactic:
obtain rfl : s = u := hsu.antisymm (disjoint_compl_left_iff_subset.1 hdu)

Premises used: Set.disjoint_compl_left_iff_subset, HasSubset.Subset.antisymm, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
u : Set α
hsu : s ⊆ u
hdu : Disjoint sᶜ u
hmu : MeasurableSet u
hsu₁ : s ⊆ s
⊢ Disjoint sᶜ s

Tactic:
obtain rfl : s = u := hsu.antisymm (disjoint_compl_left_iff_subset.1 hdu)

Premises used: Set.disjoint_compl_left_iff_subset, HasSubset.Subset.antisymm, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
u : Set α
hsu : s ⊆ u
hdu : Disjoint sᶜ u
hmu : MeasurableSet u
hsu₁ : s ⊆ s
hdu₁ : Disjoint sᶜ s
⊢ MeasurableSet s

Tactic:
obtain rfl : s = u := hsu.antisymm (disjoint_compl_left_iff_subset.1 hdu)

Premises used: Set.disjoint_compl_left_iff_subset, HasSubset.Subset.antisymm, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
hsu : s ⊆ s
hdu : Disjoint sᶜ s
hmu : MeasurableSet s
⊢ MeasurableSet s

Tactic:
hmu
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
hsu : s ⊆ s
hdu : Disjoint sᶜ s
hmu : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact hmu
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s

Tactic:
⟨fun h => ?_, fun h => hf h⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
refine : ∀ (h : MeasurableSet (f ⁻¹' s)), MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s

Tactic:
refine ⟨fun h => ?_, fun h => hf h⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
rcases : ∀ (τ : TopologicalSpace Z), SecondCountableTopology Z → T4Space Z → OpensMeasurableSpace Z → MeasurableSet s
⊢ MeasurableSet s

Tactic:
rcases exists_opensMeasurableSpace_of_countablySeparated Z with ⟨τ, _, _, _⟩

Premises used: exists_opensMeasurableSpace_of_countablySeparated
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
⊢ MeasurableSet s

Tactic:
apply AnalyticSet.measurableSet_of_compl

Premises used: MeasureTheory.AnalyticSet.measurableSet_of_compl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
hs : AnalyticSet (f '' f ⁻¹' s)
⊢ AnalyticSet s

Tactic:
rw [← image_preimage_eq s hsurj]

Premises used: Set.image_preimage_eq
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' s)

Tactic:
h.analyticSet_image hf

Premises used: MeasurableSet.analyticSet_image
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' s)

Tactic:
exact h.analyticSet_image hf

Premises used: MeasurableSet.analyticSet_image
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
hsc : AnalyticSet (f '' f ⁻¹' sᶜ)
⊢ AnalyticSet sᶜ

Tactic:
rw [← image_preimage_eq sᶜ hsurj]

Premises used: Compl.compl, Set.image_preimage_eq
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' sᶜ)

Tactic:
h.compl.analyticSet_image hf

Premises used: Set.Mem, setOf, MeasurableSet.compl, Set.preimage, Not, MeasurableSet.analyticSet_image
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' sᶜ)

Tactic:
exact h.compl.analyticSet_image hf

Premises used: MeasurableSet.compl, MeasurableSet.analyticSet_image
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
⊢ MeasurableSpace.map f inst = inst_2

Tactic:
MeasurableSpace.ext fun _ => hf.measurableSet_preimage_iff_of_surjective hsurj

Premises used: Measurable.measurableSet_preimage_iff_of_surjective, MeasurableSpace.ext
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
⊢ Measurable f

Tactic:
have d := hf.mono le_rfl OpensMeasurableSpace.borel_le
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this : MeasurableSpace Y := borel Y
⊢ BorelSpace Y

Tactic:
haveI : BorelSpace Y := ⟨rfl⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this_1 : MeasurableSpace Y := borel Y
this : BorelSpace Y
⊢ MeasurableSpace.map f inst = borel Y

Tactic:
d.map_measurableSpace_eq hsurj

Premises used: Measurable.map_measurableSpace_eq
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this_1 : MeasurableSpace Y := borel Y
this : BorelSpace Y
⊢ MeasurableSpace.map f inst = borel Y

Tactic:
exact d.map_measurableSpace_eq hsurj

Premises used: Measurable.map_measurableSpace_eq
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
⊢ BorelSpace Y

Tactic:
⟨(hf.map_measurableSpace_eq hsurj).symm.trans <| hf.map_measurableSpace_eq_borel hsurj⟩

Premises used: Measurable.map_measurableSpace_eq, BorelSpace.mk, Eq.symm, Eq.trans, Measurable.map_measurableSpace_eq_borel
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
f : X → Z
inst_3 : CountablySeparated.{u_5} (↑(range f) : Type u_5)
hf : Measurable f
s : Set Z
⊢ MeasurableSet (f ⁻¹' s) ↔
    MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s)

Tactic:
have hf' : Measurable (rangeFactorization f) := hf.subtype_mk
  hf'.measurableSet_preimage_iff_of_surjective (s := Subtype.val ⁻¹' s)
    rangeFactorization_surjective

Premises used: Set.Mem, Measurable.subtype_mk, setOf, Measurable.measurableSet_preimage_iff_of_surjective, Set.rangeFactorization_surjective, Set.preimage, Set.rangeFactorization
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
f : X → Z
inst_3 : CountablySeparated.{u_5} (↑(range f) : Type u_5)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
rw :
  MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
    MeasurableSet (s ∩ range f)
rw₁ :
  MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
    MeasurableSet (range f ∩ s)
rw₂ :
  MeasurableSet
      (image (α := { x : Z // x ∈ range f }) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f))
        (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s)) ↔
    MeasurableSet (range f ∩ s)
rw₃ rw₄ : MeasurableSet (range f ∩ s) ↔ MeasurableSet (range f ∩ s)
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm,
    ← (MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe]

Premises used: MeasurableEmbedding.measurableSet_image, Subtype.image_preimage_coe, Set.inter_comm, Measurable.measurableSet_preimage_iff_preimage_val, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
β : Type u_6
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace β
inst_3 : MeasurableSpace Z
f : X → Z
inst_4 : CountablySeparated.{u_5} (↑(range f) : Type u_5)
hf : Measurable f
g : Z → β
⊢ Measurable (g ∘ f) ↔ Measurable ((range f).restrict (π := fun (a : Z) ↦ β) g)

Tactic:
forall₂_congr fun s _ => measurableSet_preimage_iff_preimage_val hf (s := g ⁻¹' s)

Premises used: Measurable, forall₂_congr, Measurable.measurableSet_preimage_iff_preimage_val
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Z : Type u_5
β : Type u_6
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace β
inst_3 : MeasurableSpace Z
inst_4 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
g : Z → β
⊢ Measurable (g ∘ f) ↔ Measurable g

Tactic:
forall₂_congr fun s _ => measurableSet_preimage_iff_of_surjective hf hsurj (s := g ⁻¹' s)

Premises used: Measurable, Measurable.measurableSet_preimage_iff_of_surjective, forall₂_congr
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : TopologicalSpace Y
inst_5 : T0Space Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst, inst_4] f
hsurj : Surjective f
⊢ let this := borel Y;
  BorelSpace Y

Tactic:
borelize Y
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : TopologicalSpace Y
inst_5 : T0Space Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst, inst_4] f
hsurj : Surjective f
this : MeasurableSpace Y := borel Y
this_1 : BorelSpace Y
⊢ MeasurableSpace.map f inst_2 = borel Y

Tactic:
hf.measurable.map_measurableSpace_eq hsurj

Premises used: Measurable.map_measurableSpace_eq, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : TopologicalSpace Y
inst_5 : T0Space Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst, inst_4] f
hsurj : Surjective f
this : MeasurableSpace Y := borel Y
this_1 : BorelSpace Y
⊢ MeasurableSpace.map f inst_2 = borel Y

Tactic:
exact hf.measurable.map_measurableSpace_eq hsurj

Premises used: Measurable.map_measurableSpace_eq, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst, inst_2] f
hsurj : Surjective f
⊢ let this := borel X;
  BorelSpace X

Tactic:
borelize X
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst, inst_2] f
hsurj : Surjective f
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ MeasurableSpace.map f (borel X) = borel Y

Tactic:
hf.map_eq_borel hsurj

Premises used: Continuous.map_eq_borel
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst, inst_2] f
hsurj : Surjective f
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ MeasurableSpace.map f (borel X) = borel Y

Tactic:
exact hf.map_eq_borel hsurj

Premises used: Continuous.map_eq_borel
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
ι : Type u_2
X : Type u_3
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
s : Setoid X
inst_4 : T0Space.{u_3} (Quotient s)
inst_5 : SecondCountableTopology.{u_3} (Quotient s)
⊢ BorelSpace.{u_3} (Quotient s)

Tactic:
⟨continuous_quotient_mk'.map_eq_borel Quotient.mk'_surjective⟩

Premises used: continuous_quotient_mk', Quotient.mk'_surjective, Continuous.map_eq_borel, BorelSpace.mk
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
ι : Type u_2
G : Type u_3
inst : TopologicalSpace G
inst_1 : PolishSpace G
inst_2 : Group G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
N : Subgroup G
inst_5 : T2Space.{u_3} (G ⧸ N)
inst_6 : SecondCountableTopology.{u_3} (G ⧸ N)
⊢ BorelSpace.{u_3} (G ⧸ N)

Tactic:
Quotient.borelSpace

Premises used: Quotient.borelSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
ι : Type u_2
G : Type u_3
inst : TopologicalSpace G
inst_1 : PolishSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
N : Subgroup G
inst_6 : N.Normal
inst_7 : IsClosed[inst] (↑N : Set G)
⊢ BorelSpace.{u_3} (G ⧸ N)

Tactic:
⟨continuous_mk.map_eq_borel mk_surjective⟩

Premises used: QuotientGroup.continuous_mk, Continuous.map_eq_borel, BorelSpace.mk, QuotientGroup.mk_surjective
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
⊢ ∃ (b : Set (Set γ)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
exists_countable_basis γ

Premises used: TopologicalSpace.exists_countable_basis
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
obtain :
  ∀ (b : Set (Set γ)) (b_count : b.Countable) (b_nonempty : ∅ ∉ b) (hb : IsTopologicalBasis b), MeasurableSet (range f)
⊢ MeasurableSet (range f)

Tactic:
obtain ⟨b, b_count, b_nonempty, hb⟩ :
    ∃ b : Set (Set γ), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b := exists_countable_basis γ

Premises used: TopologicalSpace.exists_countable_basis, Set
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
haveI : ∀ (this : Encodable (↑b : Type u_3)), MeasurableSet (range f)
⊢ MeasurableSet (range f)

Tactic:
haveI : Encodable b := b_count.toEncodable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
p : A
this₁ :
  Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ))
    (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ))
⊢ ∃ (q : Set β),
    f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q ∧
      Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) q ∧ MeasurableSet q

Tactic:
apply
      AnalyticSet.measurablySeparable ((hb.isOpen p.1.1.2).analyticSet_image f_cont)
        ((hb.isOpen p.1.2.2).analyticSet_image f_cont)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, Prod.fst, IsOpen.analyticSet_image, Subtype.val, Prod.snd, Subtype.property, MeasureTheory.AnalyticSet.measurablySeparable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
p : A
⊢ Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ))
    (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ))

Tactic:
Disjoint.image p.2 f_inj.injOn (subset_univ _) (subset_univ _)

Premises used: Function.Injective.injOn, Set.subset_univ, Disjoint.image, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
p : A
⊢ Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ))
    (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ))

Tactic:
exact Disjoint.image p.2 f_inj.injOn (subset_univ _) (subset_univ _)

Premises used: Function.Injective.injOn, Set.subset_univ, Disjoint.image, Subtype.property