[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
x✝ : OpensLeCover U
⊢ {
          obj := fun V =>
            {
              obj :=
                { left := V.obj, right := { as := PUnit.unit },
                  hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
              property :=
                (_ :
                  ∃ Y_1 h g,
                    presieveOfCoveringAux U Y g ∧
                      h ≫ g =
                        { left := V.obj, right := { as := PUnit.unit },
                            hom :=
                              homOfLE
                                (_ :
                                  (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
          map := fun {x x_1} g => Over.homMk g }.map
      (𝟙 x✝) =
    𝟙
      ({
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.obj
        x✝)
[PROOFSTEP]
refine Over.OverMorphism.ext ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
x✝ : OpensLeCover U
⊢ ({
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.map
        (𝟙 x✝)).left =
    (𝟙
        ({
              obj := fun V =>
                {
                  obj :=
                    { left := V.obj, right := { as := PUnit.unit },
                      hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                  property :=
                    (_ :
                      ∃ Y_1 h g,
                        presieveOfCoveringAux U Y g ∧
                          h ≫ g =
                            { left := V.obj, right := { as := PUnit.unit },
                                hom :=
                                  homOfLE
                                    (_ :
                                      (𝟭 (Opens ↑X)).obj V.obj ≤
                                        (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
              map := fun {x x_1} g => Over.homMk g }.obj
          x✝)).left
[PROOFSTEP]
simp only [Functor.id_obj, Sieve.generate_apply, Functor.const_obj_obj, Over.homMk_left, eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
x✝² x✝¹ x✝ : OpensLeCover U
f : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
⊢ {
          obj := fun V =>
            {
              obj :=
                { left := V.obj, right := { as := PUnit.unit },
                  hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
              property :=
                (_ :
                  ∃ Y_1 h g,
                    presieveOfCoveringAux U Y g ∧
                      h ≫ g =
                        { left := V.obj, right := { as := PUnit.unit },
                            hom :=
                              homOfLE
                                (_ :
                                  (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
          map := fun {x x_1} g => Over.homMk g }.map
      (f ≫ g) =
    {
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.map
        f ≫
      {
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.map
        g
[PROOFSTEP]
refine Over.OverMorphism.ext ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
x✝² x✝¹ x✝ : OpensLeCover U
f : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
⊢ ({
            obj := fun V =>
              {
                obj :=
                  { left := V.obj, right := { as := PUnit.unit },
                    hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                property :=
                  (_ :
                    ∃ Y_1 h g,
                      presieveOfCoveringAux U Y g ∧
                        h ≫ g =
                          { left := V.obj, right := { as := PUnit.unit },
                              hom :=
                                homOfLE
                                  (_ :
                                    (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
            map := fun {x x_1} g => Over.homMk g }.map
        (f ≫ g)).left =
    ({
              obj := fun V =>
                {
                  obj :=
                    { left := V.obj, right := { as := PUnit.unit },
                      hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                  property :=
                    (_ :
                      ∃ Y_1 h g,
                        presieveOfCoveringAux U Y g ∧
                          h ≫ g =
                            { left := V.obj, right := { as := PUnit.unit },
                                hom :=
                                  homOfLE
                                    (_ :
                                      (𝟭 (Opens ↑X)).obj V.obj ≤
                                        (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
              map := fun {x x_1} g => Over.homMk g }.map
          f ≫
        {
              obj := fun V =>
                {
                  obj :=
                    { left := V.obj, right := { as := PUnit.unit },
                      hom := homOfLE (_ : (𝟭 (Opens ↑X)).obj V.obj ≤ (Functor.fromPUnit Y).obj { as := PUnit.unit }) },
                  property :=
                    (_ :
                      ∃ Y_1 h g,
                        presieveOfCoveringAux U Y g ∧
                          h ≫ g =
                            { left := V.obj, right := { as := PUnit.unit },
                                hom :=
                                  homOfLE
                                    (_ :
                                      (𝟭 (Opens ↑X)).obj V.obj ≤
                                        (Functor.fromPUnit Y).obj { as := PUnit.unit }) }.hom) },
              map := fun {x x_1} g => Over.homMk g }.map
          g).left
[PROOFSTEP]
simp only [Functor.id_obj, Sieve.generate_apply, Functor.const_obj_obj, Over.homMk_left, eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom),
    (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X_1 =
      (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj X_1
[PROOFSTEP]
rintro ⟨⟨_, _⟩, _⟩
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
left✝ : Opens ↑X
right✝ : Discrete PUnit
hom✝ : (𝟭 (Opens ↑X)).obj left✝ ⟶ (Functor.fromPUnit Y).obj right✝
property✝ : (Sieve.generate (presieveOfCoveringAux U Y)).arrows { left := left✝, right := right✝, hom := hom✝ }.hom
⊢ (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj
      { obj := { left := left✝, right := right✝, hom := hom✝ }, property := property✝ } =
    (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj
      { obj := { left := left✝, right := right✝, hom := hom✝ }, property := property✝ }
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
left✝ : Opens ↑X
right✝ : Discrete PUnit
hom✝ : (𝟭 (Opens ↑X)).obj left✝ ⟶ (Functor.fromPUnit Y).obj right✝
property✝ : (Sieve.generate (presieveOfCoveringAux U Y)).arrows { left := left✝, right := right✝, hom := hom✝ }.hom
⊢ { obj := { left := left✝, right := right✝, hom := hom✝ }, property := property✝ } =
    (generateEquivalenceOpensLe_inverse' U ?m.44608).obj
      ((generateEquivalenceOpensLe_functor' U ?m.44561).obj
        { obj := { left := left✝, right := right✝, hom := hom✝ }, property := property✝ })
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 Y_1 : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom) (f : X_1 ⟶ Y_1),
    (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).map f =
      eqToHom
          (_ :
            (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X_1 =
              (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj
                X_1) ≫
        (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).map f ≫
          eqToHom
            (_ :
              (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj
                  Y_1 =
                (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj Y_1)
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ Y✝ : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).map f✝ =
    eqToHom
        (_ :
          (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X✝ =
            (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj X✝) ≫
      (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).map f✝ ≫
        eqToHom
          (_ :
            (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj Y✝ =
              (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj Y✝)
[PROOFSTEP]
refine Over.OverMorphism.ext ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ Y✝ : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom
f✝ : X✝ ⟶ Y✝
⊢ ((𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).map f✝).left =
    (eqToHom
          (_ :
            (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X✝ =
              (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj
                X✝) ≫
        (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).map f✝ ≫
          eqToHom
            (_ :
              (generateEquivalenceOpensLe_functor' U ?m.44561 ⋙ generateEquivalenceOpensLe_inverse' U ?m.44608).obj Y✝ =
                (𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj Y✝)).left
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 : OpensLeCover U),
    (generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙
            generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj
        X_1 =
      (𝟭 (OpensLeCover U)).obj X_1
[PROOFSTEP]
intro
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ : OpensLeCover U
⊢ (generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙ generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj
      X✝ =
    (𝟭 (OpensLeCover U)).obj X✝
[PROOFSTEP]
refine FullSubcategory.ext _ _ ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ : OpensLeCover U
⊢ ((generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙ generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj
        X✝).obj =
    ((𝟭 (OpensLeCover U)).obj X✝).obj
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 Y_1 : OpensLeCover U) (f : X_1 ⟶ Y_1),
    HEq
      ((generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙
            generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).map
        f)
      ((𝟭 (OpensLeCover U)).map f)
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
X✝ Y✝ : OpensLeCover U
f✝ : X✝ ⟶ Y✝
⊢ HEq
    ((generateEquivalenceOpensLe_inverse' U (_ : Y = iSup U) ⋙
          generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).map
      f✝)
    ((𝟭 (OpensLeCover U)).map f✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
        (eqToHom
          (_ :
            op (opensLeCoverCocone U).pt =
              op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt)) ≫
      NatTrans.app (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows))).π j =
    NatTrans.app
      (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
          (F.mapCone (Cocone.op (opensLeCoverCocone U)))).π
      j
[PROOFSTEP]
erw [← F.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
      (eqToHom
          (_ :
            op (opensLeCoverCocone U).pt =
              op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt) ≫
        NatTrans.app (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows)).π j) =
    NatTrans.app
      (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
          (F.mapCone (Cocone.op (opensLeCoverCocone U)))).π
      j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom (_ : op (opensLeCoverCocone U).pt = op Y) ≫ j.unop.obj.hom.op) =
    F.map
      (NatTrans.app (opensLeCoverCocone U).ι ((generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj j.unop)).op
[PROOFSTEP]
congr 1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
        (eqToHom
          (_ :
            op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
              op (opensLeCoverCocone U).pt)) ≫
      NatTrans.app
        (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
            (F.mapCone (Cocone.op (opensLeCoverCocone U)))).π
        j =
    NatTrans.app (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows))).π j
[PROOFSTEP]
erw [← F.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
      (eqToHom
          (_ :
            op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
              op (opensLeCoverCocone U).pt) ≫
        NatTrans.app (Cocone.op (opensLeCoverCocone U)).π
          ((Equivalence.op (generateEquivalenceOpensLe U hY)).functor.obj j)) =
    NatTrans.app (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows))).π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
      (eqToHom (_ : op Y = op (opensLeCoverCocone U).pt) ≫
        (NatTrans.app (opensLeCoverCocone U).ι
            ((generateEquivalenceOpensLe_functor' U (_ : Y = iSup U)).obj j.unop)).op) =
    F.map j.unop.obj.hom.op
[PROOFSTEP]
congr 1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ConeMorphism.mk
        (F.map
          (eqToHom
            (_ :
              op (opensLeCoverCocone U).pt =
                op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt))) ≫
      ConeMorphism.mk
        (F.map
          (eqToHom
            (_ :
              op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
                op (opensLeCoverCocone U).pt))) =
    𝟙
      (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
        (F.mapCone (Cocone.op (opensLeCoverCocone U))))
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (ConeMorphism.mk
          (F.map
            (eqToHom
              (_ :
                op (opensLeCoverCocone U).pt =
                  op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt))) ≫
        ConeMorphism.mk
          (F.map
            (eqToHom
              (_ :
                op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
                  op (opensLeCoverCocone U).pt)))).Hom =
    (𝟙
        (Cone.whisker (Equivalence.op (generateEquivalenceOpensLe U hY)).functor
          (F.mapCone (Cocone.op (opensLeCoverCocone U))))).Hom
[PROOFSTEP]
simp [eqToHom_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ConeMorphism.mk
        (F.map
          (eqToHom
            (_ :
              op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
                op (opensLeCoverCocone U).pt))) ≫
      ConeMorphism.mk
        (F.map
          (eqToHom
            (_ :
              op (opensLeCoverCocone U).pt =
                op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt))) =
    𝟙 (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows)))
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (ConeMorphism.mk
          (F.map
            (eqToHom
              (_ :
                op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt =
                  op (opensLeCoverCocone U).pt))) ≫
        ConeMorphism.mk
          (F.map
            (eqToHom
              (_ :
                op (opensLeCoverCocone U).pt =
                  op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows).pt)))).Hom =
    (𝟙 (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U Y)).arrows)))).Hom
[PROOFSTEP]
simp [eqToHom_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
R : Presieve Y
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone (coveringOfPresieve Y R)))) ≃
    IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate R).arrows)))
[PROOFSTEP]
convert
  isLimitOpensLeEquivGenerate₁ F (coveringOfPresieve Y R)
    (coveringOfPresieve.iSup_eq_of_mem_grothendieck Y R hR).symm using
  1
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
R : Presieve Y
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate R).arrows))) =
    IsLimit
      (F.mapCone
        (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux (coveringOfPresieve Y R) Y)).arrows)))
[PROOFSTEP]
rw [covering_presieve_eq_self R]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ IsSheaf F ↔ IsSheafOpensLeCover F
[PROOFSTEP]
refine' (Presheaf.isSheaf_iff_isLimit _ _).trans _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))) ↔
    IsSheafOpensLeCover F
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))) →
    IsSheafOpensLeCover F
[PROOFSTEP]
intro h ι U
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone U))))
[PROOFSTEP]
rw [(isLimitOpensLeEquivGenerate₁ F U rfl).nonempty_congr]
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty
    (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U (iSup U))).arrows))))
[PROOFSTEP]
apply h
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCoveringAux U (iSup U)) ∈
    GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) (iSup U)
[PROOFSTEP]
apply presieveOfCovering.mem_grothendieckTopology
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ IsSheafOpensLeCover F →
    ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
[PROOFSTEP]
intro h Y S
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
⊢ S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
[PROOFSTEP]
rw [← Sieve.generate_sieve S]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
⊢ Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate S.arrows).arrows))))
[PROOFSTEP]
intro hS
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate S.arrows).arrows))))
[PROOFSTEP]
rw [← (isLimitOpensLeEquivGenerate₂ F S.1 hS).nonempty_congr]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone (coveringOfPresieve Y S.arrows)))))
[PROOFSTEP]
apply h


[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]


[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ fst f g ≫ f = snd f g ≫ g
[PROOFSTEP]
ext ⟨_, h⟩
[GOAL]
case w.mk
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
val✝ : ↑X.toTop × ↑Y.toTop
h : val✝ ∈ {xy | ↑f xy.fst = ↑g xy.snd}
⊢ ↑(fst f g ≫ f) { val := val✝, property := h } = ↑(snd f g ≫ g) { val := val✝, property := h }
[PROOFSTEP]
exact h
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
z : ↑Z.toTop
⊢ (↑a z, ↑b z) ∈ {xy | ↑f xy.fst = ↑g xy.snd}
[PROOFSTEP]
apply_fun (fun q => q z) at w
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
z : ↑Z.toTop
w : ↑(a ≫ f) z = ↑(b ≫ g) z
⊢ (↑a z, ↑b z) ∈ {xy | ↑f xy.fst = ↑g xy.snd}
[PROOFSTEP]
exact w
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ Continuous fun z => { val := (↑a z, ↑b z), property := (_ : ↑(a ≫ f) z = ↑(b ≫ g) z) }
[PROOFSTEP]
apply Continuous.subtype_mk
[GOAL]
case h
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ Continuous fun x => (↑a x, ↑b x)
[PROOFSTEP]
rw [continuous_prod_mk]
[GOAL]
case h
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ (Continuous fun x => ↑a x) ∧ Continuous fun x => ↑b x
[PROOFSTEP]
exact ⟨a.continuous, b.continuous⟩
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
⊢ a = b
[PROOFSTEP]
ext z
[GOAL]
case w
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : (forget CompHaus).obj Z
⊢ ↑a z = ↑b z
[PROOFSTEP]
apply_fun (fun q => q z) at hfst hsnd
[GOAL]
case w
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
z : (forget CompHaus).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑a z = ↑b z
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case w.a
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
z : (forget CompHaus).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑(↑a z) = ↑(↑b z)
[PROOFSTEP]
apply Prod.ext
[GOAL]
case w.a.h₁
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
z : (forget CompHaus).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).fst = (↑(↑b z)).fst
[PROOFSTEP]
exact hfst
[GOAL]
case w.a.h₂
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
Z : CompHaus
a b : Z ⟶ pullback f g
z : (forget CompHaus).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).snd = (↑(↑b z)).snd
[PROOFSTEP]
exact hsnd
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.fst f g = (pullbackIsoPullback f g).hom ≫ Limits.pullback.fst
[PROOFSTEP]
dsimp [pullbackIsoPullback]
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.fst f g =
    (Limits.IsLimit.conePointUniqueUpToIso (pullback.isLimit f g) (Limits.limit.isLimit (Limits.cospan f g))).hom ≫
      Limits.pullback.fst
[PROOFSTEP]
simp only [Limits.limit.conePointUniqueUpToIso_hom_comp, pullback.cone_pt, pullback.cone_π]
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.snd f g = (pullbackIsoPullback f g).hom ≫ Limits.pullback.snd
[PROOFSTEP]
dsimp [pullbackIsoPullback]
[GOAL]
X Y B : CompHaus
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.snd f g =
    (Limits.IsLimit.conePointUniqueUpToIso (pullback.isLimit f g) (Limits.limit.isLimit (Limits.cospan f g))).hom ≫
      Limits.pullback.snd
[PROOFSTEP]
simp only [Limits.limit.conePointUniqueUpToIso_hom_comp, pullback.cone_pt, pullback.cone_π]
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
e : (a : α) → X a ⟶ B
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
apply continuous_sigma
[GOAL]
case hf
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
e : (a : α) → X a ⟶ B
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
intro a
[GOAL]
case hf
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
e : (a : α) → X a ⟶ B
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
exact (e a).continuous
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g
[PROOFSTEP]
ext ⟨a, x⟩
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toTop
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
specialize h a
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
apply_fun (fun q => q x) at h
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toTop
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
exact h
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), NatTrans.app (cocone X).ι j ≫ m = NatTrans.app s.ι j
a : α
⊢ ι (fun a => X a) a ≫ m = ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s
[PROOFSTEP]
specialize hm ⟨a⟩
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
hm : NatTrans.app (cocone X).ι { as := a } ≫ m = NatTrans.app s.ι { as := a }
⊢ ι (fun a => X a) a ≫ m = ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s
[PROOFSTEP]
ext t
[GOAL]
case w
α : Type
inst✝ : Fintype α
X : α → CompHaus
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
hm : NatTrans.app (cocone X).ι { as := a } ≫ m = NatTrans.app s.ι { as := a }
t : (forget CompHaus).obj (X a)
⊢ ↑(ι (fun a => X a) a ≫ m) t =
    ↑(ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s) t
[PROOFSTEP]
apply_fun (fun q => q t) at hm
[GOAL]
case w
α : Type
inst✝ : Fintype α
X : α → CompHaus
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
t : (forget CompHaus).obj (X a)
hm : ↑(NatTrans.app (cocone X).ι { as := a } ≫ m) t = ↑(NatTrans.app s.ι { as := a }) t
⊢ ↑(ι (fun a => X a) a ≫ m) t =
    ↑(ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s) t
[PROOFSTEP]
exact hm
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
a : α
⊢ Limits.Sigma.ι X a ≫ (coproductIsoCoproduct X).inv = finiteCoproduct.ι X a
[PROOFSTEP]
dsimp [coproductIsoCoproduct]
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
a : α
⊢ Limits.Sigma.ι X a ≫
      (Limits.IsColimit.coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
          (Limits.colimit.isColimit (Discrete.functor X))).inv =
    finiteCoproduct.ι X a
[PROOFSTEP]
simp only [Limits.colimit.comp_coconePointUniqueUpToIso_inv, finiteCoproduct.cocone_pt, finiteCoproduct.cocone_ι,
  Discrete.natTrans_app]
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
a : α
⊢ Function.Injective ↑(ι X a)
[PROOFSTEP]
intro x y hxy
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
a : α
x y : (forget CompHaus).obj (X a)
hxy : ↑(ι X a) x = ↑(ι X a) y
⊢ x = y
[PROOFSTEP]
exact eq_of_heq (Sigma.ext_iff.mp hxy).2
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
π : (a : α) → X a ⟶ B
a : α
⊢ ∀ (x : (forget CompHaus).obj (X a)), ↑(desc X π) (↑(ι X a) x) = ↑(π a) x
[PROOFSTEP]
intro x
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
π : (a : α) → X a ⟶ B
a : α
x : (forget CompHaus).obj (X a)
⊢ ↑(desc X π) (↑(ι X a) x) = ↑(π a) x
[PROOFSTEP]
change (ι X a ≫ desc X π) _ = _
[GOAL]
α : Type
inst✝ : Fintype α
X : α → CompHaus
B : CompHaus
π : (a : α) → X a ⟶ B
a : α
x : (forget CompHaus).obj (X a)
⊢ ↑(ι X a ≫ desc X π) x = ↑(π a) x
[PROOFSTEP]
simp only [ι_desc]
  -- `elementwise` should work here, but doesn't


[GOAL]
X : Type u
Y Z : Profinite
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
Y Z : Profinite
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
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).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
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
let h : Ultrafilter X → Y := Ultrafilter.extend t
[GOAL]
case intro
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toCompHaus.toTop := Ultrafilter.extend t
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
have hh : Continuous h := continuous_ultrafilter_extend _
[GOAL]
case intro
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toCompHaus.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
use⟨h, hh⟩
[GOAL]
case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toCompHaus.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ ContinuousMap.mk h ≫ g = f
[PROOFSTEP]
apply Faithful.map_injective (F := forget Profinite)
[GOAL]
case h.a
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toCompHaus.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ (forget Profinite).map (ContinuousMap.mk h ≫ g) = (forget Profinite).map f
[PROOFSTEP]
simp only [ContinuousMap.coe_mk, coe_comp]
[GOAL]
case h.a
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toCompHaus.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ (forget Profinite).map (ContinuousMap.mk (Ultrafilter.extend (g' ∘ ↑f ∘ pure)) ≫ g) = (forget Profinite).map f
[PROOFSTEP]
convert
  denseRange_pure.equalizer (g.continuous.comp hh) f.continuous
    _
      -- Porting note: same fix as in `Topology.Category.CompHaus.Projective`
[GOAL]
case h.a
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toCompHaus.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
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toCompHaus.toTop := Ultrafilter.extend t
hh : Continuous h
g'' : C(↑Y.toCompHaus.toTop, ↑Z.toCompHaus.toTop) := g
⊢ (↑g ∘ h) ∘ pure = ↑f ∘ pure
[PROOFSTEP]
have : g'' ∘ g' = id := hg'.comp_eq_id
[GOAL]
case h.a
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ↑g
g' : (forget Profinite).obj Z → (forget Profinite).obj Y
hg' : Function.RightInverse g' ↑g
t : X → ↑Y.toCompHaus.toTop := g' ∘ ↑f ∘ pure
h : Ultrafilter X → ↑Y.toCompHaus.toTop := Ultrafilter.extend t
hh : Continuous h
g'' : C(↑Y.toCompHaus.toTop, ↑Z.toCompHaus.toTop) := g
this : ↑g'' ∘ g' = id
⊢ (↑g ∘ h) ∘ pure = ↑f ∘ pure
[PROOFSTEP]
rw [comp.assoc, ultrafilter_extend_extends, ← comp.assoc, this, comp.left_id]


[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
g : α →C₀ β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
zero_at_infty'✝ : Tendsto (ContinuousMap.mk toFun✝).toFun (cocompact α) (𝓝 0)
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, zero_at_infty' := zero_at_infty'✝ } =
    (fun f => f.toFun) g
⊢ { toContinuousMap := ContinuousMap.mk toFun✝, zero_at_infty' := zero_at_infty'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
zero_at_infty'✝¹ : Tendsto (ContinuousMap.mk toFun✝¹).toFun (cocompact α) (𝓝 0)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
zero_at_infty'✝ : Tendsto (ContinuousMap.mk toFun✝).toFun (cocompact α) (𝓝 0)
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, zero_at_infty' := zero_at_infty'✝ }
⊢ { toContinuousMap := ContinuousMap.mk toFun✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    { toContinuousMap := ContinuousMap.mk toFun✝, zero_at_infty' := zero_at_infty'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ↑f
⊢ Continuous f'
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ↑f
⊢ Continuous ↑f
[PROOFSTEP]
exact f.continuous_toFun
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ↑f
⊢ Tendsto (ContinuousMap.mk f').toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simp_rw [h]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ↑f
⊢ Tendsto (↑f) (cocompact α) (𝓝 0)
[PROOFSTEP]
exact f.zero_at_infty'
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : C(α, β)
⊢ Tendsto (ContinuousMap.mk ↑f).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : C(α, β)
⊢ (fun f => ↑f)
      ((fun f => { toContinuousMap := ContinuousMap.mk ↑f, zero_at_infty' := (_ : Tendsto (↑f) (cocompact α) (𝓝 0)) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : C(α, β)
a✝ : α
⊢ ↑((fun f => ↑f)
          ((fun f =>
              { toContinuousMap := ContinuousMap.mk ↑f, zero_at_infty' := (_ : Tendsto (↑f) (cocompact α) (𝓝 0)) })
            f))
      a✝ =
    ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : α →C₀ β
⊢ (fun f => { toContinuousMap := ContinuousMap.mk ↑f, zero_at_infty' := (_ : Tendsto (↑f) (cocompact α) (𝓝 0)) })
      ((fun f => ↑f) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : α →C₀ β
x✝ : α
⊢ ↑((fun f => { toContinuousMap := ContinuousMap.mk ↑f, zero_at_infty' := (_ : Tendsto (↑f) (cocompact α) (𝓝 0)) })
          ((fun f => ↑f) f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero β
inst✝² : ZeroAtInftyContinuousMapClass F α β
G : Type u_2
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
⊢ ∀ (f : G), Tendsto (↑f) (cocompact α) (𝓝 0)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : MulZeroClass β
inst✝ : ContinuousMul β
f g : α →C₀ β
⊢ Tendsto (↑f * ↑g).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [mul_zero] using (zero_at_infty f).mul (zero_at_infty g)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddZeroClass β
inst✝ : ContinuousAdd β
f g : α →C₀ β
⊢ Tendsto (↑f + ↑g).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [add_zero] using (zero_at_infty f).add (zero_at_infty g)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
f g : α →C₀ β
⊢ ↑(nsmulRec 0 f) = 0 • ↑f
[PROOFSTEP]
rw [nsmulRec, zero_smul, coe_zero]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
f g : α →C₀ β
n : ℕ
⊢ ↑(nsmulRec (n + 1) f) = (n + 1) • ↑f
[PROOFSTEP]
rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec n]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
f✝ g : α →C₀ β
n : ℕ
f : α →C₀ β
⊢ Tendsto (n • ↑f).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa [coe_nsmulRec] using zero_at_infty (nsmulRec n f)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f✝ g f : α →C₀ β
⊢ Tendsto (-↑f).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [neg_zero] using (zero_at_infty f).neg
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f✝ g✝ f g : α →C₀ β
⊢ Tendsto (↑f - ↑g).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [sub_zero] using (zero_at_infty f).sub (zero_at_infty g)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f g : α →C₀ β
n : ℕ
⊢ ↑(zsmulRec (Int.ofNat n) f) = Int.ofNat n • ↑f
[PROOFSTEP]
rw [zsmulRec, Int.ofNat_eq_coe, coe_nsmulRec, coe_nat_zsmul]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f g : α →C₀ β
n : ℕ
⊢ ↑(zsmulRec (Int.negSucc n) f) = Int.negSucc n • ↑f
[PROOFSTEP]
rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmulRec]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
f✝ g : α →C₀ β
n : ℤ
f : α →C₀ β
⊢ Tendsto (ContinuousMap.mk (n • ↑f)).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa using zero_at_infty (zsmulRec n f)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
x : α
inst✝³ : Zero β
R : Type u_2
inst✝² : Zero R
inst✝¹ : SMulWithZero R β
inst✝ : ContinuousConstSMul R β
r : R
f : α →C₀ β
⊢ Tendsto (ContinuousMap.mk (r • ↑f)).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa [smul_zero] using (zero_at_infty f).const_smul r
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : IsScalarTower R β β
r : R
f g : α →C₀ β
⊢ (r • f) • g = r • f • g
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : IsScalarTower R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ ↑((r • f) • g) x✝ = ↑(r • f • g) x✝
[PROOFSTEP]
simp only [smul_eq_mul, coe_mul, coe_smul, Pi.mul_apply, Pi.smul_apply]
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : IsScalarTower R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ r • ↑f x✝ * ↑g x✝ = r • (↑f x✝ * ↑g x✝)
[PROOFSTEP]
rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
⊢ r • f • g = f • r • g
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ ↑(r • f • g) x✝ = ↑(f • r • g) x✝
[PROOFSTEP]
simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : TopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
x✝ : α
⊢ r • (↑f x✝ * ↑g x✝) = ↑f x✝ * r • ↑g x✝
[PROOFSTEP]
rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
⊢ ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C
[PROOFSTEP]
obtain ⟨K : Set α, hK₁, hK₂⟩ :=
  mem_cocompact.mp (tendsto_def.mp (zero_at_infty (f : F)) _ (closedBall_mem_nhds (0 : β) zero_lt_one))
[GOAL]
case intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
⊢ ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C
[PROOFSTEP]
obtain ⟨C, hC⟩ := (hK₁.image (map_continuous f)).bounded.subset_ball (0 : β)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
⊢ ∃ C, ∀ (x y : α), dist (↑f x) (↑f y) ≤ C
[PROOFSTEP]
refine' ⟨max C 1 + max C 1, fun x y => _⟩
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x y : α
⊢ dist (↑f x) (↑f y) ≤ max C 1 + max C 1
[PROOFSTEP]
have : ∀ x, f x ∈ closedBall (0 : β) (max C 1) := by
  intro x
  by_cases hx : x ∈ K
  · exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)
  · exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x y : α
⊢ ∀ (x : α), ↑f x ∈ closedBall 0 (max C 1)
[PROOFSTEP]
intro x
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x✝ y x : α
⊢ ↑f x ∈ closedBall 0 (max C 1)
[PROOFSTEP]
by_cases hx : x ∈ K
[GOAL]
case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x✝ y x : α
hx : x ∈ K
⊢ ↑f x ∈ closedBall 0 (max C 1)
[PROOFSTEP]
exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)
[GOAL]
case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x✝ y x : α
hx : ¬x ∈ K
⊢ ↑f x ∈ closedBall 0 (max C 1)
[PROOFSTEP]
exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ↑f ⁻¹' closedBall 0 1
C : ℝ
hC : ↑f '' K ⊆ closedBall 0 C
x y : α
this : ∀ (x : α), ↑f x ∈ closedBall 0 (max C 1)
⊢ dist (↑f x) (↑f y) ≤ max C 1 + max C 1
[PROOFSTEP]
exact (dist_triangle (f x) 0 (f y)).trans (add_le_add (mem_closedBall.mp <| this x) (mem_closedBall'.mp <| this y))
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
h : toBcf f = toBcf g
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
h : toBcf f = toBcf g
x : α
⊢ ↑f x = ↑g x
[PROOFSTEP]
simpa only using FunLike.congr_fun h x
[GOAL]
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F✝ α β
C : ℝ
f✝ g : α →C₀ β
ι : Type u_2
F : ι → α →C₀ β
f : α →C₀ β
l : Filter ι
⊢ Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => ↑(F i)) (↑f) l
[PROOFSTEP]
simpa only [Metric.tendsto_nhds] using
  @BoundedContinuousFunction.tendsto_iff_tendstoUniformly _ _ _ _ _ (fun i => (F i).toBcf) f.toBcf l
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f g : α →C₀ β
⊢ Isometry toBcf
[PROOFSTEP]
tauto
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f g : α →C₀ β
⊢ IsClosed (range toBcf)
[PROOFSTEP]
refine' isClosed_iff_clusterPt.mpr fun f hf => _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ClusterPt f (𝓟 (range toBcf))
⊢ f ∈ range toBcf
[PROOFSTEP]
rw [clusterPt_principal_iff] at hf
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
⊢ f ∈ range toBcf
[PROOFSTEP]
have : Tendsto f (cocompact α) (𝓝 0) :=
  by
  refine' Metric.tendsto_nhds.mpr fun ε hε => _
  obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
  refine' (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp (eventually_of_forall fun x hx => _)
  calc
    dist (f x) 0 ≤ dist (g.toBcf x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
    _ < dist g.toBcf f + ε / 2 := (add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx)
    _ < ε := by simpa [add_halves ε] using add_lt_add_right (mem_ball.1 hg) (ε / 2)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
⊢ Tendsto (↑f) (cocompact α) (𝓝 0)
[PROOFSTEP]
refine' Metric.tendsto_nhds.mpr fun ε hε => _
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : α) in cocompact α, dist (↑f x) 0 < ε
[PROOFSTEP]
obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g✝ : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : toBcf g ∈ ball f (ε / 2)
⊢ ∀ᶠ (x : α) in cocompact α, dist (↑f x) 0 < ε
[PROOFSTEP]
refine' (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp (eventually_of_forall fun x hx => _)
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g✝ : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : toBcf g ∈ ball f (ε / 2)
x : α
hx : dist (↑g x) 0 < ε / 2
⊢ dist (↑f x) 0 < ε
[PROOFSTEP]
calc
  dist (f x) 0 ≤ dist (g.toBcf x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
  _ < dist g.toBcf f + ε / 2 := (add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx)
  _ < ε := by simpa [add_halves ε] using add_lt_add_right (mem_ball.1 hg) (ε / 2)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g✝ : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : toBcf g ∈ ball f (ε / 2)
x : α
hx : dist (↑g x) 0 < ε / 2
⊢ dist (toBcf g) f + ε / 2 < ε
[PROOFSTEP]
simpa [add_halves ε] using add_lt_add_right (mem_ball.1 hg) (ε / 2)
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : MetricSpace β
inst✝¹ : Zero β
inst✝ : ZeroAtInftyContinuousMapClass F α β
C : ℝ
f✝ g : α →C₀ β
f : α →ᵇ β
hf : ∀ (U : Set (α →ᵇ β)), U ∈ 𝓝 f → Set.Nonempty (U ∩ range toBcf)
this : Tendsto (↑f) (cocompact α) (𝓝 0)
⊢ f ∈ range toBcf
[PROOFSTEP]
exact ⟨⟨f.toContinuousMap, this⟩, rfl⟩
[GOAL]
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C₀ β
⊢ Tendsto (ContinuousMap.mk fun x => star (↑f x)).toFun (cocompact α) (𝓝 0)
[PROOFSTEP]
simpa only [star_zero] using (continuous_star.tendsto (0 : β)).comp (zero_at_infty f)


[GOAL]
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
suffices Epi f ↔ Epi ((forget TopCat).map f)
  by
  rw [this, CategoryTheory.epi_iff_surjective]
  rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [this, CategoryTheory.epi_iff_surjective]
[GOAL]
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Function.Surjective ((forget TopCat).map f) ↔ Function.Surjective ↑f
[PROOFSTEP]
rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Epi ((forget TopCat).map f)
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)
[PROOFSTEP]
intro
[GOAL]
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget TopCat).map f)
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Epi ((forget TopCat).map f) → Epi f
[PROOFSTEP]
apply Functor.epi_of_epi_map
[GOAL]
X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
suffices Mono f ↔ Mono ((forget TopCat).map f)
  by
  rw [this, CategoryTheory.mono_iff_injective]
  rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
rw [this, CategoryTheory.mono_iff_injective]
[GOAL]
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Function.Injective ((forget TopCat).map f) ↔ Function.Injective ↑f
[PROOFSTEP]
rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Mono ((forget TopCat).map f)
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Mono f → Mono ((forget TopCat).map f)
[PROOFSTEP]
intro
[GOAL]
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Mono f
⊢ Mono ((forget TopCat).map f)
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Mono ((forget TopCat).map f) → Mono f
[PROOFSTEP]
apply Functor.mono_of_mono_map


[GOAL]
X : Profinite
X✝ Y✝ Z✝ : DiscreteQuotient ↑X.toCompHaus.toTop
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
          map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
      (x✝¹ ≫ x✝) =
    { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
            map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
        x✝¹ ≫
      { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
            map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
X : Profinite
X✝ Y✝ Z✝ : DiscreteQuotient ↑X.toCompHaus.toTop
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ :
  ↑({ obj := fun S => FintypeCat.of (Quotient S.toSetoid),
          map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.obj
      X✝)
⊢ { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
          map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
      (x✝² ≫ x✝¹) x✝ =
    ({ obj := fun S => FintypeCat.of (Quotient S.toSetoid),
              map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
          x✝² ≫
        { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
              map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
          x✝¹)
      x✝
[PROOFSTEP]
aesop_cat
[GOAL]
X : Profinite
⊢ Function.Bijective ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X))
[PROOFSTEP]
refine' ⟨fun a b h => _, fun a => _⟩
[GOAL]
case refine'_1
X : Profinite
a b : (forget Profinite).obj (asLimitCone X).pt
h :
  ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a =
    ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b
⊢ a = b
[PROOFSTEP]
refine' DiscreteQuotient.eq_of_forall_proj_eq fun S => _
[GOAL]
case refine'_1
X : Profinite
a b : (forget Profinite).obj (asLimitCone X).pt
h :
  ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a =
    ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b
S : DiscreteQuotient ((forget Profinite).obj (asLimitCone X).pt)
⊢ DiscreteQuotient.proj S a = DiscreteQuotient.proj S b
[PROOFSTEP]
apply_fun fun f : (limitCone X.diagram).pt => f.val S at h
[GOAL]
case refine'_1
X : Profinite
a b : (forget Profinite).obj (asLimitCone X).pt
S : DiscreteQuotient ((forget Profinite).obj (asLimitCone X).pt)
h :
  ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a) S =
    ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b) S
⊢ DiscreteQuotient.proj S a = DiscreteQuotient.proj S b
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
⊢ ∃ a_1, ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a_1 = a
[PROOFSTEP]
obtain ⟨b, hb⟩ := DiscreteQuotient.exists_of_compat (fun S => a.val S) fun _ _ h => a.prop (homOfLE h)
[GOAL]
case refine'_2.intro
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
⊢ ∃ a_1, ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a_1 = a
[PROOFSTEP]
use b
[GOAL]
case h
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
⊢ ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b = a
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case h.a
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
⊢ ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b) = ↑a
[PROOFSTEP]
apply funext
[GOAL]
case h.a.h
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
⊢ ∀ (x : DiscreteQuotient ↑X.toCompHaus.toTop),
    ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b) x = ↑a x
[PROOFSTEP]
rintro S
[GOAL]
case h.a.h
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
S : DiscreteQuotient ↑X.toCompHaus.toTop
⊢ ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b) S = ↑a S
[PROOFSTEP]
apply hb


[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
⊢ fst f g ≫ f = snd f g ≫ g
[PROOFSTEP]
ext ⟨_, h⟩
[GOAL]
case w.mk
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
val✝ : ↑X.toCompHaus.toTop × ↑Y.toCompHaus.toTop
h : val✝ ∈ {xy | ↑f xy.fst = ↑g xy.snd}
⊢ ↑(fst f g ≫ f) { val := val✝, property := h } = ↑(snd f g ≫ g) { val := val✝, property := h }
[PROOFSTEP]
exact h
[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
z : ↑Z.toCompHaus.toTop
⊢ (↑a z, ↑b z) ∈ {xy | ↑f xy.fst = ↑g xy.snd}
[PROOFSTEP]
apply_fun (· z) at w
[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a : Z ⟶ X
b : Z ⟶ Y
z : ↑Z.toCompHaus.toTop
w : ↑(a ≫ f) z = ↑(b ≫ g) z
⊢ (↑a z, ↑b z) ∈ {xy | ↑f xy.fst = ↑g xy.snd}
[PROOFSTEP]
exact w
[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ Continuous fun z => { val := (↑a z, ↑b z), property := (_ : ↑(a ≫ f) z = ↑(b ≫ g) z) }
[PROOFSTEP]
apply Continuous.subtype_mk
[GOAL]
case h
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ Continuous fun x => (↑a x, ↑b x)
[PROOFSTEP]
rw [continuous_prod_mk]
[GOAL]
case h
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ (Continuous fun x => ↑a x) ∧ Continuous fun x => ↑b x
[PROOFSTEP]
exact ⟨a.continuous, b.continuous⟩
[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
⊢ a = b
[PROOFSTEP]
ext z
[GOAL]
case w
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : (forget Profinite).obj Z
⊢ ↑a z = ↑b z
[PROOFSTEP]
apply_fun (· z) at hfst hsnd
[GOAL]
case w
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑a z = ↑b z
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case w.a
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑(↑a z) = ↑(↑b z)
[PROOFSTEP]
apply Prod.ext
[GOAL]
case w.a.h₁
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).fst = (↑(↑b z)).fst
[PROOFSTEP]
exact hfst
[GOAL]
case w.a.h₂
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).snd = (↑(↑b z)).snd
[PROOFSTEP]
exact hsnd
[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.fst f g = (pullbackIsoPullback f g).hom ≫ Limits.pullback.fst
[PROOFSTEP]
dsimp [pullbackIsoPullback]
[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.fst f g =
    (Limits.IsLimit.conePointUniqueUpToIso (pullback.isLimit f g) (Limits.limit.isLimit (Limits.cospan f g))).hom ≫
      Limits.pullback.fst
[PROOFSTEP]
simp only [Limits.limit.conePointUniqueUpToIso_hom_comp, pullback.cone_pt, pullback.cone_π]
[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.snd f g = (pullbackIsoPullback f g).hom ≫ Limits.pullback.snd
[PROOFSTEP]
dsimp [pullbackIsoPullback]
[GOAL]
X Y B : Profinite
f : X ⟶ B
g : Y ⟶ B
⊢ pullback.snd f g =
    (Limits.IsLimit.conePointUniqueUpToIso (pullback.isLimit f g) (Limits.limit.isLimit (Limits.cospan f g))).hom ≫
      Limits.pullback.snd
[PROOFSTEP]
simp only [Limits.limit.conePointUniqueUpToIso_hom_comp, pullback.cone_pt, pullback.cone_π]
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
e : (a : α) → X a ⟶ B
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
apply continuous_sigma
[GOAL]
case hf
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
e : (a : α) → X a ⟶ B
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
intro a
[GOAL]
case hf
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
e : (a : α) → X a ⟶ B
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
exact (e a).continuous
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g
[PROOFSTEP]
ext ⟨a, x⟩
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toCompHaus.toTop
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
specialize h a
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
apply_fun (· x) at h
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
exact h
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), NatTrans.app (cocone X).ι j ≫ m = NatTrans.app s.ι j
a : α
⊢ ι (fun a => X a) a ≫ m = ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s
[PROOFSTEP]
specialize hm ⟨a⟩
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
hm : NatTrans.app (cocone X).ι { as := a } ≫ m = NatTrans.app s.ι { as := a }
⊢ ι (fun a => X a) a ≫ m = ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s
[PROOFSTEP]
ext t
[GOAL]
case w
α : Type
inst✝ : Fintype α
X : α → Profinite
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
hm : NatTrans.app (cocone X).ι { as := a } ≫ m = NatTrans.app s.ι { as := a }
t : (forget Profinite).obj (X a)
⊢ ↑(ι (fun a => X a) a ≫ m) t =
    ↑(ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s) t
[PROOFSTEP]
apply_fun (· t) at hm
[GOAL]
case w
α : Type
inst✝ : Fintype α
X : α → Profinite
s : Limits.Cocone (Discrete.functor X)
m : (cocone X).pt ⟶ s.pt
a : α
t : (forget Profinite).obj (X a)
hm : ↑(NatTrans.app (cocone X).ι { as := a } ≫ m) t = ↑(NatTrans.app s.ι { as := a }) t
⊢ ↑(ι (fun a => X a) a ≫ m) t =
    ↑(ι (fun a => X a) a ≫ (fun s => desc (fun a => X a) fun a => NatTrans.app s.ι { as := a }) s) t
[PROOFSTEP]
exact hm
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
a : α
⊢ Limits.Sigma.ι X a ≫ (coproductIsoCoproduct X).inv = finiteCoproduct.ι X a
[PROOFSTEP]
simp only [coproductIsoCoproduct, Limits.colimit.comp_coconePointUniqueUpToIso_inv, finiteCoproduct.cocone_pt,
  finiteCoproduct.cocone_ι, Discrete.natTrans_app]
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
a : α
⊢ Function.Injective ↑(ι X a)
[PROOFSTEP]
intro x y hxy
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
a : α
x y : (forget Profinite).obj (X a)
hxy : ↑(ι X a) x = ↑(ι X a) y
⊢ x = y
[PROOFSTEP]
exact eq_of_heq (Sigma.ext_iff.mp hxy).2
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
π : (a : α) → X a ⟶ B
a : α
⊢ ∀ (x : (forget Profinite).obj (X a)), ↑(desc X π) (↑(ι X a) x) = ↑(π a) x
[PROOFSTEP]
intro x
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
π : (a : α) → X a ⟶ B
a : α
x : (forget Profinite).obj (X a)
⊢ ↑(desc X π) (↑(ι X a) x) = ↑(π a) x
[PROOFSTEP]
change (ι X a ≫ desc X π) _ = _
[GOAL]
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
π : (a : α) → X a ⟶ B
a : α
x : (forget Profinite).obj (X a)
⊢ ↑(ι X a ≫ desc X π) x = ↑(π a) x
[PROOFSTEP]
simp only [ι_desc]