-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.MeasurableSet.analyticSet_image {X Y : Type*} [MeasurableSpace X]
    [StandardBorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y]
    [OpensMeasurableSpace Y] {f : X → Y} [SecondCountableTopology (range f)] {s : Set X}
    (hs : MeasurableSet s) (hf : Measurable f) : AnalyticSet (f '' s)

Proof state:
case intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous f
hτ' : PolishSpace X
⊢ AnalyticSet (f '' s)

Tactic:
letI m' : MeasurableSpace X := @borel _ τ'

Result:
case intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
⊢ AnalyticSet (f '' s)

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
⊢ AnalyticSet (f '' s)

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

Result:
case intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous f
hτ' : PolishSpace X
⊢ AnalyticSet (f '' s)

Proof state:
case intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
⊢ AnalyticSet (f '' s)

Tactic:
haveI b' : BorelSpace X := ⟨rfl⟩

Result:
case intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
⊢ AnalyticSet (f '' s)

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
⊢ AnalyticSet (f '' s)

Tactic:
letI := upgradeStandardBorel X

Result:
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
⊢ AnalyticSet (f '' s)

Proof state:
case intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
⊢ AnalyticSet (f '' s)

Tactic:
have hle := borel_anti hle

Result:
case intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle✝ : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
hle : borel X ≤ borel X
⊢ AnalyticSet (f '' s)

Proof state:
case intro.intro.intro
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle✝ : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous 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

Result:
no goals