awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : 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 γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
cauchy_y : CauchySeq y
this_3 : Nonempty γ
z : γ := limUnder atTop y
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst_2] v
w_open : IsOpen[inst_2] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
δ : ℝ
δpos : δ > 0
hδ : ball z δ ⊆ f ⁻¹' v
n : ℕ
hn : u n + dist (y n) z < δ
fsnv : f '' (↑(s n) : Set γ) ⊆ v
this : x ∈ closure[inst_2] v
⊢ False

Tactic:
disjoint_left.1 (hvw.closure_left w_open) this xw

Premises used: Set.disjoint_left, Iff.mp, Disjoint.closure_left
-- 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_2 : 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 γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
x : β
hx : Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) x
s : (n : ℕ) → (↑b : Type u_3)
hs : ∀ (n : ℕ), Bornology.IsBounded (↑(s n) : Set γ) ∧ diam (↑(s n) : Set γ) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : (n : ℕ) → γ
hy : ∀ (n : ℕ), y n ∈ (↑(s n) : Set γ)
I : ∀ (m n : ℕ), ((↑(s m) : Set γ) ∩ (↑(s n) : Set γ)).Nonempty
cauchy_y : CauchySeq y
this_3 : Nonempty γ
z : γ := limUnder atTop y
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst_2] v
w_open : IsOpen[inst_2] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
δ : ℝ
δpos : δ > 0
hδ : ball z δ ⊆ f ⁻¹' v
n : ℕ
hn : u n + dist (y n) z < δ
fsnv : f '' (↑(s n) : Set γ) ⊆ v
this : x ∈ closure[inst_2] v
⊢ False

Tactic:
exact disjoint_left.1 (hvw.closure_left w_open) this xw

Premises used: Set.disjoint_left, Iff.mp, Disjoint.closure_left
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
rw : MeasurableSet.{u_4} (α := β) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
⊢ MeasurableSet (f '' s)

Tactic:
rw [image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ PolishSpace.{u_3} (↑s : Type u_3)

Tactic:
haveI : PolishSpace s := IsClosed.polishSpace hs
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace.{u_3} (↑s : Type u_3)
f_cont₁ : Continuous[instTopologicalSpaceSubtype, inst_2] fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
f_inj₁ : Injective.{u_3 + 1, u_4 + 1} (β := β) fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
⊢ MeasurableSet.{u_4} (α := β) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))

Tactic:
apply measurableSet_range_of_continuous_injective

Premises used: MeasureTheory.measurableSet_range_of_continuous_injective
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace.{u_3} (↑s : Type u_3)
f_cont₁ f_cont₂ f_cont₃ f_cont₄ :
  ∀ (f_cont : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : γ) ↦ β) f)) (f_inj : InjOn f s)
    (this : PolishSpace.{u_3} (↑s : Type u_3)),
    Continuous[instTopologicalSpaceSubtype, inst_2] fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)

Tactic:
rwa [continuousOn_iff_continuous_restrict] at f_cont

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace.{u_3} (↑s : Type u_3)
f_inj₁ f_inj₂ f_inj₃ f_inj₄ :
  ∀ (f_inj : Injective (s.restrict (π := fun (a : γ) ↦ β) f)) (this : PolishSpace.{u_3} (↑s : Type u_3)),
    Injective.{u_3 + 1, u_4 + 1} (β := β) fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
⊢ Injective.{u_3 + 1, u_4 + 1} (β := β) fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)

Tactic:
rwa [injOn_iff_injective] at f_inj

Premises used: Set.injOn_iff_injective
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst_3 : PolishSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ ∃ t' ≤ tγ, PolishSpace γ ∧ IsClosed s ∧ IsOpen s

Tactic:
hs.isClopenable

Premises used: MeasurableSet.isClopenable, PolishSpace.IsClopenable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst_3 : PolishSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
obtain :
  ∀ (t' : TopologicalSpace γ) (t't : t' ≤ tγ) (t'_polish : PolishSpace γ) (s_closed : IsClosed s),
    IsOpen s → MeasurableSet (f '' s)
⊢ MeasurableSet (f '' s)

Tactic:
obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
      ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s :=
    hs.isClopenable

Premises used: MeasurableSet.isClopenable, TopologicalSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst_3 : PolishSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
s_closed : IsClosed[t'] s
right : IsOpen[t'] s
⊢ MeasurableSet (f '' s)

Tactic:
@IsClosed.measurableSet_image_of_continuousOn_injOn γ t' t'_polish β _ _ _ _ s s_closed f
      (f_cont.mono_dom t't) f_inj

Premises used: ContinuousOn.mono_dom, IsClosed.measurableSet_image_of_continuousOn_injOn
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst_3 : PolishSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
s_closed : IsClosed[t'] s
right : IsOpen[t'] s
⊢ MeasurableSet (f '' s)

Tactic:
exact
    @IsClosed.measurableSet_image_of_continuousOn_injOn γ t' t'_polish β _ _ _ _ s s_closed f
      (f_cont.mono_dom t't) f_inj

Premises used: ContinuousOn.mono_dom, IsClosed.measurableSet_image_of_continuousOn_injOn
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
rcases :
  ∀ (τ : TopologicalSpace α), SecondCountableTopology α → T4Space α → OpensMeasurableSpace α → MeasurableSet (f '' s)
⊢ MeasurableSet (f '' s)

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

Premises used: exists_opensMeasurableSpace_of_countablySeparated
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left : SecondCountableTopology α
left_1 : T4Space α
right : OpensMeasurableSpace α
⊢ ∃ t' ≤ tγ, Continuous[_, τ] f ∧ PolishSpace γ

Tactic:
f_meas.exists_continuous

Premises used: Measurable.exists_continuous
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left : SecondCountableTopology α
left_1 : T4Space α
right : OpensMeasurableSpace α
obtain :
  ∀ (t' : TopologicalSpace γ) (t't : t' ≤ tγ) (f_cont : Continuous[_, τ] f) (t'_polish : PolishSpace γ),
    MeasurableSet (f '' s)
⊢ MeasurableSet (f '' s)

Tactic:
obtain ⟨t', t't, f_cont, t'_polish⟩ :
      ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' :=
    f_meas.exists_continuous

Premises used: Measurable.exists_continuous, TopologicalSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left : SecondCountableTopology α
left_1 : T4Space α
right : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous[t', τ] f
t'_polish : PolishSpace γ
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rwa [← eq_borel_upgradeStandardBorel γ]

Premises used: eq_borel_upgradeStandardBorel
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left : SecondCountableTopology α
left_1 : T4Space α
right : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous[t', τ] f
t'_polish : PolishSpace γ
⊢ MeasurableSet s

Tactic:
have hs' := (borel_anti t't s) <| by rwa [← eq_borel_upgradeStandardBorel γ]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this_1 : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left : SecondCountableTopology α
left_1 : T4Space α
right : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous[t', τ] f
t'_polish : PolishSpace γ
hs' : MeasurableSet s
this_2 : MeasurableSpace γ := borel γ
this : BorelSpace γ := ⋯
⊢ MeasurableSet (f '' s)

Tactic:
hs'.image_of_continuousOn_injOn f_cont.continuousOn f_inj

Premises used: Continuous.continuousOn, MeasurableSet.image_of_continuousOn_injOn
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this_1 : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left : SecondCountableTopology α
left_1 : T4Space α
right : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous[t', τ] f
t'_polish : PolishSpace γ
hs' : MeasurableSet s
this_2 : MeasurableSpace γ := borel γ
this : BorelSpace γ := ⋯
⊢ MeasurableSet (f '' s)

Tactic:
exact hs'.image_of_continuousOn_injOn f_cont.continuousOn f_inj

Premises used: Continuous.continuousOn, MeasurableSet.image_of_continuousOn_injOn
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
f : γ → β
inst_2 : BorelSpace β
inst_3 : TopologicalSpace γ
inst_4 : PolishSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
f_cont : Continuous[inst_3, tβ] f
f_inj : Injective f
⊢ MeasurableEmbedding f

Tactic:
{ injective := f_inj
    measurable := f_cont.measurable
    measurableSet_image' := fun _u hu =>
      hu.image_of_continuousOn_injOn f_cont.continuousOn f_inj.injOn }

Premises used: Continuous.continuousOn, Function.Injective.injOn, MeasurableEmbedding.mk, MeasurableSet.image_of_continuousOn_injOn, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : BorelSpace β
inst_3 : TopologicalSpace γ
inst_4 : PolishSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set (↑s : Type u_3)
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)

Tactic:
have A : MeasurableSet (((↑) : s → γ) '' u) :=
        (MeasurableEmbedding.subtype_coe hs).measurableSet_image.2 hu
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : BorelSpace β
inst_3 : TopologicalSpace γ
inst_4 : PolishSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set (↑s : Type u_3)
hu : MeasurableSet u
A : MeasurableSet (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)
⊢ MeasurableSet (f '' Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)

Tactic:
have B : MeasurableSet (f '' ((↑) : s → γ) '' u) :=
        A.image_of_continuousOn_injOn (f_cont.mono (Subtype.coe_image_subset s u))
          (f_inj.mono (Subtype.coe_image_subset s u))
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : BorelSpace β
inst_3 : TopologicalSpace γ
inst_4 : PolishSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set (↑s : Type u_3)
hu : MeasurableSet u
A : MeasurableSet (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)
B : MeasurableSet (f '' Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (B : MeasurableSet (f ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)),
    MeasurableSet (s.restrict (π := fun (a : γ) ↦ β) f '' u)
⊢ MeasurableSet (s.restrict (π := fun (a : γ) ↦ β) f '' u)

Tactic:
rwa [← image_comp] at B

Premises used: Set.image_comp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
f_meas : Measurable f
f_inj : Injective f
⊢ MeasurableEmbedding f

Tactic:
{ injective := f_inj
    measurable := f_meas
    measurableSet_image' := fun _u hu => hu.image_of_measurable_injOn f_meas f_inj.injOn }

Premises used: MeasurableSet.image_of_measurable_injOn, Function.Injective.injOn, MeasurableEmbedding.mk
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ = borel γ

Tactic:
le_antisymm ?_ (borel_anti hle)

Premises used: le_antisymm, borel_anti
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
refine : borel γ ≤ borel γ
⊢ borel γ = borel γ

Tactic:
refine le_antisymm ?_ (borel_anti hle)

Premises used: le_antisymm, borel_anti
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
⊢ MeasurableEmbedding.{u_3, u_3} (α := γ) id

Tactic:
have e := @Continuous.measurableEmbedding
    _ _ (@borel _ t') t' _ _ (@BorelSpace.mk _ _ (borel γ) rfl)
    t _ (@borel _ t) (@BorelSpace.mk _ t (@borel _ t) rfl) (continuous_id_of_le hle) injective_id
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
e : MeasurableEmbedding.{u_3, u_3} (α := γ) id
⊢ MeasurableSet (id '' s)

Tactic:
e.measurableSet_image.2 hs

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
e : MeasurableEmbedding.{u_3, u_3} (α := γ) id
h : s = id '' s
⊢ MeasurableSet s

Tactic:
convert! e.measurableSet_image.2 hs
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
e : MeasurableEmbedding.{u_3, u_3} (α := γ) id
⊢ s = id '' s

Tactic:
simp only [id_eq, image_id']

Premises used: Set.image_id', id_eq
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
⊢ IsClopenable s ↔ MeasurableSet s

Tactic:
⟨fun hs => ?_, fun hs => hs.isClopenable⟩

Premises used: MeasurableSet.isClopenable, Iff.intro
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
refine : ∀ (hs : IsClopenable s), MeasurableSet s
⊢ IsClopenable s ↔ MeasurableSet s

Tactic:
refine ⟨fun hs => ?_, fun hs => hs.isClopenable⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
hs : IsClopenable s
borelize : ∀ [BorelSpace γ], MeasurableSet s
⊢ MeasurableSet s

Tactic:
borelize γ
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
hs : IsClopenable s
inst_1 : BorelSpace γ
this : MeasurableSpace γ := borel γ
⊢ ∃ t' ≤ tγ, PolishSpace γ ∧ IsClosed s ∧ IsOpen s

Tactic:
hs

Premises used: PolishSpace.IsClopenable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
hs : IsClopenable s
inst_1 : BorelSpace γ
this : MeasurableSpace γ := borel γ
obtain :
  ∀ (t' : TopologicalSpace γ) (t't : t' ≤ tγ) (t'_polish : PolishSpace γ),
    IsClosed s → ∀ (s_open : IsOpen s), MeasurableSet s
⊢ MeasurableSet s

Tactic:
obtain ⟨t', t't, t'_polish, _, s_open⟩ :
    ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s := hs

Premises used: TopologicalSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
inst_1 : BorelSpace γ
this : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left : IsClosed[t'] s
s_open : IsOpen[t'] s
rw : MeasurableSet s
rw₁ : PolishSpace γ
⊢ MeasurableSet s

Tactic:
rw [← borel_eq_borel_of_le t'_polish _ t't]

Premises used: MeasureTheory.borel_eq_borel_of_le
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
inst_1 : BorelSpace γ
this : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ MeasurableSet s

Tactic:
MeasurableSpace.measurableSet_generateFrom s_open

Premises used: MeasurableSpace.measurableSet_generateFrom