[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V}
[PROOFSTEP]
classical
  -- The limit cone for `F` whose topology is defined as an infimum.
let D := limitConeInfi F
let E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit _)
have hE : Inducing E.hom := (TopCat.homeoOfIso E).inducing
suffices IsTopologicalBasis {U : Set D.pt | ∃ (j : _) (V : Set (F.obj j)), V ∈ T j ∧ U = D.π.app j ⁻¹' V}
  by
  convert this.inducing hE
  ext U0
  constructor
  · rintro ⟨j, V, hV, rfl⟩
    refine' ⟨D.π.app j ⁻¹' V, ⟨j, V, hV, rfl⟩, rfl⟩
  · rintro ⟨W, ⟨j, V, hV, rfl⟩, rfl⟩
    refine'
      ⟨j, V, hV, rfl⟩
        -- Using `D`, we can apply the characterization of the topological basis of a
          -- topology defined as an infimum...
convert isTopologicalBasis_iInf hT fun j (x : D.pt) => D.π.app j x using 1
ext U0
constructor
· rintro ⟨j, V, hV, rfl⟩
  let U : ∀ i, Set (F.obj i) := fun i => if h : i = j then by rw [h]; exact V else Set.univ
  refine' ⟨U, { j }, _, _⟩
  · rintro i h
    rw [Finset.mem_singleton] at h
    dsimp
    rw [dif_pos h]
    subst h
    exact hV
  · dsimp
    simp
· rintro ⟨U, G, h1, h2⟩
  obtain ⟨j, hj⟩ := IsCofiltered.inf_objs_exists G
  let g : ∀ (e) (_he : e ∈ G), j ⟶ e := fun _ he => (hj he).some
  let Vs : J → Set (F.obj j) := fun e => if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ
  let V : Set (F.obj j) := ⋂ (e : J) (_he : e ∈ G), Vs e
  refine' ⟨j, V, _, _⟩
  ·
    -- An intermediate claim used to apply induction along `G : Finset J` later on.
    have :
      ∀ (S : Set (Set (F.obj j))) (E : Finset J) (P : J → Set (F.obj j)) (_univ : Set.univ ∈ S)
        (_inter : ∀ A B : Set (F.obj j), A ∈ S → B ∈ S → A ∩ B ∈ S) (_cond : ∀ (e : J) (_he : e ∈ E), P e ∈ S),
        (⋂ (e) (_he : e ∈ E), P e) ∈ S :=
      by
      intro S E
      induction E using Finset.induction_on with
      | empty =>
        intro P he _hh
        simpa
      | @insert a E _ha hh1 =>
        intro hh2 hh3 hh4 hh5
        rw [Finset.set_biInter_insert]
        refine' hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 _)
        intro e he
        exact
          hh5 e
            (Finset.mem_insert_of_mem he)
              -- use the intermediate claim to finish off the goal using `univ` and `inter`.
    refine' this _ _ _ (univ _) (inter _) _
    intro e he
    dsimp
    rw [dif_pos he]
    exact compat j e (g e he) (U e) (h1 e he)
  ·
    -- conclude...
    rw [h2]
    change _ = (D.π.app j) ⁻¹' ⋂ (e : J) (_ : e ∈ G), Vs e
    rw [Set.preimage_iInter]
    apply congrArg
    ext1 e
    erw [Set.preimage_iInter]
    apply congrArg
    ext1 he
    change (D.π.app e) ⁻¹' U e = (D.π.app j) ⁻¹' if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ
    rw [dif_pos he, ← Set.preimage_comp]
    apply congrFun
    apply congrArg
    rw [← coe_comp, D.w]
    rfl
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V}
[PROOFSTEP]
let D := limitConeInfi F
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V}
[PROOFSTEP]
let E : C.pt ≅ D.pt := hC.conePointUniqueUpToIso (limitConeInfiIsLimit _)
[GOAL]
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 → ↑(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 = ↑(NatTrans.app C.π j) ⁻¹' V}
[PROOFSTEP]
have hE : Inducing E.hom := (TopCat.homeoOfIso E).inducing
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V}
[PROOFSTEP]
suffices IsTopologicalBasis {U : Set D.pt | ∃ (j : _) (V : Set (F.obj j)), V ∈ T j ∧ U = D.π.app j ⁻¹' V}
  by
  convert this.inducing hE
  ext U0
  constructor
  · rintro ⟨j, V, hV, rfl⟩
    refine' ⟨D.π.app j ⁻¹' V, ⟨j, V, hV, rfl⟩, rfl⟩
  · rintro ⟨W, ⟨j, V, hV, rfl⟩, rfl⟩
    refine'
      ⟨j, V, hV, rfl⟩
        -- Using `D`, we can apply the characterization of the topological basis of a
          -- topology defined as an infimum...
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V}
[PROOFSTEP]
convert this.inducing hE
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
⊢ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V} =
    Set.preimage ↑E.hom '' {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
ext U0
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V} ↔
    U0 ∈ Set.preimage ↑E.hom '' {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
constructor
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V} →
    U0 ∈ Set.preimage ↑E.hom '' {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
rintro ⟨j, V, hV, rfl⟩
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ ↑(NatTrans.app C.π j) ⁻¹' V ∈ Set.preimage ↑E.hom '' {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
refine' ⟨D.π.app j ⁻¹' V, ⟨j, V, hV, rfl⟩, rfl⟩
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
U0 : Set ↑C.pt
⊢ U0 ∈ Set.preimage ↑E.hom '' {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V} →
    U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V}
[PROOFSTEP]
rintro ⟨W, ⟨j, V, hV, rfl⟩, rfl⟩
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
this : IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
e_1✝ : ↑C.pt = (forget TopCat).obj C.pt
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ ↑E.hom ⁻¹' (↑(NatTrans.app D.π j) ⁻¹' V) ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app C.π j) ⁻¹' V}
[PROOFSTEP]
refine'
  ⟨j, V, hV, rfl⟩
    -- Using `D`, we can apply the characterization of the topological basis of a
      -- topology defined as an infimum...
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
⊢ IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
convert isTopologicalBasis_iInf hT fun j (x : D.pt) => D.π.app j x using 1
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
⊢ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V} =
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧ S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => ↑(NatTrans.app D.π i) x) ⁻¹' U i}
[PROOFSTEP]
ext U0
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
U0 : Set ↑D.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V} ↔
    U0 ∈
      {S |
        ∃ U F_1,
          (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧ S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => ↑(NatTrans.app D.π i) x) ⁻¹' U i}
[PROOFSTEP]
constructor
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
U0 : Set ↑D.pt
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V} →
    U0 ∈
      {S |
        ∃ U F_1,
          (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧ S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => ↑(NatTrans.app D.π i) x) ⁻¹' U i}
[PROOFSTEP]
rintro ⟨j, V, hV, rfl⟩
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
⊢ ↑(NatTrans.app D.π j) ⁻¹' V ∈
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧ S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => ↑(NatTrans.app D.π i) x) ⁻¹' U i}
[PROOFSTEP]
let U : ∀ i, Set (F.obj i) := fun i => if h : i = j then by rw [h]; exact V else Set.univ
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
i : J
h : i = j
⊢ Set ↑(F.obj i)
[PROOFSTEP]
rw [h]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑E.hom
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
i : J
h : i = j
⊢ Set ↑(F.obj j)
[PROOFSTEP]
exact V
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
⊢ ↑(NatTrans.app D.π j) ⁻¹' V ∈
    {S |
      ∃ U F_1,
        (∀ (i : J), i ∈ F_1 → U i ∈ T i) ∧ S = ⋂ (i : J) (_ : i ∈ F_1), (fun x => ↑(NatTrans.app D.π i) x) ⁻¹' U i}
[PROOFSTEP]
refine' ⟨U, { j }, _, _⟩
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
[PROOFSTEP]
rintro i h
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
[PROOFSTEP]
rw [Finset.mem_singleton] at h
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
[PROOFSTEP]
dsimp
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
[PROOFSTEP]
rw [dif_pos h]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
[PROOFSTEP]
subst h
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
[PROOFSTEP]
exact hV
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
⊢ ↑(NatTrans.app D.π j) ⁻¹' V = ⋂ (i : J) (_ : i ∈ {j}), (fun x => ↑(NatTrans.app D.π i) x) ⁻¹' U i
[PROOFSTEP]
dsimp
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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
⊢ ↑(NatTrans.app (limitConeInfi F).π j) ⁻¹' V =
    ⋂ (i : J) (_ : i ∈ {j}),
      (fun x => ↑(NatTrans.app (limitConeInfi F).π i) x) ⁻¹'
        if h : i = j then cast (_ : Set ↑(F.obj j) = Set ↑(F.obj i)) V else Set.univ
[PROOFSTEP]
simp
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π i) x) ⁻¹' U i} →
    U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
rintro ⟨U, G, h1, h2⟩
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π i) x) ⁻¹' U i
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
obtain ⟨j, hj⟩ := IsCofiltered.inf_objs_exists G
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π i) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
let g : ∀ (e) (_he : e ∈ G), j ⟶ e := fun _ he => (hj he).some
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
let Vs : J → Set (F.obj j) := fun e => if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(F.map (g e h)) ⁻¹' U e else Set.univ
⊢ U0 ∈ {U | ∃ j V, V ∈ T j ∧ U = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
let V : Set (F.obj j) := ⋂ (e : J) (_he : e ∈ G), Vs e
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 = ↑(NatTrans.app D.π j) ⁻¹' V}
[PROOFSTEP]
refine' ⟨j, V, _, _⟩
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ V ∈ T j
[PROOFSTEP]
have :
  ∀ (S : Set (Set (F.obj j))) (E : Finset J) (P : J → Set (F.obj j)) (_univ : Set.univ ∈ S)
    (_inter : ∀ A B : Set (F.obj j), A ∈ S → B ∈ S → A ∩ B ∈ S) (_cond : ∀ (e : J) (_he : e ∈ E), P e ∈ S),
    (⋂ (e) (_he : e ∈ E), P e) ∈ S :=
  by
  intro S E
  induction E using Finset.induction_on with
  | empty =>
    intro P he _hh
    simpa
  | @insert a E _ha hh1 =>
    intro hh2 hh3 hh4 hh5
    rw [Finset.set_biInter_insert]
    refine' hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 _)
    intro e he
    exact
      hh5 e
        (Finset.mem_insert_of_mem he)
          -- use the intermediate claim to finish off the goal using `univ` and `inter`.
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
[PROOFSTEP]
intro S E
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
[PROOFSTEP]
induction E using Finset.induction_on with
| empty =>
  intro P he _hh
  simpa
| @insert a E _ha hh1 =>
  intro hh2 hh3 hh4 hh5
  rw [Finset.set_biInter_insert]
  refine' hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 _)
  intro e he
  exact
    hh5 e
      (Finset.mem_insert_of_mem he)
        -- use the intermediate claim to finish off the goal using `univ` and `inter`.
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
[PROOFSTEP]
induction E using Finset.induction_on with
| empty =>
  intro P he _hh
  simpa
| @insert a E _ha hh1 =>
  intro hh2 hh3 hh4 hh5
  rw [Finset.set_biInter_insert]
  refine' hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 _)
  intro e he
  exact
    hh5 e
      (Finset.mem_insert_of_mem he)
        -- use the intermediate claim to finish off the goal using `univ` and `inter`.
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
[PROOFSTEP]

| empty =>
  intro P he _hh
  simpa
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
[PROOFSTEP]
intro P he _hh
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
_hh : ∀ (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
[PROOFSTEP]
simpa
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
_ha : ¬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
[PROOFSTEP]

| @insert a E _ha hh1 =>
  intro hh2 hh3 hh4 hh5
  rw [Finset.set_biInter_insert]
  refine' hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 _)
  intro e he
  exact
    hh5 e
      (Finset.mem_insert_of_mem he)
        -- use the intermediate claim to finish off the goal using `univ` and `inter`.
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
_ha : ¬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
[PROOFSTEP]
intro hh2 hh3 hh4 hh5
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
_ha : ¬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
[PROOFSTEP]
rw [Finset.set_biInter_insert]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
_ha : ¬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
[PROOFSTEP]
refine' hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 _)
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
_ha : ¬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
[PROOFSTEP]
intro e he
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E✝ : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
_ha : ¬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
[PROOFSTEP]
exact
  hh5 e
    (Finset.mem_insert_of_mem he)
      -- use the intermediate claim to finish off the goal using `univ` and `inter`.
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
[PROOFSTEP]
refine' this _ _ _ (univ _) (inter _) _
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
[PROOFSTEP]
intro e he
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
[PROOFSTEP]
dsimp
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 ↑(F.map (Nonempty.some (_ : Nonempty (j ⟶ e)))) ⁻¹' U e else Set.univ) ∈ T j
[PROOFSTEP]
rw [dif_pos he]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
⊢ ↑(F.map (Nonempty.some (_ : Nonempty (j ⟶ e)))) ⁻¹' U e ∈ T j
[PROOFSTEP]
exact compat j e (g e he) (U e) (h1 e he)
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(F.map (g e h)) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ (e : J) (_ : e ∈ G), Vs e
⊢ U0 = ↑(NatTrans.app D.π j) ⁻¹' V
[PROOFSTEP]
rw [h2]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 => ↑(NatTrans.app D.π i) x) ⁻¹' U i = ↑(NatTrans.app D.π j) ⁻¹' V
[PROOFSTEP]
change _ = (D.π.app j) ⁻¹' ⋂ (e : J) (_ : e ∈ G), Vs e
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 => ↑(NatTrans.app D.π i) x) ⁻¹' U i =
    ↑(NatTrans.app D.π j) ⁻¹' ⋂ (e : J) (_ : e ∈ G), Vs e
[PROOFSTEP]
rw [Set.preimage_iInter]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 => ↑(NatTrans.app D.π i) x) ⁻¹' U i =
    ⋂ (i : J), ↑(NatTrans.app D.π j) ⁻¹' ⋂ (_ : i ∈ G), Vs i
[PROOFSTEP]
apply congrArg
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 => ↑(NatTrans.app D.π i) x) ⁻¹' U i) = fun i =>
    ↑(NatTrans.app D.π j) ⁻¹' ⋂ (_ : i ∈ G), Vs i
[PROOFSTEP]
ext1 e
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 => ↑(NatTrans.app D.π e) x) ⁻¹' U e = ↑(NatTrans.app D.π j) ⁻¹' ⋂ (_ : e ∈ G), Vs e
[PROOFSTEP]
erw [Set.preimage_iInter]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 => ↑(NatTrans.app D.π e) x) ⁻¹' U e = ⋂ (_ : e ∈ G), ↑(NatTrans.app D.π j) ⁻¹' Vs e
[PROOFSTEP]
apply congrArg
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 => ↑(NatTrans.app D.π e) x) ⁻¹' U e) = fun i => ↑(NatTrans.app D.π j) ⁻¹' Vs e
[PROOFSTEP]
ext1 he
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 => ↑(NatTrans.app D.π e) x) ⁻¹' U e = ↑(NatTrans.app D.π j) ⁻¹' Vs e
[PROOFSTEP]
change (D.π.app e) ⁻¹' U e = (D.π.app j) ⁻¹' if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
⊢ ↑(NatTrans.app D.π e) ⁻¹' U e = ↑(NatTrans.app D.π j) ⁻¹' if h : e ∈ G then ↑(F.map (g e h)) ⁻¹' U e else Set.univ
[PROOFSTEP]
rw [dif_pos he, ← Set.preimage_comp]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
⊢ ↑(NatTrans.app D.π e) ⁻¹' U e = ↑(F.map (g e he)) ∘ ↑(NatTrans.app D.π j) ⁻¹' U e
[PROOFSTEP]
apply congrFun
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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 ↑(NatTrans.app D.π e) = Set.preimage (↑(F.map (g e he)) ∘ ↑(NatTrans.app D.π j))
[PROOFSTEP]
apply congrArg
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
⊢ ↑(NatTrans.app D.π e) = ↑(F.map (g e he)) ∘ ↑(NatTrans.app D.π j)
[PROOFSTEP]
rw [← coe_comp, D.w]
[GOAL]
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 → ↑(F.map f) ⁻¹' V ∈ T i
D : Cone F := limitConeInfi F
E : C.pt ≅ D.pt := IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F)
hE : Inducing ↑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 => ↑(NatTrans.app D.π 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 ↑(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
⊢ ↑(NatTrans.app D.π e) = ↑(NatTrans.app D.π e)
[PROOFSTEP]
rfl


[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ IsSemiringHom _root_.id
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ _root_.id 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ _root_.id 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ ∀ (x y : α), _root_.id (x + y) = _root_.id x + _root_.id y
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ ∀ (x y : α), _root_.id (x * y) = _root_.id x * _root_.id y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ _root_.id 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ _root_.id 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y x✝ y✝ : α
⊢ _root_.id (x✝ + y✝) = _root_.id x✝ + _root_.id y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y x✝ y✝ : α
⊢ _root_.id (x✝ * y✝) = _root_.id x✝ * _root_.id y✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
inst✝¹ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x y : α
hf : IsSemiringHom f
γ : Type u_1
inst✝ : Semiring γ
g : β → γ
hg : IsSemiringHom g
⊢ (g ∘ f) 0 = 0
[PROOFSTEP]
simpa [map_zero hf] using map_zero hg
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
inst✝¹ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x y : α
hf : IsSemiringHom f
γ : Type u_1
inst✝ : Semiring γ
g : β → γ
hg : IsSemiringHom g
⊢ (g ∘ f) 1 = 1
[PROOFSTEP]
simpa [map_one hf] using map_one hg
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
inst✝¹ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x✝ y✝ : α
hf : IsSemiringHom f
γ : Type u_1
inst✝ : Semiring γ
g : β → γ
hg : IsSemiringHom g
x y : α
⊢ (g ∘ f) (x + y) = (g ∘ f) x + (g ∘ f) y
[PROOFSTEP]
simp [map_add hf, map_add hg]
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
inst✝¹ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x✝ y✝ : α
hf : IsSemiringHom f
γ : Type u_1
inst✝ : Semiring γ
g : β → γ
hg : IsSemiringHom g
x y : α
⊢ (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
[PROOFSTEP]
simp [map_mul hf, map_mul hg]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x y : α
hf : IsSemiringHom f
src✝ : IsSemiringHom f := hf
⊢ ∀ (x y : α), f (x + y) = f x + f y
[PROOFSTEP]
apply @‹IsSemiringHom f›.map_add
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f 0 = f (0 + 0) - f 0
[PROOFSTEP]
rw [hf.map_add]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f 0 = f 0 + f 0 - f 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (0 + 0) - f 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (-x) = f (-x + x) - f x
[PROOFSTEP]
rw [hf.map_add]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (-x) = f (-x) + f x - f x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (-x + x) - f x = -f x
[PROOFSTEP]
simp [hf.map_zero]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (x - y) = f x - f y
[PROOFSTEP]
simp [sub_eq_add_neg, hf.map_add, hf.map_neg]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ IsRingHom _root_.id
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ _root_.id 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ ∀ (x y : α), _root_.id (x * y) = _root_.id x * _root_.id y
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ ∀ (x y : α), _root_.id (x + y) = _root_.id x + _root_.id y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ _root_.id 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y x✝ y✝ : α
⊢ _root_.id (x✝ * y✝) = _root_.id x✝ * _root_.id y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y x✝ y✝ : α
⊢ _root_.id (x✝ + y✝) = _root_.id x✝ + _root_.id y✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
⊢ (g ∘ f) 1 = 1
[PROOFSTEP]
simp [map_one hf]
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
⊢ g 1 = 1
[PROOFSTEP]
exact map_one hg
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
[PROOFSTEP]
simp [map_mul hf]
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ g (f x * f y) = g (f x) * g (f y)
[PROOFSTEP]
rw [map_mul hg]
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ (g ∘ f) (x + y) = (g ∘ f) x + (g ∘ f) y
[PROOFSTEP]
simp [map_add hf]
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ g (f x + f y) = g (f x) + g (f y)
[PROOFSTEP]
rw [map_add hg]


[GOAL]
F : Type u_1
inst✝ : Field F
S✝ S : Set F
hS : IsSubfield S
x y : F
hx : x ∈ S
hy : y ∈ S
⊢ x / y ∈ S
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
F : Type u_1
inst✝ : Field F
S✝ S : Set F
hS : IsSubfield S
x y : F
hx : x ∈ S
hy : y ∈ S
⊢ x * y⁻¹ ∈ S
[PROOFSTEP]
exact hS.toIsSubring.toIsSubmonoid.mul_mem hx (hS.inv_mem hy)
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
a : F
n : ℤ
s : Set F
hs : IsSubfield s
h : a ∈ s
⊢ a ^ n ∈ s
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ a ^ Int.ofNat n ∈ s
[PROOFSTEP]
suffices a ^ (n : ℤ) ∈ s by exact this
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
this : a ^ ↑n ∈ s
⊢ a ^ Int.ofNat n ∈ s
[PROOFSTEP]
exact this
[GOAL]
case ofNat
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ a ^ ↑n ∈ s
[PROOFSTEP]
rw [zpow_ofNat]
[GOAL]
case ofNat
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ a ^ n ∈ s
[PROOFSTEP]
exact hs.toIsSubring.toIsSubmonoid.pow_mem h
[GOAL]
case negSucc
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ a ^ Int.negSucc n ∈ s
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
case negSucc
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ (a ^ (n + 1))⁻¹ ∈ s
[PROOFSTEP]
exact hs.inv_mem (hs.toIsSubring.toIsSubmonoid.pow_mem h)
[GOAL]
F : Type u_1
inst✝¹ : Field F
S : Set F
K : Type u_2
inst✝ : Field K
f : F →+* K
s : Set K
hs : IsSubfield s
src✝ : IsSubring (↑f ⁻¹' s) := RingHom.isSubring_preimage f hs.toIsSubring
a : F
ha : ↑f a ∈ s
⊢ ↑f a⁻¹ ∈ s
[PROOFSTEP]
rw [map_inv₀]
[GOAL]
F : Type u_1
inst✝¹ : Field F
S : Set F
K : Type u_2
inst✝ : Field K
f : F →+* K
s : Set K
hs : IsSubfield s
src✝ : IsSubring (↑f ⁻¹' s) := RingHom.isSubring_preimage f hs.toIsSubring
a : F
ha : ↑f a ∈ s
⊢ (↑f a)⁻¹ ∈ s
[PROOFSTEP]
exact hs.inv_mem ha
[GOAL]
F : Type u_1
inst✝¹ : Field F
S : Set F
K : Type u_2
inst✝ : Field K
f : F →+* K
⊢ IsSubfield (Set.range ↑f)
[PROOFSTEP]
rw [← Set.image_univ]
[GOAL]
F : Type u_1
inst✝¹ : Field F
S : Set F
K : Type u_2
inst✝ : Field K
f : F →+* K
⊢ IsSubfield (↑f '' Set.univ)
[PROOFSTEP]
apply Image.isSubfield _ Univ.isSubfield
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
⊢ ∀ {a b : F}, a ∈ closure S → b ∈ closure S → a * b ∈ closure S
[PROOFSTEP]
rintro _ _ ⟨p, hp, q, hq, hq0, rfl⟩ ⟨r, hr, s, hs, hs0, rfl⟩
[GOAL]
case intro.intro.intro.intro.refl.intro.intro.intro.intro.refl
F : Type u_1
inst✝ : Field F
S : Set F
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
⊢ p / q * (r / s) ∈ closure S
[PROOFSTEP]
exact
  ⟨p * r, IsSubmonoid.mul_mem Ring.closure.isSubring.toIsSubmonoid hp hr, q * s,
    IsSubmonoid.mul_mem Ring.closure.isSubring.toIsSubmonoid hq hs, (div_mul_div_comm _ _ _ _).symm⟩
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
⊢ ∀ {a b : F}, a ∈ closure S → b ∈ closure S → a + b ∈ closure S
[PROOFSTEP]
intro a b ha hb
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
a b : F
ha : a ∈ closure S
hb : b ∈ closure S
⊢ a + b ∈ closure S
[PROOFSTEP]
rcases id ha with ⟨p, hp, q, hq, rfl⟩
[GOAL]
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
b : F
hb : b ∈ closure S
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
⊢ p / q + b ∈ closure S
[PROOFSTEP]
rcases id hb with ⟨r, hr, s, hs, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
⊢ p / q + r / s ∈ closure S
[PROOFSTEP]
by_cases hq0 : q = 0
[GOAL]
case pos
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : q = 0
⊢ p / q + r / s ∈ closure S
[PROOFSTEP]
rwa [hq0, div_zero, zero_add]
[GOAL]
case neg
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
⊢ p / q + r / s ∈ closure S
[PROOFSTEP]
by_cases hs0 : s = 0
[GOAL]
case pos
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
hs0 : s = 0
⊢ p / q + r / s ∈ closure S
[PROOFSTEP]
rwa [hs0, div_zero, add_zero]
[GOAL]
case neg
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
hs0 : ¬s = 0
⊢ p / q + r / s ∈ closure S
[PROOFSTEP]
exact
  ⟨p * s + q * r,
    IsAddSubmonoid.add_mem Ring.closure.isSubring.toIsAddSubgroup.toIsAddSubmonoid
      (Ring.closure.isSubring.toIsSubmonoid.mul_mem hp hs) (Ring.closure.isSubring.toIsSubmonoid.mul_mem hq hr),
    q * s, Ring.closure.isSubring.toIsSubmonoid.mul_mem hq hs, (div_add_div p r hq0 hs0).symm⟩
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
⊢ ∀ {a : F}, a ∈ closure S → -a ∈ closure S
[PROOFSTEP]
rintro _ ⟨p, hp, q, hq, rfl⟩
[GOAL]
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
⊢ -(p / q) ∈ closure S
[PROOFSTEP]
exact ⟨-p, Ring.closure.isSubring.toIsAddSubgroup.neg_mem hp, q, hq, neg_div q p⟩
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
⊢ ∀ {x : F}, x ∈ closure S → x⁻¹ ∈ closure S
[PROOFSTEP]
rintro _ ⟨p, hp, q, hq, rfl⟩
[GOAL]
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
⊢ (p / q)⁻¹ ∈ closure S
[PROOFSTEP]
exact ⟨q, hq, p, hp, (inv_div _ _).symm⟩
[GOAL]
F : Type u_1
inst✝ : Field F
S T : Set F
hT : IsSubfield T
H : S ⊆ T
⊢ closure S ⊆ T
[PROOFSTEP]
rintro _ ⟨p, hp, q, hq, hq0, rfl⟩
[GOAL]
case intro.intro.intro.intro.refl
F : Type u_1
inst✝ : Field F
S T : Set F
hT : IsSubfield T
H : S ⊆ T
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
⊢ p / q ∈ T
[PROOFSTEP]
exact hT.div_mem (Ring.closure_subset hT.toIsSubring H hp) (Ring.closure_subset hT.toIsSubring H hq)


[GOAL]
α : Type u
a b : Thunk α
eq : Thunk.get a = Thunk.get b
⊢ a = b
[PROOFSTEP]
have ⟨_⟩ := a
[GOAL]
α : Type u
a b : Thunk α
fn✝ : Unit → α
eq : Thunk.get { fn := fn✝ } = Thunk.get b
⊢ { fn := fn✝ } = b
[PROOFSTEP]
have ⟨_⟩ := b
[GOAL]
α : Type u
a b : Thunk α
fn✝¹ fn✝ : Unit → α
eq : Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }
⊢ { fn := fn✝¹ } = { fn := fn✝ }
[PROOFSTEP]
congr
[GOAL]
case e_fn
α : Type u
a b : Thunk α
fn✝¹ fn✝ : Unit → α
eq : Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }
⊢ fn✝¹ = fn✝
[PROOFSTEP]
exact funext fun _ ↦ eq
[GOAL]
α : Type u
inst✝ : DecidableEq α
⊢ DecidableEq (Thunk α)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
⊢ Decidable (a = b)
[PROOFSTEP]
have : a = b ↔ a.get = b.get := ⟨by intro x; rw [x], by intro; ext; assumption⟩
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
⊢ a = b → Thunk.get a = Thunk.get b
[PROOFSTEP]
intro x
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
x : a = b
⊢ Thunk.get a = Thunk.get b
[PROOFSTEP]
rw [x]
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
⊢ Thunk.get a = Thunk.get b → a = b
[PROOFSTEP]
intro
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
a✝ : Thunk.get a = Thunk.get b
⊢ a = b
[PROOFSTEP]
ext
[GOAL]
case eq
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
a✝ : Thunk.get a = Thunk.get b
⊢ Thunk.get a = Thunk.get b
[PROOFSTEP]
assumption
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
this : a = b ↔ Thunk.get a = Thunk.get b
⊢ Decidable (a = b)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
this : a = b ↔ Thunk.get a = Thunk.get b
⊢ Decidable (Thunk.get a = Thunk.get b)
[PROOFSTEP]
infer_instance