awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂
have refine_1 : U ⊆ φ ⁻¹' Z₂
Tactic: refine (closure_minimal ?_ <| hZ₂.preimage hφ).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂
⊢ closure U = φ ⁻¹' Z₂
have refine_2 : ∀ (x : X) (hx : x ∈ φ ⁻¹' Z₂), x ∈ closure U
Tactic: refine (closure_minimal ?_ <| hZ₂.preimage hφ).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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₂
have this₁ : φ x ∈ Z₁ ∪ Z₂
Tactic: have : φ x ∈ Z₁ ∪ Z₂ := (g x).2
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂
⊢ x ∈ φ ⁻¹' Z₂
have refine_1 : ∀ (hφ : φ x ∈ Z₁), x ∈ φ ⁻¹' Z₂
Tactic: rcases this with hφ | hφ
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₂
⊢ x ∈ φ ⁻¹' Z₂
have refine_1₁ : ∀ (hφ : φ x ∈ Z₂), x ∈ φ ⁻¹' Z₂
Tactic: rcases this with hφ | hφ
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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 ∈ closure U
have refine_2 : (φ x).1 ∈ closure U
Tactic: rw [← hφ₁ x]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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),
    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
have 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
Tactic: rcases zorn_superset S this with ⟨E, E_min⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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 : 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
have E_closed : IsClosed E
Tactic: obtain ⟨E_closed, E_surj⟩ := E_min.prop
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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 : 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
have E_surj : X '' E = univ
Tactic: obtain ⟨E_closed, E_surj⟩ := E_min.prop
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
have refine : ∀ (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, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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₀
⊢ E.restrict (π := fun (a : D) ↦ A) X '' E₀ ≠ univ
have contrapose : ∀ (E₀_min : E.restrict (π := fun (a : D) ↦ A) X '' E₀ = univ), E₀ = univ
Tactic: contrapose E₀_min
Cleared hypotheses: E₀_min
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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}
⊢ ∃ (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
have suffices : ∀ C ⊆ S, IsChain (fun (x1 x2 : Set D) ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
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
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
have refine : X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
⊢ X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
have pos : ∀ (hC : Nonempty.{u + 1} (↑C : Type u)), X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
Tactic: by_cases hC : Nonempty C
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
⊢ X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
have neg : ∀ (hC : ¬Nonempty.{u + 1} (↑C : Type u)), X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
Tactic: by_cases hC : Nonempty C
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
have pos : ∀ (a : A), Set.Nonempty.{u} (α := D) ((⋂ (c : (↑C : Type u)), (↑c : Set D)) ∩ fun (a_1 : D) ↦ X a_1 = a)
Tactic: refine eq_univ_of_forall fun a => inter_nonempty_iff_exists_left.mp ?_
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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)
have pos : Directed (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) fun (i : (↑C : Type u)) ↦ (↑i : Set D) ∩ X ⁻¹' {a}
Tactic: refine iInter_inter (ι := C) (X ⁻¹' {a}) _ ▸
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
      ?_ (fun c => ?_) (fun c => IsClosed.isCompact ?_) (fun c => ?_)
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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}
⊢ Set.Nonempty.{u} (α := D) ((⋂ (c : (↑C : Type u)), (↑c : Set D)) ∩ fun (a_1 : D) ↦ X a_1 = a)
have pos₁ : ∀ (c : (↑C : Type u)), ((↑c : Set D) ∩ X ⁻¹' {a}).Nonempty
Tactic: refine iInter_inter (ι := C) (X ⁻¹' {a}) _ ▸
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
      ?_ (fun c => ?_) (fun c => IsClosed.isCompact ?_) (fun c => ?_)
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
⊢ Set.Nonempty.{u} (α := D) ((⋂ (c : (↑C : Type u)), (↑c : Set D)) ∩ fun (a_1 : D) ↦ X a_1 = a)
have pos₂ : ∀ (c : (↑C : Type u)), IsClosed ((↑c : Set D) ∩ X ⁻¹' {a})
Tactic: refine iInter_inter (ι := C) (X ⁻¹' {a}) _ ▸
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
      ?_ (fun c => ?_) (fun c => IsClosed.isCompact ?_) (fun c => ?_)
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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
⊢ Directed (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) fun (i : (↑C : Type u)) ↦ (↑i : Set D) ∩ X ⁻¹' {a}
have C_chain₁ : IsChain (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) C
Tactic: replace C_chain : IsChain (· ⊇ ·) C := C_chain.symm
Cleared hypotheses: C_chain
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
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
⊢ Directed (fun (x1 x2 : Set D) ↦ x1 ⊇ x2) fun (i : (↑C : Type u)) ↦ (↑i : Set D) ∩ X ⁻¹' {a}
have this : ∀ (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}
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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)
⊢ ((↑c : Set D) ∩ X ⁻¹' {a}).Nonempty
have pos : Set.Nonempty (α := A) {a}
Tactic: rw [← image_inter_nonempty_iff, (C_sub c.mem).right, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
have neg : X '' univ = univ
Tactic: rw [@iInter_of_empty _ _ <| not_nonempty_iff.mp hC, image_univ_of_surjective X_surj]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
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
⊢ X '' ⋂ (c : (↑C : Type u)), (↑c : Set D) = univ
have neg₁ : Eq.{u + 1} (α := Set A) univ univ
Tactic: rw [@iInter_of_empty _ _ <| not_nonempty_iff.mp hC, image_univ_of_surjective X_surj]
-- 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 ⊆ closure (ρ '' Gᶜ)ᶜ
have pos : ∀ (G_empty : G = ∅), ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
Tactic: by_cases G_empty : G = ∅
-- 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
pos : ∀ (G_empty : G = ∅), ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
have neg : ∀ (G_empty : ¬G = ∅), ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
Tactic: by_cases G_empty : G = ∅
-- 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 = ∅
a : A
ha : a ∈ ρ '' G
⊢ a ∈ closure (ρ '' Gᶜ)ᶜ
have neg : ∀ (o : Set A), IsOpen o → a ∈ o → (o ∩ (ρ '' Gᶜ)ᶜ).Nonempty
Tactic: rw [mem_closure_iff]
-- 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 = ∅
a : A
ha : a ∈ ρ '' G
N : Set A
N_open : IsOpen N
hN : a ∈ N
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
have neg : ∀ (e : E) (he : e ∈ G) (ha : ρ e ∈ ρ '' G) (hN : ρ e ∈ N), (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
Tactic: rcases (G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩
Cleared hypotheses: a, ha, hN
-- 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
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
have nonempty : (G ∩ ρ ⁻¹' N).Nonempty
Tactic: have nonempty : (G ∩ ρ ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr hN⟩
-- 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
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
have is_open : IsOpen (G ∩ ρ ⁻¹' N)
Tactic: have is_open : IsOpen <| G ∩ ρ ⁻¹' N := hG.inter <| N_open.preimage ρ_cont
-- 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)
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
have ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
Tactic: have ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ :=
      zorn_subset _ (compl_ne_univ.mpr nonempty) is_open.isClosed_compl
-- 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
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
have neg : ∀ (x : A) (hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ), (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
Tactic: rcases nonempty_compl.mpr ne_univ with ⟨x, 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
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
⊢ (N ∩ (ρ '' Gᶜ)ᶜ).Nonempty
have hx' : x ∈ (ρ '' Gᶜ)ᶜ
Tactic: have hx' : x ∈ (ρ '' Gᶜ)ᶜ := fun h => hx <| image_mono (by simp) h