-- 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.intro.intro.intro.intro.refine_2.h.h.h.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
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
e : J
he : e ∈ G
⊢ ⇑(ConcreteCategory.hom (D.π.app e)) ⁻¹' U e =
    ⇑(ConcreteCategory.hom (F.map (g e he))) ∘ ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' U e

Tactic:
apply congrFun

Result:
case h.e'_3.h.mpr.intro.intro.intro.intro.refine_2.h.h.h.h.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
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
e : J
he : e ∈ G
⊢ Set.preimage ⇑(ConcreteCategory.hom (D.π.app e)) =
    Set.preimage (⇑(ConcreteCategory.hom (F.map (g e he))) ∘ ⇑(ConcreteCategory.hom (D.π.app j)))

Proof state:
case h.e'_3.h.mpr.intro.intro.intro.intro.refine_2.h.h.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
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
e : J
⊢ (fun x => (fun x => (ConcreteCategory.hom (D.π.app e)) x) ⁻¹' U e) = fun i =>
    ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' Vs e

Tactic:
ext1 he

Result:
case h.e'_3.h.mpr.intro.intro.intro.intro.refine_2.h.h.h.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
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
e : J
he : e ∈ G
⊢ (fun x => (ConcreteCategory.hom (D.π.app e)) x) ⁻¹' U e = ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' Vs e

Proof state:
case h.e'_3.h.mp.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)
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 ⋯.mpr V else Set.univ
⊢ ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' V ∈
    {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:
refine ⟨U, {j}, ?_, ?_⟩

Result:
case h.e'_3.h.mp.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)
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 ⋯.mpr V else Set.univ
⊢ ∀ i ∈ {j}, U i ∈ T i

case h.e'_3.h.mp.intro.intro.intro.refine_2
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)
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 ⋯.mpr V else Set.univ
⊢ ⇑(ConcreteCategory.hom (D.π.app j)) ⁻¹' V = ⋂ i ∈ {j}, (fun x => (ConcreteCategory.hom (D.π.app i)) x) ⁻¹' U i