[GOAL]
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Epi g
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
rw [epi_iff_surjective] at hg 
[GOAL]
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
obtain ⟨g', hg'⟩ := hg.hasRightInverse
[GOAL]
case intro
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
let t : X → Y := g' ∘ f ∘ (pure : X → Ultrafilter X)
[GOAL]
case intro
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
let h : Ultrafilter X → Y := Ultrafilter.extend t
[GOAL]
case intro
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
have hh : Continuous h := continuous_ultrafilter_extend _
[GOAL]
case intro
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
use⟨h, hh⟩
[GOAL]
case h
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ ContinuousMap.mk h ≫ g = f
[PROOFSTEP]
apply Faithful.map_injective (F := forget CompHaus)
[GOAL]
case h.a
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ (forget CompHaus).map (ContinuousMap.mk h ≫ g) = (forget CompHaus).map f
[PROOFSTEP]
simp only [Functor.map_comp, ContinuousMap.coe_mk, coe_comp]
[GOAL]
case h.a
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ (forget CompHaus).map (ContinuousMap.mk (Ultrafilter.extend (g' ∘ ↑f ∘ pure))) ≫ (forget CompHaus).map g =
    (forget CompHaus).map f
[PROOFSTEP]
convert
  denseRange_pure.equalizer (g.continuous.comp hh) f.continuous
    _
      -- Porting note: We need to get the coercions to functions under control.
          -- The next two lines should not be needed.
[GOAL]
case h.a
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ (↑g ∘ h) ∘ pure = ↑f ∘ pure
[PROOFSTEP]
let g'' : ContinuousMap Y Z := g
[GOAL]
case h.a
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
g'' : C(↑Y.toTop, ↑Z.toTop) := g
⊢ (↑g ∘ h) ∘ pure = ↑f ∘ pure
[PROOFSTEP]
have : g'' ∘ g' = id := hg'.comp_eq_id
[GOAL]
case h.a
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget CompHaus).obj Z → (forget CompHaus).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
g'' : C(↑Y.toTop, ↑Z.toTop) := g
this : ↑g'' ∘ g' = id
⊢ (↑g ∘ h) ∘ pure = ↑f ∘ pure
[PROOFSTEP]
rw [comp.assoc, ultrafilter_extend_extends, ← comp.assoc, this, comp.left_id]
