J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
let D := limitConeInfi F
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
let E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit _)
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
have hE : Inducing E.hom := (TopCat.homeoOfIso E).inducing
case h.e'_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
⊢ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V} =
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
          S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
convert isTopologicalBasis_iInf hT fun j (x : D.pt) => D.π.app j x using 1
case h.e'_3.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V} ↔
    U0 ∈
      {S |
        ∃ U F_1,
          (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
            S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
case h.e'_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
⊢ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V} =
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
          S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
ext U0
case h.e'_3.h.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V} →
    U0 ∈
      {S |
        ∃ U F_1,
          (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
            S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}

case h.e'_3.h.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈
      {S |
        ∃ U F_1,
          (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
            S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i} →
    U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
case h.e'_3.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V} ↔
    U0 ∈
      {S |
        ∃ U F_1,
          (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
            S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
constructor
case h.e'_3.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
⊢ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V} =
    Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
convert this.inducing hE
case h.e'_3.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V} ↔
    U0 ∈ Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
case h.e'_3.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
⊢ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V} =
    Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
ext U0
case h.e'_3.h.h.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V} →
    U0 ∈ Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}

case h.e'_3.h.h.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V} →
    U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
case h.e'_3.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V} ↔
    U0 ∈ Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
constructor
case h.e'_3.h.h.mp.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ (forget TopCat).map (C.π.app j) ⁻¹' V ∈
    Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
case h.e'_3.h.h.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V} →
    U0 ∈ Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
rintro ⟨j, V, hV, rfl⟩
no goals
case h.e'_3.h.h.mp.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ (forget TopCat).map (C.π.app j) ⁻¹' V ∈
    Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
refine' ⟨D.π.app j ⁻¹' V, ⟨j, V, hV, rfl⟩, rfl⟩
case h.e'_3.h.h.mpr.intro.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ (forget TopCat).map E.hom ⁻¹' ((forget TopCat).map (D.π.app j) ⁻¹' V) ∈
    {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
case h.e'_3.h.h.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ Set.preimage ((forget TopCat).map E.hom) '' {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V} →
    U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
rintro ⟨W, ⟨j, V, hV, rfl⟩, rfl⟩
no goals
case h.e'_3.h.h.mpr.intro.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ (forget TopCat).map E.hom ⁻¹' ((forget TopCat).map (D.π.app j) ⁻¹' V) ∈
    {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (C.π.app j) ⁻¹' V}
refine' ⟨j, V, hV, rfl⟩
case h.e'_3.h.mp.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ (forget TopCat).map (D.π.app j) ⁻¹' V ∈
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
          S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
case h.e'_3.h.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V} →
    U0 ∈
      {S |
        ∃ U F_1,
          (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
            S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
rintro ⟨j, V, hV, rfl⟩
case h.e'_3.h.mp.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
⊢ (forget TopCat).map (D.π.app j) ⁻¹' V ∈
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
          S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
case h.e'_3.h.mp.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ (forget TopCat).map (D.π.app j) ⁻¹' V ∈
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
          S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
let U : ∀ i, Set (F.obj i) := fun i =>
  if h : i = j then by
    rw [h]
    exact V
  else Set.univ
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
⊢ ∀ (i : J), i ∈ {j} → U i ∈ T i

case h.e'_3.h.mp.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
⊢ (forget TopCat).map (D.π.app j) ⁻¹' V = ⋂ (i : J) (_ : i ∈ {j}), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
case h.e'_3.h.mp.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
⊢ (forget TopCat).map (D.π.app j) ⁻¹' V ∈
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
          S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i}
refine' ⟨U, {j}, _, _⟩
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
i : J
h : i = j
⊢ Set ↑(F.obj j)
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
i : J
h : i = j
⊢ Set ↑(F.obj i)
rw [h]
no goals
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
i : J
h : i = j
⊢ Set ↑(F.obj j)
exact V
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
i : J
h : i ∈ {j}
⊢ U i ∈ T i
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
⊢ ∀ (i : J), i ∈ {j} → U i ∈ T i
rintro i h
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
i : J
h : i = j
⊢ U i ∈ T i
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
i : J
h : i ∈ {j}
⊢ U i ∈ T i
rw [Finset.mem_singleton] at h
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
i : J
h : i = j
⊢ (if h : i = j then cast (_ : Set ↑(F.obj j) = Set ↑(F.obj i)) V else Set.univ) ∈ T i
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
i : J
h : i = j
⊢ U i ∈ T i
dsimp
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
i : J
h : i = j
⊢ cast (_ : Set ↑(F.obj j) = Set ↑(F.obj i)) V ∈ T i
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
i : J
h : i = j
⊢ (if h : i = j then cast (_ : Set ↑(F.obj j) = Set ↑(F.obj i)) V else Set.univ) ∈ T i
rw [dif_pos h]
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
i : J
V : Set ↑(F.obj i)
hV : V ∈ T i
U : (i : J) → Set ↑(F.obj i) :=
  fun i_1 => if h : i_1 = i then Eq.mpr (_ : Set ↑(F.obj i_1) = Set ↑(F.obj i)) V else Set.univ
⊢ cast (_ : Set ↑(F.obj i) = Set ↑(F.obj i)) V ∈ T i
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
i : J
h : i = j
⊢ cast (_ : Set ↑(F.obj j) = Set ↑(F.obj i)) V ∈ T i
subst h
no goals
case h.e'_3.h.mp.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
i : J
V : Set ↑(F.obj i)
hV : V ∈ T i
U : (i : J) → Set ↑(F.obj i) :=
  fun i_1 => if h : i_1 = i then Eq.mpr (_ : Set ↑(F.obj i_1) = Set ↑(F.obj i)) V else Set.univ
⊢ cast (_ : Set ↑(F.obj i) = Set ↑(F.obj i)) V ∈ T i
exact hV
case h.e'_3.h.mp.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
⊢ (forget TopCat).map ((limitConeInfi F).π.app j) ⁻¹' V =
    ⋂ (i : J) (_ : i ∈ {j}),
      (fun x => (forget TopCat).map ((limitConeInfi F).π.app i) x) ⁻¹'
        if h : i = j then cast (_ : Set ↑(F.obj j) = Set ↑(F.obj i)) V else Set.univ
case h.e'_3.h.mp.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
⊢ (forget TopCat).map (D.π.app j) ⁻¹' V = ⋂ (i : J) (_ : i ∈ {j}), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
dsimp
no goals
case h.e'_3.h.mp.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i => if h : i = j then Eq.mpr (_ : Set ↑(F.obj i) = Set ↑(F.obj j)) V else Set.univ
⊢ (forget TopCat).map ((limitConeInfi F).π.app j) ⁻¹' V =
    ⋂ (i : J) (_ : i ∈ {j}),
      (fun x => (forget TopCat).map ((limitConeInfi F).π.app i) x) ⁻¹'
        if h : i = j then cast (_ : Set ↑(F.obj j) = Set ↑(F.obj i)) V else Set.univ
simp
case h.e'_3.h.mpr.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
case h.e'_3.h.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈
      {S |
        ∃ U F_1,
          (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧
            S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i} →
    U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
rintro ⟨U, G, h1, h2⟩
case h.e'_3.h.mpr.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
case h.e'_3.h.mpr.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
obtain ⟨j, hj⟩ := IsCofiltered.inf_objs_exists G
case h.e'_3.h.mpr.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
case h.e'_3.h.mpr.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
let g : ∀ (e) (_he : e ∈ G), j ⟶ e := fun _ he => (hj he).some
case h.e'_3.h.mpr.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
case h.e'_3.h.mpr.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
let Vs : J → Set (F.obj j) := fun e => if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ
case h.e'_3.h.mpr.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
case h.e'_3.h.mpr.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
let V : Set (F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ V ∈ T j

case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ U0 = (forget TopCat).map (D.π.app j) ⁻¹' V
case h.e'_3.h.mpr.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = (forget TopCat).map (D.π.app j) ⁻¹' V}
refine' ⟨j, V, _, _⟩
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
⊢ ∀ (e : J), e ∈ G → Vs e ∈ T j
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
⊢ V ∈ T j
refine' this _ _ _ (univ _) (inter _) _
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
e : J
he : e ∈ G
⊢ Vs e ∈ T j
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
⊢ ∀ (e : J), e ∈ G → Vs e ∈ T j
intro e he
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
e : J
he : e ∈ G
⊢ (if h : e ∈ G then (forget TopCat).map (F.map (Nonempty.some (_ : Nonempty (j ⟶ e)))) ⁻¹' U e else Set.univ) ∈ T j
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
e : J
he : e ∈ G
⊢ Vs e ∈ T j
dsimp
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
e : J
he : e ∈ G
⊢ (forget TopCat).map (F.map (Nonempty.some (_ : Nonempty (j ⟶ e)))) ⁻¹' U e ∈ T j
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
e : J
he : e ∈ G
⊢ (if h : e ∈ G then (forget TopCat).map (F.map (Nonempty.some (_ : Nonempty (j ⟶ e)))) ⁻¹' U e else Set.univ) ∈ T j
rw [dif_pos he]
no goals
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
e : J
he : e ∈ G
⊢ (forget TopCat).map (F.map (Nonempty.some (_ : Nonempty (j ⟶ e)))) ⁻¹' U e ∈ T j
exact compat j e (g e he) (U e) (h1 e he)
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
E : Finset J
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
intro S E
case empty
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ ∅ → P e ∈ S) → (⋂ (e : J) (_ : e ∈ ∅), P e) ∈ S

case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ insert a E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ insert a E), P e) ∈ S
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
E : Finset J
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
induction' E using Finset.induction_on with a E _ hh1
case empty
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
P : J → Set ↑(F.obj j)
he : Set.univ ∈ S
x✝ : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
⊢ (∀ (e : J), e ∈ ∅ → P e ∈ S) → (⋂ (e : J) (_ : e ∈ ∅), P e) ∈ S
case empty
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ ∅ → P e ∈ S) → (⋂ (e : J) (_ : e ∈ ∅), P e) ∈ S
intro P he _
no goals
case empty
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
P : J → Set ↑(F.obj j)
he : Set.univ ∈ S
x✝ : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
⊢ (∀ (e : J), e ∈ ∅ → P e ∈ S) → (⋂ (e : J) (_ : e ∈ ∅), P e) ∈ S
simpa
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J), e ∈ insert a E → hh2 e ∈ S
⊢ (⋂ (e : J) (_ : e ∈ insert a E), hh2 e) ∈ S
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ insert a E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ insert a E), P e) ∈ S
intro hh2 hh3 hh4 hh5
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J), e ∈ insert a E → hh2 e ∈ S
⊢ (hh2 a ∩ ⋂ (x : J) (_ : x ∈ E), hh2 x) ∈ S
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J), e ∈ insert a E → hh2 e ∈ S
⊢ (⋂ (e : J) (_ : e ∈ insert a E), hh2 e) ∈ S
rw [Finset.set_biInter_insert]
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J), e ∈ insert a E → hh2 e ∈ S
⊢ ∀ (e : J), e ∈ E → hh2 e ∈ S
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J), e ∈ insert a E → hh2 e ∈ S
⊢ (hh2 a ∩ ⋂ (x : J) (_ : x ∈ E), hh2 x) ∈ S
refine' hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 _)
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J), e ∈ insert a E → hh2 e ∈ S
e : J
he : e ∈ E
⊢ hh2 e ∈ S
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J), e ∈ insert a E → hh2 e ∈ S
⊢ ∀ (e : J), e ∈ E → hh2 e ∈ S
intro e he
no goals
case insert
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E✝.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
a✝ : ¬a ∈ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) →
        (∀ (e : J), e ∈ E → P e ∈ S) → (⋂ (e : J) (_ : e ∈ E), P e) ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ (e : J), e ∈ insert a E → hh2 e ∈ S
e : J
he : e ∈ E
⊢ hh2 e ∈ S
exact hh5 e (Finset.mem_insert_of_mem he)
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ (⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i) = (forget TopCat).map (D.π.app j) ⁻¹' V
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ U0 = (forget TopCat).map (D.π.app j) ⁻¹' V
rw [h2]
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ (⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i) =
    (forget TopCat).map (D.π.app j) ⁻¹' ⋂ (e : J) (_ : e ∈ G), Vs e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ (⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i) = (forget TopCat).map (D.π.app j) ⁻¹' V
change _ = (D.π.app j)⁻¹' ⋂ (e : J) (_ : e ∈ G), Vs e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ (⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i) =
    ⋂ (i : J), (forget TopCat).map (D.π.app j) ⁻¹' ⋂ (_ : i ∈ G), Vs i
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ (⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i) =
    (forget TopCat).map (D.π.app j) ⁻¹' ⋂ (e : J) (_ : e ∈ G), Vs e
rw [Set.preimage_iInter]
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ (fun i => ⋂ (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i) = fun i =>
    (forget TopCat).map (D.π.app j) ⁻¹' ⋂ (_ : i ∈ G), Vs i
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ (⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i) =
    ⋂ (i : J), (forget TopCat).map (D.π.app j) ⁻¹' ⋂ (_ : i ∈ G), Vs i
apply congrArg
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
⊢ (⋂ (_ : e ∈ G), (fun x => (forget TopCat).map (D.π.app e) x) ⁻¹' U e) =
    (forget TopCat).map (D.π.app j) ⁻¹' ⋂ (_ : e ∈ G), Vs e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ (fun i => ⋂ (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i) = fun i =>
    (forget TopCat).map (D.π.app j) ⁻¹' ⋂ (_ : i ∈ G), Vs i
ext1 e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
⊢ (⋂ (_ : e ∈ G), (fun x => (forget TopCat).map (D.π.app e) x) ⁻¹' U e) =
    ⋂ (_ : e ∈ G), (forget TopCat).map (D.π.app j) ⁻¹' Vs e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
⊢ (⋂ (_ : e ∈ G), (fun x => (forget TopCat).map (D.π.app e) x) ⁻¹' U e) =
    (forget TopCat).map (D.π.app j) ⁻¹' ⋂ (_ : e ∈ G), Vs e
erw [Set.preimage_iInter]
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
⊢ (fun x => (fun x => (forget TopCat).map (D.π.app e) x) ⁻¹' U e) = fun i => (forget TopCat).map (D.π.app j) ⁻¹' Vs e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
⊢ (⋂ (_ : e ∈ G), (fun x => (forget TopCat).map (D.π.app e) x) ⁻¹' U e) =
    ⋂ (_ : e ∈ G), (forget TopCat).map (D.π.app j) ⁻¹' Vs e
apply congrArg
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ (fun x => (forget TopCat).map (D.π.app e) x) ⁻¹' U e = (forget TopCat).map (D.π.app j) ⁻¹' Vs e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
⊢ (fun x => (fun x => (forget TopCat).map (D.π.app e) x) ⁻¹' U e) = fun i => (forget TopCat).map (D.π.app j) ⁻¹' Vs e
ext1 he
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ (forget TopCat).map (D.π.app e) ⁻¹' U e =
    (forget TopCat).map (D.π.app j) ⁻¹' if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ (fun x => (forget TopCat).map (D.π.app e) x) ⁻¹' U e = (forget TopCat).map (D.π.app j) ⁻¹' Vs e
change (forget TopCat).map (D.π.app e)⁻¹' U e =
  (forget TopCat).map (D.π.app j) ⁻¹' if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ (forget TopCat).map (D.π.app e) ⁻¹' U e =
    (forget TopCat).map (F.map (g e he)) ∘ (forget TopCat).map (D.π.app j) ⁻¹' U e
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ (forget TopCat).map (D.π.app e) ⁻¹' U e =
    (forget TopCat).map (D.π.app j) ⁻¹' if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
rw [dif_pos he, ← Set.preimage_comp]
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ Set.preimage ((forget TopCat).map (D.π.app e)) =
    Set.preimage ((forget TopCat).map (F.map (g e he)) ∘ (forget TopCat).map (D.π.app j))
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ (forget TopCat).map (D.π.app e) ⁻¹' U e =
    (forget TopCat).map (F.map (g e he)) ∘ (forget TopCat).map (D.π.app j) ⁻¹' U e
apply congrFun
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ (forget TopCat).map (D.π.app e) = (forget TopCat).map (F.map (g e he)) ∘ (forget TopCat).map (D.π.app j)
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ Set.preimage ((forget TopCat).map (D.π.app e)) =
    Set.preimage ((forget TopCat).map (F.map (g e he)) ∘ (forget TopCat).map (D.π.app j))
apply congrArg
no goals
case h.e'_3.h.mpr.intro.intro.intro.intro.refine'_2.h.h.h.h.h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j) (V : Set ↑(F.obj j)), V ∈ T j → (forget TopCat).map (F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ((forget TopCat).map E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ (i : J), i ∈ G → U i ∈ T i
h2 : U0 = ⋂ (i : J) (_ : i ∈ G), (fun x => (forget TopCat).map (D.π.app i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he => Nonempty.some (_ : Nonempty (j ⟶ x))
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then (forget TopCat).map (F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
e : J
he : e ∈ G
⊢ (forget TopCat).map (D.π.app e) = (forget TopCat).map (F.map (g e he)) ∘ (forget TopCat).map (D.π.app j)
rw [←coe_comp, D.w]