awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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ᶜ)ᶜ
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
have neg : ∀ (y : E) (hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ) (hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ), (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
Tactic: rcases ρ_surj x with ⟨y, rfl⟩
Cleared hypotheses: x, hx, hx'
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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ᶜ)ᶜ
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
have hy : y ∈ G ∩ ρ ⁻¹' N
Tactic: have hy : y ∈ G ∩ ρ ⁻¹' N := by simpa using mt (mem_image_of_mem ρ) <| mem_compl hx
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂
⊢ x₁ = x₂
have by_contra : ∀ (hx : ¬x₁ = x₂), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂
⊢ False
have rcases : ∀ (G₁ G₂ : Set E) (G₁_open : IsOpen G₁) (G₂_open : IsOpen G₂) (hx₁ : x₁ ∈ G₁) (hx₂ : x₂ ∈ G₂) (disj : Disjoint G₁ G₂),
  False
Tactic: rcases t2_separation hx with ⟨G₁, G₂, G₁_open, G₂_open, hx₁, hx₂, disj⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₂
⊢ False
have G₁_comp : IsCompact G₁ᶜ
Tactic: have G₁_comp : IsCompact G₁ᶜ := IsClosed.isCompact G₁_open.isClosed_compl
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₁ᶜ
⊢ False
have G₂_comp : IsCompact G₂ᶜ
Tactic: have G₂_comp : IsCompact G₂ᶜ := IsClosed.isCompact G₂_open.isClosed_compl
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₂ᶜ
⊢ False
have G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
Tactic: have G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ := (G₁_comp.image ρ_cont).isClosed.isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₁ᶜ)ᶜ
⊢ False
have G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
Tactic: have G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ := (G₂_comp.image ρ_cont).isClosed.isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂ᶜ)ᶜ
have rw : (ρ '' 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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂ᶜ)ᶜ = ∅
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
have rw₁ : (ρ '' 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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂ᶜ)ᶜ = ∅
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
have rw₂ : (ρ '' (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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂ᶜ))ᶜ = ∅
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
have rw₃ : (ρ '' (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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂)ᶜ)ᶜ = ∅
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
have rw₄ : (ρ '' ∅ᶜ)ᶜ = ∅
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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₄ : (ρ '' ∅ᶜ)ᶜ = ∅
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
have rw₅ : (ρ '' univ)ᶜ = ∅
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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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)ᶜ = ∅
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
have rw₆ : ρ '' univ = univ
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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
⊢ Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
have rw₇ : Eq.{u + 1} (α := Set A) univ univ
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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₂ᶜ)ᶜ
⊢ False
have disj' : 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]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₂ᶜ)ᶜ
⊢ False
have disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)
Tactic: have disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ) :=
    disjoint_closure_of_disjoint_isOpen disj' G₁_open' G₂_open'
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₂ᶜ)ᶜ)
⊢ False
have hx₁' : ρ 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₁
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₂ᶜ)ᶜ)
hx₁' : ρ x₁ ∈ closure (ρ '' G₁ᶜ)ᶜ
⊢ False
have hx₂' : ρ 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₂
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
have D_comp : CompactSpace.{u} (↑D : Type u)
Tactic: have D_comp : CompactSpace D := isCompact_iff_compactSpace.mp
    (isClosed_eq (φ_cont.comp continuous_fst) (f_cont.comp continuous_snd)).isCompact
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
have X₁_cont : Continuous X₁
Tactic: have X₁_cont : Continuous X₁ := continuous_fst.comp continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
have X₁_surj : Surjective X₁
Tactic: have X₁_surj : X₁.Surjective := fun a => ⟨⟨⟨a, _⟩, (f_surj <| φ a).choose_spec.symm⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
have rcases : ∀ (E : Set (↑D : Type u)),
  CompactSpace.{u} (↑E : Type u) →
    ∀ (E_onto : X₁ '' E = univ)
      (E_min :
        ∀ (E₀ : Set (↑E : Type u)),
          E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ),
      ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
Tactic: rcases exists_compact_surjective_zorn_subset X₁_cont X₁_surj with ⟨E, _, E_onto, E_min⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
have ρ_cont : Continuous ρ
Tactic: have ρ_cont : Continuous ρ := X₁_cont.continuousOn.restrict
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
a : A
⊢ ∃ (a_1 : (↑E : Type u)), ρ a_1 = a
have rcases : ∀ (d : (↑D : Type u)) (hd : d ∈ E), ∃ (a : (↑E : Type u)), ρ a = X₁ d
Tactic: rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
have ρ_surj : Surjective ρ
Tactic: have ρ_surj : ρ.Surjective := fun a => by
    rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩; exact ⟨⟨d, hd⟩, rfl⟩