-- Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean
theorem isTopologicalBasis_cofiltered_limit (hC : IsLimit C) (T : ∀ j, Set (Set (F.obj j)))
    (hT : ∀ j, IsTopologicalBasis (T j)) (univ : ∀ i : J, Set.univ ∈ T i)
    (inter : ∀ (i) (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)) (_hV : V ∈ T j), F.map f ⁻¹' V ∈ T i) :
    IsTopologicalBasis
      {U : Set C.pt | ∃ (j : _) (V : Set (F.obj j)), V ∈ T j ∧ U = C.π.app j ⁻¹' V}

Proof state:
case h.e'_3.h.mpr
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
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 ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit F)
hE : IsInducing ⇑(ConcreteCategory.hom E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈ {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x => (ConcreteCategory.hom (D.π.app i)) x) ⁻¹' U i} →
    U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' V}

Tactic:
rintro ⟨U, G, h1, h2⟩

Result:
case h.e'_3.h.mpr.intro.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
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 ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit F)
hE : IsInducing ⇑(ConcreteCategory.hom E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x => (ConcreteCategory.hom (D.π.app i)) x) ⁻¹' U i
⊢ U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' V}

Proof state:
case h.e'_3.h
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
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 ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit F)
hE : IsInducing ⇑(ConcreteCategory.hom E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' V} ↔
    U0 ∈ {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x => (ConcreteCategory.hom (D.π.app i)) x) ⁻¹' U i}

Tactic:
constructor

Result:
case h.e'_3.h.mp
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
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 ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit F)
hE : IsInducing ⇑(ConcreteCategory.hom E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' V} →
    U0 ∈ {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x => (ConcreteCategory.hom (D.π.app i)) x) ⁻¹' U i}

case h.e'_3.h.mpr
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
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 ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit F)
hE : IsInducing ⇑(ConcreteCategory.hom E.hom)
U0 : Set ↑D.pt
⊢ U0 ∈ {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x => (ConcreteCategory.hom (D.π.app i)) x) ⁻¹' U i} →
    U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' V}

Proof state:
case h.e'_3.h.mpr.intro.intro.intro.intro.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
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 ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit F)
hE : IsInducing ⇑(ConcreteCategory.hom E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x => (ConcreteCategory.hom (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 => ⋯.some
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj 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 ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
e : J
he : e ∈ G
⊢ (if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ) ∈ T j

Tactic:
rw [dif_pos he]

Result:
case h.e'_3.h.mpr.intro.intro.intro.intro.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
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 ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit F)
hE : IsInducing ⇑(ConcreteCategory.hom E.hom)
U0 : Set ↑D.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x => (ConcreteCategory.hom (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 => ⋯.some
Vs : J → Set ↑(F.obj j) := fun e => if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj 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 ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
e : J
he : e ∈ G
⊢ ⇑(ConcreteCategory.hom (F.map (g e he))) ⁻¹' U e ∈ T j