awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pos : Directed (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) fun (i : (↑C : Type u)) ↦ (↑i : Set D) ∩ X ⁻¹' {a}
pos₁ : ∀ (c : (↑C : Type u)), ((↑c : Set D) ∩ X ⁻¹' {a}).Nonempty
pos₂ pos₃ : ∀ (c : (↑C : Type u)), IsClosed ((↑c : Set D) ∩ X ⁻¹' {a})
⊢ Set.Nonempty.{u} (α := D) ((⋂ (c : (↑C : Type u)), (↑c : Set D)) ∩ fun (a_1 : D) ↦ X a_1 = a)

Tactic:
refine iInter_inter (ι := C) (X ⁻¹' {a}) _ ▸
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
      ?_ (fun c => ?_) (fun c => IsClosed.isCompact ?_) (fun c => ?_)
-- 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
⊢ IsChain (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) C

Tactic:
replace C_chain : IsChain (· ⊇ ·) C := C_chain.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}
C : Set (Set D)
C_sub : C ⊆ S
hC : Nonempty.{u + 1} (↑C : Type u)
a : A
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) C
⊢ ∀ (s t : Set D), s ⊇ t → s ∩ X ⁻¹' {a} ⊇ t ∩ X ⁻¹' {a}

Tactic:
have : ∀ s t : Set D, s ⊇ t → _ ⊇ _ := fun _ _ => inter_subset_inter_left <| X ⁻¹' {a}
-- 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
hC : Nonempty.{u + 1} (↑C : Type u)
a : A
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) C
this : ∀ (s t : Set D), s ⊇ t → s ∩ X ⁻¹' {a} ⊇ t ∩ X ⁻¹' {a}
⊢ Directed (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) fun (i : (↑C : Type u)) ↦ (↑i : Set D) ∩ X ⁻¹' {a}

Tactic:
(directedOn_iff_directed.mp C_chain.directedOn).mono_comp (· ⊇ ·) this

Premises used: Directed.mono_comp, IsChain.directedOn, directedOn_iff_directed, Iff.mp, 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}
C : Set (Set D)
C_sub : C ⊆ S
hC : Nonempty.{u + 1} (↑C : Type u)
a : A
C_chain : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) C
this : ∀ (s t : Set D), s ⊇ t → s ∩ X ⁻¹' {a} ⊇ t ∩ X ⁻¹' {a}
⊢ Directed (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) fun (i : (↑C : Type u)) ↦ (↑i : Set D) ∩ X ⁻¹' {a}

Tactic:
exact (directedOn_iff_directed.mp C_chain.directedOn).mono_comp (· ⊇ ·) this

Premises used: Directed.mono_comp, IsChain.directedOn, directedOn_iff_directed, Iff.mp, 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}
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
c : (↑C : Type u)
pos : Set.Nonempty (α := A) {a}
⊢ ((↑c : Set D) ∩ X ⁻¹' {a}).Nonempty

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

Premises used: Set.univ_inter, And.right, Subtype.mem, Set.image_inter_nonempty_iff
-- 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
c : (↑C : Type u)
⊢ Set.Nonempty (α := A) {a}

Tactic:
singleton_nonempty a

Premises used: Set.singleton_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)
a : A
c : (↑C : Type u)
⊢ Set.Nonempty (α := A) {a}

Tactic:
exact singleton_nonempty a

Premises used: Set.singleton_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)
a : A
c : (↑C : Type u)
⊢ IsClosed ((↑c : Set D) ∩ X ⁻¹' {a})

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

Premises used: T1Space.t1, And.left, Subtype.mem, IsClosed.preimage, IsClosed.inter
-- 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
c : (↑C : Type u)
⊢ IsClosed ((↑c : Set D) ∩ X ⁻¹' {a})

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

Premises used: T1Space.t1, And.left, Subtype.mem, IsClosed.preimage, IsClosed.inter
-- 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)
neg : X '' univ = univ
neg₁ neg₂ : Eq.{u + 1} (α := Set A) univ univ
⊢ X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ

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

Premises used: Set.iInter_of_empty, not_nonempty_iff, Set.image_univ_of_surjective, Iff.mp
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
pos : ∀ (G_empty : G = ∅), ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
neg : ∀ (G_empty : ¬G = ∅), ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ

Tactic:
by_cases G_empty : G = ∅
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : G = ∅
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ

Tactic:
simpa only [G_empty, image_empty] using empty_subset _

Premises used: Set.empty_subset, Set.image_empty
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
neg : ∀ (o : Set A), IsOpen o → a ∈ o → (o ∩ (ρ '' Gᶜ)ᶜ).Nonempty
⊢ a ∈ closure (ρ '' Gᶜ)ᶜ

Tactic:
rw [mem_closure_iff]

Premises used: mem_closure_iff
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
N : Set A
N_open : IsOpen N
hN : a ∈ N
neg : ∀ (e : E) (he : e ∈ G) (ha : ρ e ∈ ρ '' G) (hN : ρ e ∈ N), (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty

Tactic:
rcases (G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩

Premises used: Set.mem_image, Iff.mp, rfl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
⊢ (G ∩ ρ ⁻¹' N).Nonempty

Tactic:
have nonempty : (G ∩ ρ ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr hN⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
⊢ IsOpen (G ∩ ρ ⁻¹' N)

Tactic:
have is_open : IsOpen <| G ∩ ρ ⁻¹' N := hG.inter <| N_open.preimage ρ_cont
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
⊢ ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ

Tactic:
have ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ :=
      zorn_subset _ (compl_ne_univ.mpr nonempty) is_open.isClosed_compl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
neg : ∀ (x : A) (hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ), (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty

Tactic:
rcases nonempty_compl.mpr ne_univ with ⟨x, hx⟩

Premises used: Iff.mpr, Set.nonempty_compl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
h : x ∈ ρ '' Gᶜ
⊢ Gᶜ ⊆ (G ∩ ρ ⁻¹' N)ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
⊢ x ∈ (ρ '' Gᶜ)ᶜ

Tactic:
have hx' : x ∈ (ρ '' Gᶜ)ᶜ := fun h => hx <| image_mono (by simp) h
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : x ∈ (ρ '' Gᶜ)ᶜ
neg : ∀ (y : E) (hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ) (hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ), (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty

Tactic:
rcases ρ_surj x with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ y ∈ G ∩ ρ ⁻¹' N

Tactic:
simpa using mt (mem_image_of_mem ρ) <| mem_compl hx

Premises used: mt, Set.mem_image_of_mem, Set.mem_compl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ y ∈ G ∩ ρ ⁻¹' N

Tactic:
have hy : y ∈ G ∩ ρ ⁻¹' N := by simpa using mt (mem_image_of_mem ρ) <| mem_compl hx
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
hy : y ∈ G ∩ ρ ⁻¹' N
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty

Tactic:
⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩

Premises used: Set.mem_inter, Set.Nonempty, Exists.intro, Iff.mp, Set.mem_of_mem_inter_right, Set.mem_preimage
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
hy : y ∈ G ∩ ρ ⁻¹' N
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty

Tactic:
exact ⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
U₁ U₂ : Set A
h : Disjoint U₁ U₂
hU₁ : IsOpen U₁
hU₂ : IsOpen U₂
⊢ Disjoint (closure U₁) (closure U₂)

Tactic:
(h.closure_right hU₁).closure_left <| open_closure U₂ hU₂

Premises used: ExtremallyDisconnected.open_closure, Disjoint.closure_right, Disjoint.closure_left
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
by_contra : ∀ (hx : ¬x₁ = x₂), False
⊢ x₁ = x₂

Tactic:
by_contra hx
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
rcases :
  ∀ (G₁ G₂ : Set E) (G₁_open : IsOpen G₁) (G₂_open : IsOpen G₂) (hx₁ : x₁ ∈ G₁) (hx₂ : x₂ ∈ G₂) (disj : Disjoint G₁ G₂),
    False
⊢ False

Tactic:
rcases t2_separation hx with ⟨G₁, G₂, G₁_open, G₂_open, hx₁, hx₂, disj⟩

Premises used: t2_separation
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
⊢ IsCompact G₁ᶜ

Tactic:
have G₁_comp : IsCompact G₁ᶜ := IsClosed.isCompact G₁_open.isClosed_compl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
⊢ IsCompact G₂ᶜ

Tactic:
have G₂_comp : IsCompact G₂ᶜ := IsClosed.isCompact G₂_open.isClosed_compl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
⊢ IsOpen (ρ '' G₁ᶜ)ᶜ

Tactic:
have G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ := (G₁_comp.image ρ_cont).isClosed.isOpen_compl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
⊢ IsOpen (ρ '' G₂ᶜ)ᶜ

Tactic:
have G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ := (G₂_comp.image ρ_cont).isClosed.isOpen_compl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
rw : (ρ '' G₁ᶜ)ᶜ ∩ (ρ '' G₂ᶜ)ᶜ = ∅
rw₁ : (ρ '' G₁ᶜ ∪ ρ '' G₂ᶜ)ᶜ = ∅
rw₂ : (ρ '' (G₁ᶜ ∪ G₂ᶜ))ᶜ = ∅
rw₃ : (ρ '' (G₁ ∩ G₂)ᶜ)ᶜ = ∅
rw₄ : (ρ '' ∅ᶜ)ᶜ = ∅
rw₅ : (ρ '' univ)ᶜ = ∅
rw₆ : ρ '' univ = univ
rw₇ rw₈ : Eq.{u + 1} (α := Set A) univ univ
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ

Tactic:
rw [disjoint_iff_inter_eq_empty, ← compl_union, ← image_union, ← compl_inter,
      disjoint_iff_inter_eq_empty.mp disj, compl_empty, compl_empty_iff,
      image_univ_of_surjective ρ_surj]

Premises used: Set.compl_union, Set.compl_inter, Set.disjoint_iff_inter_eq_empty, Set.compl_empty_iff, Set.image_univ_of_surjective, Iff.mp, Set.compl_empty, Set.image_union
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ

Tactic:
have disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ := by
    rw [disjoint_iff_inter_eq_empty, ← compl_union, ← image_union, ← compl_inter,
      disjoint_iff_inter_eq_empty.mp disj, compl_empty, compl_empty_iff,
      image_univ_of_surjective ρ_surj]
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
⊢ Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)

Tactic:
have disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ) :=
    disjoint_closure_of_disjoint_isOpen disj' G₁_open' G₂_open'
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)
⊢ ρ x₁ ∈ closure (ρ '' G₁ᶜ)ᶜ

Tactic:
have hx₁' := image_subset_closure_compl_image_compl_of_isOpen ρ_cont ρ_surj zorn_subset G₁_open <|
    mem_image_of_mem ρ hx₁