-- 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:
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})

Tactic:
all_goals exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage π_cont

Result:
no goals

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
⊢ π '' ⋂ c, ↑c = univ

Tactic:
refine eq_univ_of_forall fun a => inter_nonempty_iff_exists_left.mp ?_

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

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, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Tactic:
refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩

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₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Proof state:
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})

Tactic:
exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage π_cont

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₀_closed : IsClosed E₀
E₀_min : E.restrict π '' E₀ = univ
⊢ E₀ = univ

Tactic:
exact eq_univ_of_image_val_eq <|
  E_min.eq_of_subset ⟨E₀_closed.trans E_closed, image_image_val_eq_restrict_image ▸ E₀_min⟩
    image_val_subset

Result:
no goals

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
⊢ (↑c ∩ π ⁻¹' {a}).Nonempty

Tactic:
rw [← image_inter_nonempty_iff, (C_sub c.mem).right, univ_inter]

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

Proof state:
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

Tactic:
obtain ⟨E_closed, E_surj⟩ := E_min.prop

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, 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 π
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
⊢ π '' ⋂ c, ↑c = univ

Tactic:
by_cases hC : Nonempty C

Result:
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
⊢ π '' ⋂ c, ↑c = univ

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