awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed[t'] s
right : IsOpen[t'] s
A : AnalyticSet s
⊢ s = id '' s

Tactic:
simp only [id, image_id']

Premises used: Set.image_id', id
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
⊢ ∃ (b : Set (Set (↑(range f) : Type u_4))), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
exists_countable_basis (range f)

Premises used: Set.Elem, TopologicalSpace.exists_countable_basis, Set.range
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
obtain :
  ∀ (b : Set (Set (↑(range f) : Type u_4))) (b_count : b.Countable) (hb : IsTopologicalBasis b),
    ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

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

Premises used: Set.Elem, TopologicalSpace.exists_countable_basis, Set.range, Set
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
⊢ Countable.{u_4 + 1} (↑b : Type u_4)

Tactic:
haveI : Countable b := b_count.to_subtype
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
s : (↑b : Type u_4)
hs : MeasurableSet (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
⊢ IsClopenable (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))

Tactic:
apply MeasurableSet.isClopenable

Premises used: MeasurableSet.isClopenable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
s : (↑b : Type u_4)
⊢ MeasurableSet (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))

Tactic:
hf.subtype_mk (hb.isOpen s.2).measurableSet

Premises used: Measurable.subtype_mk, TopologicalSpace.IsTopologicalBasis.isOpen, IsOpen.measurableSet, Set.rangeFactorization, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
s : (↑b : Type u_4)
⊢ MeasurableSet (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))

Tactic:
exact hf.subtype_mk (hb.isOpen s.2).measurableSet

Premises used: Measurable.subtype_mk, TopologicalSpace.IsTopologicalBasis.isOpen, IsOpen.measurableSet, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
⊢ ∀ (s : (↑b : Type u_4)), IsClopenable (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))

Tactic:
have : ∀ s : b, IsClopenable (rangeFactorization f ⁻¹' s) := fun s ↦ by
    apply MeasurableSet.isClopenable
    exact hf.subtype_mk (hb.isOpen s.2).measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this_1 : Countable.{u_4 + 1} (↑b : Type u_4)
this : ∀ (s : (↑b : Type u_4)), IsClopenable (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
choose :
  ∀ (T : (s : (↑b : Type u_4)) → TopologicalSpace α) (Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t)
    (Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α),
    (∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))) →
      ∀ (Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))),
        ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

Tactic:
choose T Tt Tpolish _ Topen using this
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
⊢ ∃ (t' : TopologicalSpace α), (∀ (i : (↑b : Type u_4)), t' ≤ T i) ∧ t' ≤ t ∧ PolishSpace α

Tactic:
exists_polishSpace_forall_le (t := t) T Tt Tpolish

Premises used: PolishSpace.exists_polishSpace_forall_le
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
obtain :
  ∀ (t' : TopologicalSpace α) (t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i) (t't : t' ≤ t) (t'_polish : PolishSpace α),
    ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

Tactic:
obtain ⟨t', t'T, t't, t'_polish⟩ :
      ∃ t' : TopologicalSpace α, (∀ i, t' ≤ T i) ∧ t' ≤ t ∧ @PolishSpace α t' :=
    exists_polishSpace_forall_le (t := t) T Tt Tpolish

Premises used: PolishSpace.exists_polishSpace_forall_le, TopologicalSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
t' : TopologicalSpace α
t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

Tactic:
⟨t', t't, ?_, t'_polish⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
t' : TopologicalSpace α
t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
refine : Continuous[t', tβ] f
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

Tactic:
refine ⟨t', t't, ?_, t'_polish⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
t' : TopologicalSpace α
t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
⊢ Continuous[t', instTopologicalSpaceSubtype] (rangeFactorization f)

Tactic:
have : Continuous[t', _] (rangeFactorization f) :=
    hb.continuous_iff.2 fun s hs => t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this_1 : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
t' : TopologicalSpace α
t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
this : Continuous[t', instTopologicalSpaceSubtype] (rangeFactorization f)
⊢ Continuous[t', tβ] f

Tactic:
continuous_subtype_val.comp this

Premises used: continuous_subtype_val, Continuous.comp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst : PolishSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
tβ : TopologicalSpace β
inst_3 : MeasurableSpace β
inst_4 : OpensMeasurableSpace β
f : α → β
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
hf : Measurable f
b : Set (Set (↑(range f) : Type u_4))
b_count : b.Countable
hb : IsTopologicalBasis b
this_1 : Countable.{u_4 + 1} (↑b : Type u_4)
T : (s : (↑b : Type u_4)) → TopologicalSpace α
Tt : ∀ (s : (↑b : Type u_4)), T s ≤ t
Tpolish : ∀ (s : (↑b : Type u_4)), PolishSpace α
h : ∀ (s : (↑b : Type u_4)), IsClosed[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
Topen : ∀ (s : (↑b : Type u_4)), IsOpen[T s] (rangeFactorization f ⁻¹' (↑s : Set (↑(range f) : Type u_4)))
t' : TopologicalSpace α
t'T : ∀ (i : (↑b : Type u_4)), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
this : Continuous[t', instTopologicalSpaceSubtype] (rangeFactorization f)
⊢ Continuous[t', tβ] f

Tactic:
exact continuous_subtype_val.comp this

Premises used: continuous_subtype_val, Continuous.comp
-- 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 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
⊢ MeasurableSet s

Tactic:
rw [eq_borel_upgradeStandardBorel X] at hs

Premises used: eq_borel_upgradeStandardBorel
-- 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 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
hs₁ : MeasurableSet s
⊢ Measurable f

Tactic:
rw [eq_borel_upgradeStandardBorel X] at hs

Premises used: eq_borel_upgradeStandardBorel
-- 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 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
rcases :
  ∀ (τ' : TopologicalSpace X) (hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace) (hfc : Continuous[_, inst_2] f)
    (hτ' : PolishSpace X), AnalyticSet (f '' s)
⊢ AnalyticSet (f '' s)

Tactic:
rcases hf.exists_continuous with ⟨τ', hle, hfc, hτ'⟩

Premises used: Measurable.exists_continuous
-- 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 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous[τ', inst_2] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
⊢ BorelSpace X

Tactic:
haveI b' : BorelSpace X := ⟨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 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous[τ', inst_2] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
⊢ borel X ≤ borel X

Tactic:
have hle := borel_anti hle
-- 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 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle_1 : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous[τ', inst_2] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
hle : borel X ≤ borel X
⊢ AnalyticSet (f '' s)

Tactic:
(hle _ hs).analyticSet.image_of_continuous hfc

Premises used: MeasureTheory.AnalyticSet.image_of_continuous, MeasurableSet.analyticSet
-- 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 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle_1 : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous[τ', inst_2] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
hle : borel X ≤ borel X
⊢ AnalyticSet (f '' s)

Tactic:
exact (hle _ hs).analyticSet.image_of_continuous hfc

Premises used: MeasureTheory.AnalyticSet.image_of_continuous, MeasurableSet.analyticSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
s : Set Y
hs : AnalyticSet s
f : X → Y
hf : Continuous[inst, inst_1] f
rcases :
  ∀ (Z : Type) (w : TopologicalSpace Z),
    PolishSpace Z →
      ∀ (g : Z → Y) (hg : Continuous[_, inst_1] g) (hs : AnalyticSet (range g)), AnalyticSet (f ⁻¹' range g)
⊢ AnalyticSet (f ⁻¹' s)

Tactic:
rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨Z, _, _, g, hg, rfl⟩

Premises used: MeasureTheory.analyticSet_iff_exists_polishSpace_range, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
Z : Type
w : TopologicalSpace Z
w_1 : PolishSpace Z
g : Z → Y
hg : Continuous[w, inst_1] g
hs : AnalyticSet (range g)
⊢ IsClosed[instTopologicalSpaceProd] {x : X × Z | f x.1 = g x.2}

Tactic:
have : IsClosed {x : X × Z | f x.1 = g x.2} := isClosed_eq hf.fst' hg.snd'
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
Z : Type
w : TopologicalSpace Z
w_1 : PolishSpace Z
g : Z → Y
hg : Continuous[w, inst_1] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x : X × Z | f x.1 = g x.2}
⊢ AnalyticSet.{u_3} (α := X) (image (α := X × Z) Prod.fst {x : X × Z | f x.1 = g x.2})

Tactic:
this.analyticSet.image_of_continuous continuous_fst

Premises used: MeasureTheory.AnalyticSet.image_of_continuous, continuous_fst, IsClosed.analyticSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
Z : Type
w : TopologicalSpace Z
w_1 : PolishSpace Z
g : Z → Y
hg : Continuous[w, inst_1] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x : X × Z | f x.1 = g x.2}
h : f ⁻¹' range g = image (α := X × Z) Prod.fst {x : X × Z | f x.1 = g x.2}
⊢ AnalyticSet (f ⁻¹' range g)

Tactic:
convert! this.analyticSet.image_of_continuous continuous_fst

Premises used: MeasureTheory.AnalyticSet.image_of_continuous, continuous_fst, IsClosed.analyticSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
Z : Type
w : TopologicalSpace Z
w_1 : PolishSpace Z
g : Z → Y
hg : Continuous[w, inst_1] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x : X × Z | f x.1 = g x.2}
h :
  ∀ (x : X), x ∈ f ⁻¹' range g ↔ Membership.mem (γ := Set X) (image (α := X × Z) Prod.fst {x : X × Z | f x.1 = g x.2}) x
⊢ f ⁻¹' range g = image (α := X × Z) Prod.fst {x : X × Z | f x.1 = g x.2}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
Z : Type
w : TopologicalSpace Z
w_1 : PolishSpace Z
g : Z → Y
hg : Continuous[w, inst_1] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x : X × Z | f x.1 = g x.2}
x : X
⊢ x ∈ f ⁻¹' range g ↔ Membership.mem (γ := Set X) (image (α := X × Z) Prod.fst {x : X × Z | f x.1 = g x.2}) x

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
h : ∀ (m n : ι), MeasurablySeparable (s m) (t n)
choose :
  ∀ (u : (m n : ι) → Set α) (hsu : ∀ (m n : ι), s m ⊆ u m n) (htu : ∀ (m n : ι), Disjoint (t n) (u m n))
    (hu : ∀ (m n : ι), MeasurableSet (u m n)), MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)
⊢ MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)

Tactic:
choose u hsu htu hu using h
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)

Tactic:
⟨⋃ m, ⋂ n, u m n, ?_, ?_, ?_⟩

Premises used: Set.iInter, MeasureTheory.MeasurablySeparable, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
refine_1 : Subset.{u_3} (α := Set α) (⋃ (n : ι), s n) (⋃ (m : ι), ⋂ (n : ι), u m n)
refine_2 : Disjoint.{u_3} (α := Set α) (⋃ (m : ι), t m) (⋃ (m : ι), ⋂ (n : ι), u m n)
refine_3 : MeasurableSet.{u_3} (α := α) (⋃ (m : ι), ⋂ (n : ι), u m n)
⊢ MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)

Tactic:
refine ⟨⋃ m, ⋂ n, u m n, ?_, ?_, ?_⟩