[GOAL]
⊢ T2Space Empty
[PROOFSTEP]
infer_instance
[GOAL]
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : toUniformSpace (CpltSepUniformSpace.of (Completion ↑X)) ⟶ toUniformSpace Y
⊢ extensionHom (completionHom X ≫ f) = f
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : toUniformSpace (CpltSepUniformSpace.of (Completion ↑X)) ⟶ toUniformSpace Y
⊢ ↑(extensionHom (completionHom X ≫ f)) = ↑f
[PROOFSTEP]
funext x
[GOAL]
case a.h
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : toUniformSpace (CpltSepUniformSpace.of (Completion ↑X)) ⟶ toUniformSpace Y
x : ↑(toUniformSpace (completionFunctor.obj X))
⊢ ↑(extensionHom (completionHom X ≫ f)) x = ↑f x
[PROOFSTEP]
exact congr_fun (Completion.extension_comp_coe f.property) x
[GOAL]
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : completionFunctor.obj X ⟶ Y
⊢ (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f
[PROOFSTEP]
dsimp
[GOAL]
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : completionFunctor.obj X ⟶ Y
⊢ extensionHom (completionHom X ≫ f) = f
[PROOFSTEP]
erw [extension_comp_coe]
[GOAL]
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ ↑((fun f => completionHom X ≫ f) ((fun f => extensionHom f) f)) = ↑f
[PROOFSTEP]
funext x
[GOAL]
case a.h
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : ↑X
⊢ ↑((fun f => completionHom X ≫ f) ((fun f => extensionHom f) f)) x = ↑f x
[PROOFSTEP]
cases f
[GOAL]
case a.h.mk
X : UniformSpaceCat
Y : CpltSepUniformSpace
x : ↑X
val✝ : ↑X → ↑((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y)
property✝ : UniformContinuous val✝
⊢ ↑((fun f => completionHom X ≫ f) ((fun f => extensionHom f) { val := val✝, property := property✝ })) x =
    ↑{ val := val✝, property := property✝ } x
[PROOFSTEP]
exact @Completion.extension_coe _ _ _ _ _ (CpltSepUniformSpace.separatedSpace _) ‹_› _
[GOAL]
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ ↑((fun X Y =>
              { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                left_inv :=
                  (_ :
                    ∀ (f : completionFunctor.obj X ⟶ Y),
                      (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                right_inv :=
                  (_ :
                    ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                      (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
            X' Y).symm
      (f ≫ g) =
    completionFunctor.map f ≫
      ↑((fun X Y =>
                { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                  left_inv :=
                    (_ :
                      ∀ (f : completionFunctor.obj X ⟶ Y),
                        (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                        (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
              X Y).symm
        g
[PROOFSTEP]
apply hom_ext
[GOAL]
case a
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ (forget UniformSpaceCat).map
      (↑((fun X Y =>
                { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                  left_inv :=
                    (_ :
                      ∀ (f : completionFunctor.obj X ⟶ Y),
                        (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                        (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
              X' Y).symm
        (f ≫ g)) =
    (forget UniformSpaceCat).map
      (completionFunctor.map f ≫
        ↑((fun X Y =>
                  { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                    left_inv :=
                      (_ :
                        ∀ (f : completionFunctor.obj X ⟶ Y),
                          (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                          (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
                X Y).symm
          g)
[PROOFSTEP]
funext x
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
⊢ (forget UniformSpaceCat).map
      (↑((fun X Y =>
                { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                  left_inv :=
                    (_ :
                      ∀ (f : completionFunctor.obj X ⟶ Y),
                        (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                        (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
              X' Y).symm
        (f ≫ g))
      x =
    (forget UniformSpaceCat).map
      (completionFunctor.map f ≫
        ↑((fun X Y =>
                  { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                    left_inv :=
                      (_ :
                        ∀ (f : completionFunctor.obj X ⟶ Y),
                          (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                          (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
                X Y).symm
          g)
      x
[PROOFSTEP]
dsimp
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
⊢ (forget UniformSpaceCat).map (extensionHom (f ≫ g)) x =
    (forget UniformSpaceCat).map (completionFunctor.map f ≫ extensionHom g) x
[PROOFSTEP]
erw [coe_comp]
  -- Porting note : used to be `erw [← Completion.extension_map]`
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
⊢ (forget UniformSpaceCat).map (extensionHom (f ≫ g)) x =
    ((forget UniformSpaceCat).map (extensionHom g) ∘ (forget UniformSpaceCat).map (completionFunctor.map f)) x
[PROOFSTEP]
have := (Completion.extension_map (γ := Y) (f := g) g.2 f.2)
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
this :
  Completion.extension ((forget UniformSpaceCat).map g) ∘ Completion.map ↑f =
    Completion.extension ((forget UniformSpaceCat).map g ∘ ↑f)
⊢ (forget UniformSpaceCat).map (extensionHom (f ≫ g)) x =
    ((forget UniformSpaceCat).map (extensionHom g) ∘ (forget UniformSpaceCat).map (completionFunctor.map f)) x
[PROOFSTEP]
simp only [forget_map_eq_coe] at this ⊢
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
this : Completion.extension ↑g ∘ Completion.map ↑f = Completion.extension (↑g ∘ ↑f)
⊢ ↑(extensionHom (f ≫ g)) x = (↑(extensionHom g) ∘ ↑(completionFunctor.map f)) x
[PROOFSTEP]
erw [this]
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
this : Completion.extension ↑g ∘ Completion.map ↑f = Completion.extension (↑g ∘ ↑f)
⊢ ↑(extensionHom (f ≫ g)) x = Completion.extension (↑g ∘ ↑f) x
[PROOFSTEP]
rfl
