case inl
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : IsEmpty β
⊢ AnalyticSet (range f)

case inr
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
⊢ AnalyticSet (range f)
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
⊢ AnalyticSet (range f)
cases isEmpty_or_nonempty β
case inl
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : IsEmpty β
⊢ AnalyticSet ∅
case inl
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : IsEmpty β
⊢ AnalyticSet (range f)
rw [range_eq_empty]
no goals
case inl
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : IsEmpty β
⊢ AnalyticSet ∅
exact analyticSet_empty
case inr
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
⊢ range f = ∅ ∨ ∃ f_1, Continuous f_1 ∧ range f_1 = range f
case inr
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
⊢ AnalyticSet (range f)
rw [AnalyticSet]
case inr.intro.intro
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
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
case inr
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
⊢ range f = ∅ ∨ ∃ f_1, Continuous f_1 ∧ range f_1 = range f
obtain ⟨g, g_cont, hg⟩ : ∃ g : (ℕ → ℕ) → β, Continuous g ∧ Surjective g :=
  exists_nat_nat_continuous_surjective β
case inr.intro.intro
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous g
hg : Surjective g
⊢ range (f ∘ g) = range f
case inr.intro.intro
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
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
refine' Or.inr ⟨f ∘ g, f_cont.comp g_cont, _⟩
no goals
case inr.intro.intro
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.684
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous f
h✝ : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous g
hg : Surjective g
⊢ range (f ∘ g) = range f
rw [hg.range_comp]