awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this_1 : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ IsClosed (g ⁻¹' Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z₁ ∪ Z₂) ⁻¹' Z₁)

Tactic:
hZ₁.preimage hφ

Premises used: Set.Mem, setOf, Set.prod, Set.preimage, IsClosed.preimage
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this_1 : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ IsClosed (g ⁻¹' Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z₁ ∪ Z₂) ⁻¹' Z₁)

Tactic:
exact hZ₁.preimage hφ

Premises used: IsClosed.preimage
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this_1 : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
rw : (Z₁ ∪ Z₂) ∩ ∅ = ∅
rw₁ rw₂ : Eq.{u + 1} (α := Set (X × Bool)) ∅ ∅
⊢ (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅

Tactic:
rw [hZ₁₂.inter_eq, inter_empty]

Premises used: Set.inter_empty, Disjoint.inter_eq
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
suffices : closure U = φ ⁻¹' Z₂
⊢ IsOpen (closure U)

Tactic:
suffices closure U = φ ⁻¹' Z₂ by
    rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl,
      ← preimage_subtype_coe_eq_compl Subset.rfl]
    · exact hZ₁.preimage hφ
    · rw [hZ₁₂.inter_eq, inter_empty]
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
⊢ closure U = φ ⁻¹' Z₂

Tactic:
(closure_minimal ?_ <| hZ₂.preimage hφ).antisymm fun x hx => ?_

Premises used: closure_minimal, HasSubset.Subset.antisymm, IsClosed.preimage
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
refine_1 : U ⊆ φ ⁻¹' Z₂
refine_2 : ∀ (x : X) (hx : x ∈ φ ⁻¹' Z₂), x ∈ closure U
⊢ closure U = φ ⁻¹' Z₂

Tactic:
refine (closure_minimal ?_ <| hZ₂.preimage hφ).antisymm fun x hx => ?_

Premises used: closure_minimal, HasSubset.Subset.antisymm, IsClosed.preimage
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ U
⊢ φ x ∈ Z₁ ∪ Z₂

Tactic:
have : φ x ∈ Z₁ ∪ Z₂ := (g x).2
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this_1 : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ U
this : φ x ∈ Z₁ ∪ Z₂
refine_1 : ∀ (hφ : φ x ∈ Z₁), x ∈ φ ⁻¹' Z₂
refine_1₁ : ∀ (hφ : φ x ∈ Z₂), x ∈ φ ⁻¹' Z₂
⊢ x ∈ φ ⁻¹' Z₂

Tactic:
rcases this with hφ | hφ
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ_1 : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ U
hφ : φ x ∈ Z₁
⊢ x ∈ φ ⁻¹' Z₂

Tactic:
exact ((hφ₁ x ▸ hφ.1) hx).elim
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ_1 : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ U
hφ : φ x ∈ Z₂
⊢ x ∈ φ ⁻¹' Z₂

Tactic:
hφ

Premises used: Set.Mem, setOf, Set.prod, Set.preimage
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ_1 : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ U
hφ : φ x ∈ Z₂
⊢ x ∈ φ ⁻¹' Z₂

Tactic:
exact hφ
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ φ ⁻¹' Z₂
refine_2 : (φ x).1 ∈ closure U
⊢ x ∈ closure U

Tactic:
rw [← hφ₁ x]
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ φ ⁻¹' Z₂
⊢ (φ x).1 ∈ closure U

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ φ ⁻¹' Z₂
⊢ (φ x).1 ∈ closure U

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
rcases :
  ∀ (E : Set D) (E_min : Minimal (fun (x : Set D) ↦ x ∈ S) E),
    ∃ (E : Set D),
      CompactSpace.{u} (↑E : Type u) ∧
        X '' E = univ ∧
          ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : D) ↦ A) X '' E₀ ≠ univ
⊢ ∃ (E : Set D),
    CompactSpace.{u} (↑E : Type u) ∧
      X '' E = univ ∧
        ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : D) ↦ A) X '' E₀ ≠ univ

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

Premises used: zorn_superset
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun (x : Set D) ↦ x ∈ S) E
⊢ IsClosed E

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

Premises used: Minimal.prop
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun (x : Set D) ↦ x ∈ S) E
E_closed : IsClosed E
⊢ X '' E = univ

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

Premises used: Minimal.prop
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun (x : Set D) ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
⊢ ∃ (E : Set D),
    CompactSpace.{u} (↑E : Type u) ∧
      X '' E = univ ∧
        ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : D) ↦ A) X '' E₀ ≠ univ

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

Premises used: isCompact_iff_compactSpace, And.intro, IsClosed.isCompact, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun (x : Set D) ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
refine : ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : D) ↦ A) X '' E₀ ≠ univ
⊢ ∃ (E : Set D),
    CompactSpace.{u} (↑E : Type u) ∧
      X '' E = univ ∧
        ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : D) ↦ A) X '' E₀ ≠ univ

Tactic:
refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun (x : Set D) ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
E₀ : Set (↑E : Type u)
E₀_min : E₀ ≠ univ
E₀_closed : IsClosed E₀
contrapose : ∀ (E₀_min : E.restrict (π := fun (a : D) ↦ A) X '' E₀ = univ), E₀ = univ
⊢ E.restrict (π := fun (a : D) ↦ A) X '' E₀ ≠ univ

Tactic:
contrapose E₀_min
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun (x : Set D) ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
E₀ : Set (↑E : Type u)
E₀_closed : IsClosed E₀
E₀_min : E.restrict (π := fun (a : D) ↦ A) X '' E₀ = univ
⊢ E₀ = univ

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

Premises used: Eq.rec, Set.image_val_subset, Minimal.eq_of_subset, Set.eq_univ_of_image_val_eq, And.intro, IsClosed.trans, Set.image_image_val_eq_restrict_image, Eq.symm
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun (x : Set D) ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
E₀ : Set (↑E : Type u)
E₀_closed : IsClosed E₀
E₀_min : E.restrict (π := fun (a : D) ↦ A) X '' 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

Premises used: Eq.rec, Set.image_val_subset, Minimal.eq_of_subset, Set.eq_univ_of_image_val_eq, And.intro, IsClosed.trans, Set.image_image_val_eq_restrict_image, Eq.symm
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
suffices : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
⊢ ∃ (E : Set D),
    CompactSpace.{u} (↑E : Type u) ∧
      X '' E = univ ∧
        ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : D) ↦ A) X '' E₀ ≠ univ

Tactic:
suffices ∀ (C : Set <| Set D) (_ : C ⊆ S) (_ : IsChain (· ⊆ ·) C), ∃ s ∈ S, ∀ c ∈ C, s ⊆ c by
    rcases zorn_superset S this with ⟨E, E_min⟩
    obtain ⟨E_closed, E_surj⟩ := E_min.prop
    refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
    intro E₀ E₀_min E₀_closed
    contrapose E₀_min
    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
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C
⊢ ∃ s ∈ S, ∀ c ∈ C, s ⊆ c

Tactic:
⟨iInter (fun c : C => c), ⟨isClosed_iInter fun ⟨_, h⟩ => (C_sub h).left, ?_⟩,
    fun c hc _ h => mem_iInter.mp h ⟨c, hc⟩⟩

Premises used: Set.iInter, Set.mem_iInter, _private.0.exists_compact_surjective_zorn_subset.match_1, Subtype.mk, IsClosed, And.left, And.intro, Exists.intro, Iff.mp, Subtype.val, isClosed_iInter
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C
refine : X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
⊢ ∃ s ∈ S, ∀ c ∈ C, s ⊆ c

Tactic:
refine ⟨iInter (fun c : C => c), ⟨isClosed_iInter fun ⟨_, h⟩ => (C_sub h).left, ?_⟩,
    fun c hc _ h => mem_iInter.mp h ⟨c, hc⟩⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C
pos : ∀ (hC : Nonempty.{u + 1} (↑C : Type u)), X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
neg : ∀ (hC : ¬Nonempty.{u + 1} (↑C : Type u)), X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
⊢ X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ

Tactic:
by_cases hC : Nonempty C

Premises used: Set.Elem, Nonempty
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C
hC : Nonempty.{u + 1} (↑C : Type u)
⊢ X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ

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

Premises used: Set.eq_univ_of_forall, Iff.mp, Set.inter_nonempty_iff_exists_left
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C
hC : Nonempty.{u + 1} (↑C : Type u)
pos : ∀ (a : A), Set.Nonempty.{u} (α := D) ((⋂ (c : (↑C : Type u)), (↑c : Set D)) ∩ fun (a_1 : D) ↦ X a_1 = a)
⊢ X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ

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

Premises used: Set.eq_univ_of_forall, Iff.mp, Set.inter_nonempty_iff_exists_left
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A D : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace D
inst_2 : T1Space A
inst_3 : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E : Set D | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C
hC : Nonempty.{u + 1} (↑C : Type u)
a : A
⊢ Set.Nonempty.{u} (α := D) ((⋂ (c : (↑C : Type u)), (↑c : Set D)) ∩ fun (a_1 : D) ↦ X a_1 = a)

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

Premises used: Set.Mem, setOf, Eq.rec, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, Set.iInter_inter, Set.preimage, IsClosed.isCompact, Set.singleton, Singleton.singleton, Eq.symm