-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem analyticSet_range_of_polishSpace {β : Type*} [TopologicalSpace β] [PolishSpace β]
    {f : β → α} (f_cont : Continuous f) : AnalyticSet (range f)

Proof state:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : IsEmpty β
⊢ AnalyticSet (range f)

Tactic:
rw [range_eq_empty]

Result:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : IsEmpty β
⊢ AnalyticSet ∅

Proof state:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
⊢ AnalyticSet (range f)

Tactic:
rw [AnalyticSet]

Result:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
⊢ range f = ∅ ∨ ∃ f_1, Continuous f_1 ∧ range f_1 = range f

Proof state:
case inr.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous g
hg : Surjective g
⊢ range f = ∅ ∨ ∃ f_1, Continuous f_1 ∧ range f_1 = range f

Tactic:
refine Or.inr ⟨f ∘ g, f_cont.comp g_cont, ?_⟩

Result:
case inr.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous g
hg : Surjective g
⊢ range (f ∘ g) = range f

Proof state:
case inr.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous g
hg : Surjective g
⊢ range (f ∘ g) = range f

Tactic:
rw [hg.range_comp]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
⊢ range f = ∅ ∨ ∃ f_1, Continuous f_1 ∧ range f_1 = range f

Tactic:
obtain ⟨g, g_cont, hg⟩ : ∃ g : (ℕ → ℕ) → β, Continuous g ∧ Surjective g :=
  exists_nat_nat_continuous_surjective β

Result:
case inr.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous g
hg : Surjective g
⊢ range f = ∅ ∨ ∃ f_1, Continuous f_1 ∧ range f_1 = range f

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
⊢ AnalyticSet (range f)

Tactic:
cases isEmpty_or_nonempty β

Result:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : IsEmpty β
⊢ AnalyticSet (range f)

case inr
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
⊢ AnalyticSet (range f)

Proof state:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : IsEmpty β
⊢ AnalyticSet ∅

Tactic:
exact analyticSet_empty

Result:
no goals