-- Mathlib/Topology/ExtremallyDisconnected.lean
/-- Lemma 2.4 in [Gleason, *Projective topological spaces*][gleason1958]:
a continuous surjection $\pi$ from a compact space $D$ to a Fréchet space $A$ restricts to
a compact subset $E$ of $D$, such that $\pi$ maps $E$ onto $A$ and satisfies the
"Zorn subset condition", where $\pi(E_0) \ne A$ for any proper closed subset $E_0 \subsetneq E$. -/
lemma exists_compact_surjective_zorn_subset [T1Space A] [CompactSpace D] {π : D → A}
    (π_cont : Continuous π) (π_surj : π.Surjective) : ∃ E : Set D, CompactSpace E ∧ π '' E = univ ∧
    ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Proof state:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
⊢ ∃ E, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Tactic:
let S : Set <| Set D := {E : Set D | IsClosed E ∧ π '' E = univ}

Result:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
⊢ ∃ E, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Proof state:
case pos
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
⊢ ((⋂ c, ↑c) ∩ fun a_1 => π a_1 = a).Nonempty

Tactic:
refine iInter_inter (ι := C) (π ⁻¹' {a}) _ ▸
  IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
  ?_ (fun c => ?_) (fun c => IsClosed.isCompact ?_) (fun c => ?_)

Result:
case pos.refine_1
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
⊢ Directed (fun x1 x2 => x1 ⊇ x2) fun i => ↑i ∩ π ⁻¹' {a}

case pos.refine_2
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ (↑c ∩ π ⁻¹' {a}).Nonempty

case pos.refine_3
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ π ⁻¹' {a})

case pos.refine_4
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ π ⁻¹' {a})

Proof state:
case pos.refine_1
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
hC : Nonempty ↑C
a : A
C_chain : IsChain (fun x1 x2 => x1 ⊇ x2) C
⊢ Directed (fun x1 x2 => x1 ⊇ x2) fun i => ↑i ∩ π ⁻¹' {a}

Tactic:
have : ∀ s t : Set D, s ⊇ t → _ ⊇ _ := fun _ _ => inter_subset_inter_left <| π ⁻¹' {a}

Result:
case pos.refine_1
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
hC : Nonempty ↑C
a : A
C_chain : IsChain (fun x1 x2 => x1 ⊇ x2) C
this : ∀ (s t : Set D), s ⊇ t → s ∩ π ⁻¹' {a} ⊇ t ∩ π ⁻¹' {a}
⊢ Directed (fun x1 x2 => x1 ⊇ x2) fun i => ↑i ∩ π ⁻¹' {a}

Proof state:
case neg
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
hC : ¬Nonempty ↑C
⊢ π '' ⋂ c, ↑c = univ

Tactic:
rw [@iInter_of_empty _ _ <| not_nonempty_iff.mp hC, image_univ_of_surjective π_surj]

Result:
no goals

Proof state:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
⊢ ∃ E, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Tactic:
rcases zorn_superset S this with ⟨E, E_min⟩

Result:
case intro
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x => x ∈ S) E
⊢ ∃ E, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Proof state:
case pos.refine_2
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ {a}.Nonempty

Tactic:
exact singleton_nonempty a

Result:
no goals

Proof state:
case intro.intro
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x => x ∈ S) E
E_closed : IsClosed E
E_surj : π '' E = univ
E₀ : Set ↑E
E₀_min : E₀ ≠ univ
E₀_closed : IsClosed E₀
⊢ E.restrict π '' E₀ ≠ univ

Tactic:
contrapose! E₀_min

Result:
case intro.intro
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x => x ∈ S) E
E_closed : IsClosed E
E_surj : π '' E = univ
E₀ : Set ↑E
E₀_closed : IsClosed E₀
E₀_min : E.restrict π '' E₀ = univ
⊢ E₀ = univ