J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ IsClosed (partialSections F H)
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
⊢ IsClosed (partialSections F H)
have :
  partialSections F H =
    ⋂ (f : FiniteDiagramArrow G) (_ : f ∈ H), { u | F.map f.2.2.2.2 (u f.1) = u f.2.1 } := by
  ext1
  simp only [Set.mem_iInter, Set.mem_setOf_eq]
  rfl
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ IsClosed
    (⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst})
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ IsClosed (partialSections F H)
rw [this]
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ ∀ (i : TopCat.FiniteDiagramArrow G),
    (i ∈ fun i => i ∈ H.val) → IsClosed {u | (forget TopCat).map (F.map i.snd.snd.snd.snd) (u i.fst) = u i.snd.fst}
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ IsClosed
    (⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst})
apply isClosed_biInter
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
⊢ IsClosed {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
⊢ ∀ (i : TopCat.FiniteDiagramArrow G),
    (i ∈ fun i => i ∈ H.val) → IsClosed {u | (forget TopCat).map (F.map i.snd.snd.snd.snd) (u i.fst) = u i.snd.fst}
intro f _
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ IsClosed {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
⊢ IsClosed {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
have : T2Space ((forget TopCat).obj (F.obj f.snd.fst)) := I f.snd.fst
case h.hf
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ Continuous fun x => (forget TopCat).map (F.map f.snd.snd.snd.snd) (x f.fst)

case h.hg
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ Continuous fun x => x f.snd.fst
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ IsClosed {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
apply isClosed_eq
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔
    x✝ ∈
      ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
        {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
⊢ partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
ext1
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔
    ∀ (i : TopCat.FiniteDiagramArrow G), i ∈ H → (forget TopCat).map (F.map i.snd.snd.snd.snd) (x✝ i.fst) = x✝ i.snd.fst
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔
    x✝ ∈
      ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
        {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
simp only [Set.mem_iInter, Set.mem_setOf_eq]
no goals
case h
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔
    ∀ (i : TopCat.FiniteDiagramArrow G), i ∈ H → (forget TopCat).map (F.map i.snd.snd.snd.snd) (x✝ i.fst) = x✝ i.snd.fst
rfl
no goals
case h.hf
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ Continuous fun x => (forget TopCat).map (F.map f.snd.snd.snd.snd) (x f.fst)
apply Continuous.comp (F.map f.snd.snd.snd.snd).continuous_toFun (continuous_apply f.fst)
no goals
case h.hg
J✝ : Type v
inst✝¹ : SmallCategory J✝
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
I : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this✝ :
  partialSections F H =
    ⋂ (f : TopCat.FiniteDiagramArrow G) (_ : f ∈ H),
      {u | (forget TopCat).map (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ fun i => i ∈ H.val
this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))
⊢ Continuous fun x => x f.snd.fst
apply continuous_apply f.snd.fst