case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous f
hs : IsClosed (range f)
hne : Set.Nonempty (range f)
fs : ∀ (x : (n : ℕ) → E n), x ∈ range f → f x = x
⊢ ∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
⊢ ∃ f, (∀ (x : ↑s), f ↑x = x) ∧ Surjective f ∧ Continuous f
obtain ⟨f, fs, rfl, f_cont⟩ :
  ∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f :=
  exists_retraction_of_isClosed hs hne
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous f
hs : IsClosed (range f)
hne : Set.Nonempty (range f)
fs : ∀ (x : (n : ℕ) → E n), x ∈ range f → f x = x
A : ∀ (x : ↑(range f)), rangeFactorization f ↑x = x
⊢ ∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous f
hs : IsClosed (range f)
hne : Set.Nonempty (range f)
fs : ∀ (x : (n : ℕ) → E n), x ∈ range f → f x = x
⊢ ∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1
have A : ∀ x : range f, rangeFactorization f x = x := fun x ↦ Subtype.eq <| fs x x.2
no goals
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous f
hs : IsClosed (range f)
hne : Set.Nonempty (range f)
fs : ∀ (x : (n : ℕ) → E n), x ∈ range f → f x = x
A : ∀ (x : ↑(range f)), rangeFactorization f ↑x = x
⊢ ∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1
exact ⟨rangeFactorization f, A, fun x => ⟨x, A x⟩, f_cont.subtype_mk _⟩