-- More compactness: finite sets and finite unions of compact sets are
-- compact, a compact set meets a closed set in a compact set, compact
-- sets in Hausdorff spaces are closed and separate from points and from
-- each other, a compact Hausdorff space is regular and normal, and a
-- family of closed sets with the finite intersection property meets
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Topology.CompactMore
import Separation
import Cardinal.FiniteUnion
import Set.Choice

-- Finite sets are compact: pick one cover member through each point.

def coverMembers (C a : Set) : Set := { U ∈ C | a ∈ U }

defgraph coverChoice (C A : Set) (a ∈ A) : C := choose(coverMembers(C, a))
requires covers : A ⊆ ⋃(C)
proof
  have covered := covers with a, member
  obtain ⟨U, hU, haU⟩ := union.membership.forward with covered
  have found : U ∈ coverMembers(C, a) := coverMembers.membership.backward with ⟨hU, haU⟩
  have inhabited : Nonempty(coverMembers(C, a)) := ⟨U, found⟩
  have chosen := choose.member with inhabited
  have parts := coverMembers.membership.forward with chosen
  exact parts.left

theorem coverChoice.selected (C A a : Set)
  requires covers : A ⊆ ⋃(C)
  requires ha : a ∈ A
  shows coverChoice(C, A)(a) ∈ coverMembers(C, a)
proof
  have value := coverChoice.value with covers, ha
  rw value
  have covered := covers with a, ha
  obtain ⟨U, hU, haU⟩ := union.membership.forward with covered
  have found : U ∈ coverMembers(C, a) := coverMembers.membership.backward with ⟨hU, haU⟩
  have inhabited : Nonempty(coverMembers(C, a)) := ⟨U, found⟩
  exact choose.member with inhabited

theorem IsCompact.finite (X T A : Set)
  requires finite : Finite(A)
  requires hA : A ⊆ X
  shows IsCompact(X, T, A)
proof
  constructor
  . exact hA
  . intros C cover
    have covers := cover.right
    have graph := coverChoice.function with covers
    witness functionImage(coverChoice(C, A), A, C)
    refine ⟨(functionImage.subset at coverChoice(C, A), A, C), (Finite.function_image with graph, finite, (Subset.reflexive at A)), ?_⟩
    intros a ha
    have selected := coverChoice.selected with covers, ha
    have parts := coverMembers.membership.forward with selected
    have imageMember := functionImage.value with graph, ha
    exact union.contains with imageMember, parts.right

theorem IsCompact.whole_of_finite (X T : Set)
  requires finite : Finite(X)
  shows IsCompact(X, T, X)
proof
  exact IsCompact.finite with finite, (Subset.reflexive at X)

-- A finite union of compact sets is compact: choose a finite subcover of
-- each member and take their union.

def finiteSubcovers (C A : Set) : Set := { G ∈ 𝒫(C) | Finite(G) ∧ A ⊆ ⋃(G) }

defgraph subcoverChoice (X T C F : Set) (A ∈ F) : 𝒫(C) := choose(finiteSubcovers(C, A))
requires compact : ∀ B ∈ F, IsCompact(X, T, B)
requires cover : OpenCover(T, ⋃(F), C)
proof
  have compactA := compact with A, member
  have below := union.subset_of_member with member
  have coverA : OpenCover(T, A, C) := ⟨cover.left, (Subset.transitive with below, cover.right)⟩
  obtain ⟨G, hG, finiteG, covered⟩ := compactA.right with C, coverA
  have found : G ∈ finiteSubcovers(C, A) := finiteSubcovers.membership.backward with ⟨(powerset.membership_iff.backward with hG), finiteG, covered⟩
  have inhabited : Nonempty(finiteSubcovers(C, A)) := ⟨G, found⟩
  have chosen := choose.member with inhabited
  have parts := finiteSubcovers.membership.forward with chosen
  exact parts.left

theorem subcoverChoice.selected (X T C F A : Set)
  requires compact : ∀ B ∈ F, IsCompact(X, T, B)
  requires cover : OpenCover(T, ⋃(F), C)
  requires hA : A ∈ F
  shows subcoverChoice(X, T, C, F)(A) ∈ finiteSubcovers(C, A)
proof
  have value := subcoverChoice.value with compact, cover, hA
  rw value
  have compactA := compact with A, hA
  have below := union.subset_of_member with hA
  have coverA : OpenCover(T, A, C) := ⟨cover.left, (Subset.transitive with below, cover.right)⟩
  obtain ⟨G, hG, finiteG, covered⟩ := compactA.right with C, coverA
  have found : G ∈ finiteSubcovers(C, A) := finiteSubcovers.membership.backward with ⟨(powerset.membership_iff.backward with hG), finiteG, covered⟩
  have inhabited : Nonempty(finiteSubcovers(C, A)) := ⟨G, found⟩
  exact choose.member with inhabited

theorem IsCompact.finite_union (X T F : Set)
  requires finite : Finite(F)
  requires compact : ∀ B ∈ F, IsCompact(X, T, B)
  shows IsCompact(X, T, ⋃(F))
proof
  constructor
  . apply union.subset
    intros B hB
    have compactB := compact with B, hB
    exact compactB.left
  . intros C cover
    have graph := subcoverChoice.function with compact, cover
    have imageFinite := Finite.function_image with graph, finite, (Subset.reflexive at F)
    witness ⋃(functionImage(subcoverChoice(X, T, C, F), F, 𝒫(C)))
    refine ⟨?_, ?_, ?_⟩
    . apply union.subset
      intros G hG
      have inside := functionImage.subset at subcoverChoice(X, T, C, F), F, 𝒫(C)
      exact powerset.membership_iff.forward with (inside with G, hG)
    . apply Finite.big_union with imageFinite
      intros G hG
      simp [functionImage.membership] at hG
      obtain ⟨hGP, B, hB, shape⟩ := hG
      have selected := subcoverChoice.selected with compact, cover, hB
      have parts := finiteSubcovers.membership.forward with selected
      rw shape
      exact parts.right.left
    . intros x hx
      obtain ⟨B, hB, hxB⟩ := union.membership.forward with hx
      have selected := subcoverChoice.selected with compact, cover, hB
      have parts := finiteSubcovers.membership.forward with selected
      have covered := parts.right.right with x, hxB
      obtain ⟨U, hU, hxU⟩ := union.membership.forward with covered
      have imageMember := functionImage.value with graph, hB
      have inUnion := union.contains with imageMember, hU
      exact union.contains with inUnion, hxU

-- A compact set meets a closed set in a compact set: add the complement
-- of the closed set to a cover of the intersection.
theorem IsCompact.intersection_closed (X T K C : Set)
  requires topology : IsTopology(X, T)
  requires compact : IsCompact(X, T, K)
  requires closed : IsClosed(X, T, C)
  shows IsCompact(X, T, K ∩ C)
proof
  have hKX := compact.left
  constructor
  . exact Subset.transitive with (intersection.subset_left at K, C), hKX
  . intros D cover
    have extendedOpen : insert(complement(X, C), D) ⊆ T
      intros U hU
      have split := insert.membership.forward with hU
      cases split with isComplement | inD
      . rw isComplement
        exact closed.right
      . exact cover.left with U, inD
    have extendedCover : K ⊆ ⋃(insert(complement(X, C), D))
      intros k hk
      have hkX := hKX with k, hk
      have split : k ∈ C ∨ ¬k ∈ C by tauto
      cases split with inC | outside
      . have inBoth : k ∈ K ∩ C := intersection.membership.backward with ⟨hk, inC⟩
        have covered := cover.right with k, inBoth
        obtain ⟨U, hU, hkU⟩ := union.membership.forward with covered
        have found : U ∈ insert(complement(X, C), D)
          apply insert.membership.backward
          right
          exact hU
        exact union.contains with found, hkU
      . have inComplement : k ∈ complement(X, C) := complement.membership.backward with ⟨hkX, outside⟩
        have found : complement(X, C) ∈ insert(complement(X, C), D)
          apply insert.membership.backward
          left
          rfl
        exact union.contains with found, inComplement
    obtain ⟨F, hF, finiteF, coveredK⟩ := compact.right with insert(complement(X, C), D), ⟨extendedOpen, extendedCover⟩
    witness F ∖ {complement(X, C)}
    refine ⟨?_, (Finite.subset with finiteF, (difference.subset_left at F, {complement(X, C)})), ?_⟩
    . intros U hU
      have parts := difference.singleton_membership.forward with hU
      have split := insert.membership.forward with (hF with U, parts.left)
      cases split with isComplement | inD
      . exfalso
        exact parts.right with isComplement
      . exact inD
    . intros k hk
      have inBoth := intersection.membership.forward with hk
      have covered := coveredK with k, inBoth.left
      obtain ⟨U, hU, hkU⟩ := union.membership.forward with covered
      have kept : U ∈ F ∖ {complement(X, C)}
        apply difference.singleton_membership.backward
        refine ⟨hU, ?_⟩
        intro isComplement
        rw isComplement at hkU
        have away := complement.membership.forward with hkU
        exact away.right with inBoth.right
      exact union.contains with kept, hkU

-- Separating a compact set from a set D: when every point of K has an
-- open neighbourhood disjoint from an open set around D, so does K.

def separators (T D U : Set) : Set := { V ∈ T | D ⊆ V ∧ Disjoint(U, V) }
def separatingOpens (T D : Set) : Set := { U ∈ T | Nonempty(separators(T, D, U)) }

defgraph separatorChoice (T D F : Set) (U ∈ F) : T := choose(separators(T, D, U))
requires inside : F ⊆ separatingOpens(T, D)
proof
  have hU := inside with U, member
  have parts := separatingOpens.membership.forward with hU
  have chosen := choose.member with parts.right
  have chosenParts := separators.membership.forward with chosen
  exact chosenParts.left

theorem separatorChoice.selected (T D F U : Set)
  requires inside : F ⊆ separatingOpens(T, D)
  requires hU : U ∈ F
  shows separatorChoice(T, D, F)(U) ∈ separators(T, D, U)
proof
  have value := separatorChoice.value with inside, hU
  rw value
  have hU2 := inside with U, hU
  have parts := separatingOpens.membership.forward with hU2
  exact choose.member with parts.right

theorem IsCompact.separate (X T K D : Set)
  requires topology : IsTopology(X, T)
  requires compact : IsCompact(X, T, K)
  requires hD : D ⊆ X
  requires separated : ∀ k ∈ K, ∃ U ∈ T, ∃ V ∈ T, k ∈ U ∧ D ⊆ V ∧ Disjoint(U, V)
  shows ∃ U ∈ T, ∃ V ∈ T, K ⊆ U ∧ D ⊆ V ∧ Disjoint(U, V)
proof
  have coverOpen : separatingOpens(T, D) ⊆ T
    intros U hU
    have parts := separatingOpens.membership.forward with hU
    exact parts.left
  have covers : K ⊆ ⋃(separatingOpens(T, D))
    intros k hk
    obtain ⟨U, hU, V, hV, hkU, inside, disjoint⟩ := separated with k, hk
    have found : V ∈ separators(T, D, U) := separators.membership.backward with ⟨hV, inside, disjoint⟩
    have inhabited : Nonempty(separators(T, D, U)) := ⟨V, found⟩
    have opens : U ∈ separatingOpens(T, D) := separatingOpens.membership.backward with ⟨hU, inhabited⟩
    exact union.contains with opens, hkU
  obtain ⟨F, hF, finiteF, coveredK⟩ := compact.right with separatingOpens(T, D), ⟨coverOpen, covers⟩
  have split : Nonempty(F) ∨ ¬Nonempty(F) by tauto
  cases split with inhabited | empty
  . have graph := separatorChoice.function with hF
    have openUnion := IsTopology.union with topology, (Subset.transitive with hF, coverOpen)
    have imageInside := functionImage.subset at separatorChoice(T, D, F), F, T
    have imageFinite := Finite.function_image with graph, finiteF, (Subset.reflexive at F)
    obtain ⟨U0, hU0⟩ := inhabited
    have firstMember := functionImage.value with graph, hU0
    have imageInhabited : Nonempty(functionImage(separatorChoice(T, D, F), F, T)) := ⟨separatorChoice(T, D, F)(U0), firstMember⟩
    have openMeet := IsTopology.finite_intersection with topology, imageFinite, imageInside, imageInhabited
    refine ⟨⋃(F), openUnion, ⋂(functionImage(separatorChoice(T, D, F), F, T)), openMeet, coveredK, ?_, ?_⟩
    . apply familyIntersection.greatest with imageInhabited
      intros V hV
      simp [functionImage.membership] at hV
      obtain ⟨hVT, U, hU, shape⟩ := hV
      have selected := separatorChoice.selected with hF, hU
      have parts := separators.membership.forward with selected
      rw shape
      exact parts.right.left
    . apply Disjoint.iff.backward
      intros x hx hxMeet
      obtain ⟨U, hU, hxU⟩ := union.membership.forward with hx
      have meetParts := familyIntersection.membership.forward with hxMeet
      have imageMember := functionImage.value with graph, hU
      have hxV := meetParts.right with separatorChoice(T, D, F)(U), imageMember
      have selected := separatorChoice.selected with hF, hU
      have parts := separators.membership.forward with selected
      have separatedUV := Disjoint.iff.forward with parts.right.right
      exact separatedUV with x, hxU, hxV
  . have equal : F = ∅
      by_contra different
      apply empty
      exact Nonempty.of_ne_empty with different
    rw [equal, union.empty] at coveredK
    refine ⟨∅, (IsTopology.empty with topology), X, (IsTopology.whole with topology), coveredK, hD, ?_⟩
    exact Disjoint.empty_left at X

-- In a Hausdorff space a compact set and a point outside it have
-- disjoint open neighbourhoods, so compact sets are closed.

theorem IsCompact.hausdorff_separated (X T K x : Set)
  requires topology : IsTopology(X, T)
  requires hausdorff : IsHausdorff(X, T)
  requires compact : IsCompact(X, T, K)
  requires hx : x ∈ X
  requires away : ¬x ∈ K
  shows ∃ U ∈ T, ∃ V ∈ T, K ⊆ U ∧ x ∈ V ∧ Disjoint(U, V)
proof
  have singletonInside : {x} ⊆ X := singleton.subset_iff.backward with hx
  have separated : ∀ k ∈ K, ∃ U ∈ T, ∃ V ∈ T, k ∈ U ∧ {x} ⊆ V ∧ Disjoint(U, V)
    intros k hk
    have hkX := compact.left with k, hk
    have distinct : k ≠ x
      intro same
      apply away
      rw ← same
      exact hk
    obtain ⟨U, hU, V, hV, hkU, hxV, disjoint⟩ := hausdorff with k, hkX, x, hx, distinct
    have inside : {x} ⊆ V := singleton.subset_iff.backward with hxV
    exact ⟨U, hU, V, hV, hkU, inside, disjoint⟩
  obtain ⟨U, hU, V, hV, coverK, inside, disjoint⟩ := IsCompact.separate with topology, compact, singletonInside, separated
  have hxV := singleton.subset_iff.forward with inside
  exact ⟨U, hU, V, hV, coverK, hxV, disjoint⟩

def avoiding (T K : Set) : Set := { V ∈ T | Disjoint(V, K) }

theorem IsCompact.hausdorff_closed (X T K : Set)
  requires topology : IsTopology(X, T)
  requires hausdorff : IsHausdorff(X, T)
  requires compact : IsCompact(X, T, K)
  shows IsClosed(X, T, K)
proof
  constructor
  . exact compact.left
  . have avoidingOpen : avoiding(T, K) ⊆ T
      intros V hV
      have parts := avoiding.membership.forward with hV
      exact parts.left
    have isOpen := IsTopology.union with topology, avoidingOpen
    have equal : complement(X, K) = ⋃(avoiding(T, K))
      ext x
      constructor
      . intro hx
        have parts := complement.membership.forward with hx
        obtain ⟨U, hU, V, hV, coverK, hxV, disjoint⟩ := IsCompact.hausdorff_separated with topology, hausdorff, compact, parts.left, parts.right
        have symmetric := Disjoint.symmetric with disjoint
        have disjointK := Disjoint.of_subset_right with symmetric, coverK
        have found : V ∈ avoiding(T, K) := avoiding.membership.backward with ⟨hV, disjointK⟩
        exact union.contains with found, hxV
      . intro hx
        obtain ⟨V, hV, hxV⟩ := union.membership.forward with hx
        have parts := avoiding.membership.forward with hV
        have inside := IsTopology.subset with topology, parts.left
        have separated := Disjoint.iff.forward with parts.right
        apply complement.membership.backward
        exact ⟨(inside with x, hxV), (separated with x, hxV)⟩
    rwa equal

-- In a compact Hausdorff space the compact sets are exactly the closed
-- sets.
theorem IsCompact.hausdorff_iff_closed (X T K : Set)
  requires topology : IsTopology(X, T)
  requires hausdorff : IsHausdorff(X, T)
  requires compact : IsCompact(X, T, X)
  shows IsCompact(X, T, K) ↔ IsClosed(X, T, K)
proof
  constructor
  . intro compactK
    exact IsCompact.hausdorff_closed with topology, hausdorff, compactK
  . intro closed
    exact IsCompact.closed_subset with topology, compact, closed, closed.left

theorem IsCompact.hausdorff_intersection (X T K L : Set)
  requires topology : IsTopology(X, T)
  requires hausdorff : IsHausdorff(X, T)
  requires compactK : IsCompact(X, T, K)
  requires compactL : IsCompact(X, T, L)
  shows IsCompact(X, T, K ∩ L)
proof
  have closed := IsCompact.hausdorff_closed with topology, hausdorff, compactL
  exact IsCompact.intersection_closed with topology, compactK, closed

-- Two disjoint compact sets in a Hausdorff space have disjoint open
-- neighbourhoods.
theorem IsCompact.hausdorff_separate (X T K L : Set)
  requires topology : IsTopology(X, T)
  requires hausdorff : IsHausdorff(X, T)
  requires compactK : IsCompact(X, T, K)
  requires compactL : IsCompact(X, T, L)
  requires disjoint : Disjoint(K, L)
  shows ∃ U ∈ T, ∃ V ∈ T, K ⊆ U ∧ L ⊆ V ∧ Disjoint(U, V)
proof
  have separatedKL := Disjoint.iff.forward with disjoint
  have separated : ∀ k ∈ K, ∃ U ∈ T, ∃ V ∈ T, k ∈ U ∧ L ⊆ V ∧ Disjoint(U, V)
    intros k hk
    have hkX := compactK.left with k, hk
    have away := separatedKL with k, hk
    obtain ⟨U, hU, V, hV, coverL, hkV, disjointUV⟩ := IsCompact.hausdorff_separated with topology, hausdorff, compactL, hkX, away
    have symmetric := Disjoint.symmetric with disjointUV
    exact ⟨V, hV, U, hU, hkV, coverL, symmetric⟩
  exact IsCompact.separate with topology, compactK, compactL.left, separated

theorem IsCompact.hausdorff_regular (X T : Set)
  requires topology : IsTopology(X, T)
  requires hausdorff : IsHausdorff(X, T)
  requires compact : IsCompact(X, T, X)
  shows RegularSpace(X, T)
proof
  intros x hx C closedC away
  have compactC := IsCompact.closed_subset with topology, compact, closedC, closedC.left
  obtain ⟨U, hU, V, hV, coverC, hxV, disjoint⟩ := IsCompact.hausdorff_separated with topology, hausdorff, compactC, hx, away
  have symmetric := Disjoint.symmetric with disjoint
  exact ⟨V, hV, U, hU, hxV, coverC, symmetric⟩

theorem IsCompact.hausdorff_normal (X T : Set)
  requires topology : IsTopology(X, T)
  requires hausdorff : IsHausdorff(X, T)
  requires compact : IsCompact(X, T, X)
  shows NormalSpace(X, T)
proof
  intros C closedC D closedD disjoint
  have compactC := IsCompact.closed_subset with topology, compact, closedC, closedC.left
  have compactD := IsCompact.closed_subset with topology, compact, closedD, closedD.left
  exact IsCompact.hausdorff_separate with topology, hausdorff, compactC, compactD, disjoint

-- The finite intersection property: every finite nonempty subfamily has
-- a common point. In a compact space a family of closed sets with this
-- property has a common point, and that characterises compactness.

predicate FiniteIntersectionProperty (S : Set) :=
  ∀ F, F ⊆ S → Finite(F) → Nonempty(F) → Nonempty(⋂(F))

defgraph complementMap (X G : Set) (g ∈ G) : 𝒫(X) := complement(X, g)
proof
  exact powerset.membership_iff.backward with (complement.subset at X, g)

theorem complementMap.selected (X S G g : Set)
  requires inside : ∀ C ∈ S, C ⊆ X
  requires hG : G ⊆ complements(X, S)
  requires hg : g ∈ G
  shows complementMap(X, G)(g) ∈ S ∧ complement(X, complementMap(X, G)(g)) = g
proof
  have value := complementMap.value at X, G, g with hg
  rw value
  obtain ⟨C, hC, shape⟩ := complements.membership.forward with (hG with g, hg)
  have hCX := inside with C, hC
  have fold : complement(X, C) = X ∖ C
    unfold complement
    rfl
  rw ← fold at shape
  rw ← shape
  have double := complement.complement with hCX
  rw double
  constructor
  . exact hC
  . rfl

theorem IsCompact.closed_family_meets (X T S : Set)
  requires topology : IsTopology(X, T)
  requires compact : IsCompact(X, T, X)
  requires closed : ∀ C ∈ S, IsClosed(X, T, C)
  requires fip : FiniteIntersectionProperty(S)
  requires nonempty : Nonempty(S)
  shows Nonempty(⋂(S))
proof
  have inside : ∀ C ∈ S, C ⊆ X
    intros C hC
    have closedC := closed with C, hC
    exact closedC.left
  by_contra none
  have empty : ⋂(S) = ∅
    by_contra different
    apply none
    exact Nonempty.of_ne_empty with different
  have coverOpen : complements(X, S) ⊆ T
    intros U hU
    obtain ⟨C, hC, shape⟩ := complements.membership.forward with hU
    rw ← shape
    have closedC := closed with C, hC
    have isOpen := closedC.right
    unfold complement at isOpen
    exact isOpen
  have covers : X ⊆ ⋃(complements(X, S))
    have demorgan := complements.intersection at X, S with nonempty
    rw [← demorgan, empty, complement.empty]
    exact Subset.reflexive at X
  obtain ⟨G, hG, finiteG, coveredX⟩ := compact.right with complements(X, S), ⟨coverOpen, covers⟩
  have graph := complementMap.function at X, G
  have values : ∀ g ∈ G, complementMap(X, G)(g) ∈ S
    intros g hg
    have selected := complementMap.selected with inside, hG, hg
    exact selected.left
  have graphS := FunctionBetween.codomain_of_values with graph, values
  have imageFinite := Finite.function_image with graphS, finiteG, (Subset.reflexive at G)
  have imageInside := functionImage.subset at complementMap(X, G), G, S
  have inhabitedG : Nonempty(G)
    by_contra emptyG
    have equal : G = ∅
      by_contra different
      apply emptyG
      exact Nonempty.of_ne_empty with different
    rw [equal, union.empty] at coveredX
    obtain ⟨C, hC⟩ := nonempty
    have singletonInside : {C} ⊆ S := singleton.subset_iff.backward with hC
    have meets := fip with {C}, singletonInside, (Finite.singleton at C), (Nonempty.singleton at C)
    rw familyIntersection.singleton at meets
    obtain ⟨x, hx⟩ := meets
    have hxX := inside with C, hC, x, hx
    have inEmpty := coveredX with x, hxX
    exact empty.membership with x, inEmpty
  obtain ⟨g0, hg0⟩ := inhabitedG
  have firstMember := functionImage.value with graphS, hg0
  have imageInhabited : Nonempty(functionImage(complementMap(X, G), G, S)) := ⟨complementMap(X, G)(g0), firstMember⟩
  have meets := fip with functionImage(complementMap(X, G), G, S), imageInside, imageFinite, imageInhabited
  obtain ⟨x, hx⟩ := meets
  have meetParts := familyIntersection.membership.forward with hx
  have inFirst := meetParts.right with complementMap(X, G)(g0), firstMember
  have selected0 := complementMap.selected with inside, hG, hg0
  have hxX := inside with complementMap(X, G)(g0), selected0.left, x, inFirst
  have covered := coveredX with x, hxX
  obtain ⟨g, hg, hxg⟩ := union.membership.forward with covered
  have selected := complementMap.selected with inside, hG, hg
  have imageMember := functionImage.value with graphS, hg
  have inC := meetParts.right with complementMap(X, G)(g), imageMember
  have shape := selected.right
  rw ← shape at hxg
  have away := complement.membership.forward with hxg
  exact away.right with inC

theorem IsCompact.of_closed_families (X T : Set)
  requires topology : IsTopology(X, T)
  requires meets : ∀ S, (∀ C ∈ S, IsClosed(X, T, C)) → FiniteIntersectionProperty(S) →
    Nonempty(S) → Nonempty(⋂(S))
  shows IsCompact(X, T, X)
proof
  constructor
  . exact Subset.reflexive at X
  . intros C cover
    by_contra none
    have split : Nonempty(C) ∨ ¬Nonempty(C) by tauto
    cases split with inhabitedC | emptyC
    . have inside : ∀ U ∈ C, U ⊆ X
        intros U hU
        exact IsTopology.subset with topology, (cover.left with U, hU)
      have closedFamily : ∀ D ∈ complements(X, C), IsClosed(X, T, D)
        intros D hD
        obtain ⟨U, hU, shape⟩ := complements.membership.forward with hD
        have fold : complement(X, U) = X ∖ U
          unfold complement
          rfl
        rw [← shape, ← fold]
        exact Open.complement_closed with topology, (cover.left with U, hU)
      have fip : FiniteIntersectionProperty(complements(X, C))
        intros F hF finiteF inhabitedF
        by_contra noPoint
        apply none
        have graph := complementMap.function at X, F
        have values : ∀ f ∈ F, complementMap(X, F)(f) ∈ C
          intros f hf
          have selected := complementMap.selected with inside, hF, hf
          exact selected.left
        have graphC := FunctionBetween.codomain_of_values with graph, values
        witness functionImage(complementMap(X, F), F, C)
        refine ⟨(functionImage.subset at complementMap(X, F), F, C), (Finite.function_image with graphC, finiteF, (Subset.reflexive at F)), ?_⟩
        intros x hx
        have characterization := familyIntersection.membership_of_nonempty at x, F with inhabitedF
        have notAll : ¬(∀ f ∈ F, x ∈ f)
          intro all
          apply noPoint
          exact ⟨x, (characterization.backward with all)⟩
        by_contra notCovered
        apply notAll
        intros f hf
        by_contra outside
        apply notCovered
        have selected := complementMap.selected with inside, hF, hf
        have imageMember := functionImage.value with graphC, hf
        have inOriginal : x ∈ complementMap(X, F)(f)
          by_contra notIn
          apply outside
          rw ← selected.right
          exact complement.membership.backward with ⟨hx, notIn⟩
        exact union.contains with imageMember, inOriginal
      obtain ⟨U, hU⟩ := inhabitedC
      have found : X ∖ U ∈ complements(X, C) := complements.membership.backward with ⟨U, hU, rfl⟩
      have inhabitedS : Nonempty(complements(X, C)) := ⟨X ∖ U, found⟩
      obtain ⟨x, hx⟩ := meets with complements(X, C), closedFamily, fip, inhabitedS
      have characterization := familyIntersection.membership_of_nonempty at x, complements(X, C) with inhabitedS
      have all := characterization.forward with hx
      have inFirst := all with X ∖ U, found
      have firstParts := difference.membership.forward with inFirst
      have covered := cover.right with x, firstParts.left
      obtain ⟨V, hV, hxV⟩ := union.membership.forward with covered
      have foundV : X ∖ V ∈ complements(X, C) := complements.membership.backward with ⟨V, hV, rfl⟩
      have inV := all with X ∖ V, foundV
      have partsV := difference.membership.forward with inV
      exact partsV.right with hxV
    . apply none
      have equal : C = ∅
        by_contra different
        apply emptyC
        exact Nonempty.of_ne_empty with different
      have covered := cover.right
      rw equal at covered
      witness ∅
      exact ⟨(empty.subset at C), Finite.empty, covered⟩

theorem IsCompact.iff_closed_families (X T : Set)
  requires topology : IsTopology(X, T)
  shows IsCompact(X, T, X) ↔ ∀ S, (∀ C ∈ S, IsClosed(X, T, C)) →
    FiniteIntersectionProperty(S) → Nonempty(S) → Nonempty(⋂(S))
proof
  constructor
  . intros compact S closed fip nonempty
    exact IsCompact.closed_family_meets with topology, compact, closed, fip, nonempty
  . intro meets
    exact IsCompact.of_closed_families with topology, meets