case intro.intro.intro.intro
α✝ : Type ?u.62930
inst✝³ : TopologicalSpace α✝
ι : Type ?u.62936
α : Type u_1
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
⊢ AnalyticSet s
α✝ : Type ?u.62930
inst✝³ : TopologicalSpace α✝
ι : Type ?u.62936
α : Type u_1
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
⊢ AnalyticSet s
obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
  ∃ t' : TopologicalSpace α, t' ≤ t ∧ @PolishSpace α t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s :=
  hs.isClopenable
case intro.intro.intro.intro
α✝ : Type ?u.62930
inst✝³ : TopologicalSpace α✝
ι : Type ?u.62936
α : Type u_1
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
A : AnalyticSet s
⊢ AnalyticSet s
case intro.intro.intro.intro
α✝ : Type ?u.62930
inst✝³ : TopologicalSpace α✝
ι : Type ?u.62936
α : Type u_1
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
⊢ AnalyticSet s
have A := @IsClosed.analyticSet α t' t'_polish s s_closed
case h.e'_3
α✝ : Type ?u.62930
inst✝³ : TopologicalSpace α✝
ι : Type ?u.62936
α : Type u_1
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
A : AnalyticSet s
⊢ s = id '' s
case intro.intro.intro.intro
α✝ : Type ?u.62930
inst✝³ : TopologicalSpace α✝
ι : Type ?u.62936
α : Type u_1
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
A : AnalyticSet s
⊢ AnalyticSet s
convert @AnalyticSet.image_of_continuous α t' α t s A id (continuous_id_of_le t't)
no goals
case h.e'_3
α✝ : Type ?u.62930
inst✝³ : TopologicalSpace α✝
ι : Type ?u.62936
α : Type u_1
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
A : AnalyticSet s
⊢ s = id '' s
simp only [id.def, image_id']