-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem analyticSet_iff_exists_polishSpace_range {s : Set α} :
    AnalyticSet s ↔
      ∃ (β : Type) (h : TopologicalSpace β) (_ : @PolishSpace β h) (f : β → α),
        @Continuous _ _ h _ f ∧ range f = s

Proof state:
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Tactic:
refine ⟨Empty, inferInstance, inferInstance, Empty.elim, continuous_bot, ?_⟩

Result:
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ range Empty.elim = s

Proof state:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet s

Tactic:
rw [← f_range]

Result:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet (range f)

Proof state:
case mp
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : AnalyticSet s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Tactic:
rw [AnalyticSet] at h

Result:
case mp
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Proof state:
case mp
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ AnalyticSet s → ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : AnalyticSet s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Proof state:
case mp.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : ∃ f, Continuous f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Tactic:
exact ⟨ℕ → ℕ, inferInstance, inferInstance, h⟩

Result:
no goals

Proof state:
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ range Empty.elim = ∅

Tactic:
exact range_eq_empty _

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Tactic:
rcases h with h | h

Result:
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

case mp.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : ∃ f, Continuous f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Proof state:
case mpr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ (∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s) → AnalyticSet s

Tactic:
rintro ⟨β, h, h', f, f_cont, f_range⟩

Result:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ AnalyticSet s ↔ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ AnalyticSet s → ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s

case mpr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ (∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ range f = s) → AnalyticSet s

Proof state:
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ range Empty.elim = s

Tactic:
rw [h]

Result:
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ range Empty.elim = ∅

Proof state:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet (range f)

Tactic:
exact analyticSet_range_of_polishSpace f_cont

Result:
no goals