-- Mathlib/Topology/Category/TopCat/Limits/Konig.lean
theorem partialSections.closed [∀ j : J, T2Space (F.obj j)] {G : Finset J}
    (H : Finset (FiniteDiagramArrow G)) : IsClosed (partialSections F H)

Proof state:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
⊢ IsClosed (partialSections F H)

Tactic:
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

Result:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ IsClosed (partialSections F H)

Proof state:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (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 ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq]

Result:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (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 ∈ H, (ConcreteCategory.hom (F.map i.snd.snd.snd.snd)) (x✝ i.fst) = x✝ i.snd.fst

Proof state:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (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 ∈ H, (ConcreteCategory.hom (F.map i.snd.snd.snd.snd)) (x✝ i.fst) = x✝ i.snd.fst

Tactic:
rfl

Result:
no goals

Proof state:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ Membership.mem H.val
⊢ IsClosed {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Tactic:
apply isClosed_eq <;> fun_prop

Result:
no goals

Proof state:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
⊢ partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Tactic:
ext1

Result:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (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 ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Proof state:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ IsClosed (⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst})

Tactic:
apply isClosed_biInter

Result:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ ∀ i ∈ Membership.mem H.val, IsClosed {u | (ConcreteCategory.hom (F.map i.snd.snd.snd.snd)) (u i.fst) = u i.snd.fst}

Proof state:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ ∀ i ∈ Membership.mem H.val, IsClosed {u | (ConcreteCategory.hom (F.map i.snd.snd.snd.snd)) (u i.fst) = u i.snd.fst}

Tactic:
intro f _

Result:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : TopCat.FiniteDiagramArrow G
a✝ : f ∈ Membership.mem H.val
⊢ IsClosed {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Proof state:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ IsClosed (partialSections F H)

Tactic:
rw [this]

Result:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (TopCat.FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ IsClosed (⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst})