awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen.{u_1} (X := X) (closure ((⇑e.symm : (a : Y) → X) '' U))

Tactic:
ExtremallyDisconnected.open_closure _ (e.symm.isOpen_image.mpr hU)

Premises used: ExtremallyDisconnected.open_closure, Iff.mpr, Homeomorph.symm, Homeomorph.isOpen_image
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen.{u_1} (X := X) (closure ((⇑e.symm : (a : Y) → X) '' U))

Tactic:
exact ExtremallyDisconnected.open_closure _ (e.symm.isOpen_image.mpr hU)

Premises used: ExtremallyDisconnected.open_closure, Iff.mpr, Homeomorph.symm, Homeomorph.isOpen_image
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
_ :
  Membership.mem (γ := Set X) univ x →
    ∀ ⦃y : X⦄,
      Membership.mem (γ := Set X) univ y →
        x ≠ y →
          (fun (x y : X) ↦ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v)
            x y
⊢ Membership.mem (γ := Set X) univ x →
    ∀ ⦃y : X⦄,
      Membership.mem (γ := Set X) univ y →
        x ≠ y →
          (fun (x y : X) ↦ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v)
            x y

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
_ :
  Membership.mem (γ := Set X) univ y →
    x ≠ y →
      (fun (x y : X) ↦ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y
⊢ Membership.mem (γ := Set X) univ y →
    x ≠ y →
      (fun (x y : X) ↦ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
obtain :
  ∀ (U V : Set X) (hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V),
    ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
obtain ⟨U, V, hUV⟩ := T2Space.t2 hxy

Premises used: T2Space.t2
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ IsOpen (closure U)ᶜ

Tactic:
simp only [isOpen_compl_iff, isClosed_closure]

Premises used: isClosed_closure, isOpen_compl_iff
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ univ ⊆ closure U ∪ (closure U)ᶜ

Tactic:
simp only [Set.union_compl_self, Set.subset_univ]

Premises used: Set.subset_univ, Set.union_compl_self
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
refine : y ∈ (closure U)ᶜ
⊢ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
refine ⟨closure U, (closure U)ᶜ, ExtremallyDisconnected.open_closure U hUV.1,
      by simp only [isOpen_compl_iff, isClosed_closure], subset_closure hUV.2.2.1, ?_,
      by simp only [Set.union_compl_self, Set.subset_univ], disjoint_compl_right⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
rw : ¬∀ (o : Set X), IsOpen o → y ∈ o → (o ∩ U).Nonempty
⊢ y ∈ (closure U)ᶜ

Tactic:
rw [Set.mem_compl_iff, mem_closure_iff]

Premises used: mem_closure_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
push : ∃ (o : Set X), IsOpen o ∧ y ∈ o ∧ o ∩ U = ∅
⊢ ¬∀ (o : Set X), IsOpen o → y ∈ o → (o ∩ U).Nonempty

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ∃ (o : Set X), IsOpen o ∧ y ∈ o ∧ o ∩ U = ∅

Tactic:
⟨V, ⟨hUV.2.1, hUV.2.2.2.1, ?_⟩⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
refine : V ∩ U = ∅
⊢ ∃ (o : Set X), IsOpen o ∧ y ∈ o ∧ o ∩ U = ∅

Tactic:
refine ⟨V, ⟨hUV.2.1, hUV.2.2.2.1, ?_⟩⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
rw : Disjoint U V
⊢ V ∩ U = ∅

Tactic:
rw [← Set.disjoint_iff_inter_eq_empty, disjoint_comm]

Premises used: disjoint_comm, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ Disjoint U V

Tactic:
hUV.2.2.2.2

Premises used: And.right
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ Disjoint U V

Tactic:
exact hUV.2.2.2.2

Premises used: And.right
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
⊢ g ∘ s = id

Tactic:
have hs : g ∘ s = id := funext fun z => Classical.choose_spec (g_sur z)
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
⊢ Continuous t

Tactic:
have ht : Continuous t := continuous_of_discreteTopology
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
⊢ Continuous h

Tactic:
have hh : Continuous h := continuous_stoneCechExtend ht
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
⊢ ∃ (h : StoneCech X → Y), Continuous h ∧ g ∘ h = f

Tactic:
⟨h, hh, denseRange_stoneCechUnit.equalizer (hg.comp hh) hf ?_⟩

Premises used: DenseRange.equalizer, Continuous.comp, denseRange_stoneCechUnit, And.intro, Exists.intro
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
refine : (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
⊢ ∃ (h : StoneCech X → Y), Continuous h ∧ g ∘ h = f

Tactic:
refine ⟨h, hh, denseRange_stoneCechUnit.equalizer (hg.comp hh) hf ?_⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
rw : g ∘ h ∘ stoneCechUnit = f ∘ stoneCechUnit
rw₁ : g ∘ t = f ∘ stoneCechUnit
rw₂ : (g ∘ s) ∘ f ∘ stoneCechUnit = f ∘ stoneCechUnit
rw₃ : id ∘ f ∘ stoneCechUnit = f ∘ stoneCechUnit
rw₄ rw₅ : f ∘ stoneCechUnit = f ∘ stoneCechUnit
⊢ (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit

Tactic:
rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]

Premises used: stoneCechExtend_extends, Function.comp_assoc, Function.id_comp
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
⊢ ExtremallyDisconnected X

Tactic:
{ open_closure := fun U hU => ?_ }

Premises used: ExtremallyDisconnected.mk
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
refine : ∀ (U : Set X) (hU : IsOpen U), IsOpen (closure U)
⊢ ExtremallyDisconnected X

Tactic:
refine { open_closure := fun U hU => ?_ }
-- 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₂
x : X × Bool
hx₁ : x ∈ Z₁
hx₂ : x ∈ Z₂
⊢ False

Tactic:
cases hx₁.2.symm.trans hx₂.2

Premises used: And.right, Eq.symm, Eq.trans
-- 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₂
⊢ Disjoint Z₁ Z₂

Tactic:
have hZ₁₂ : Disjoint Z₁ Z₂ := disjoint_left.2 fun x hx₁ hx₂ => by cases hx₁.2.symm.trans hx₂.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₂
⊢ IsClosed Z₁

Tactic:
have hZ₁ : IsClosed Z₁ := hU.isClosed_compl.prod (T1Space.t1 _)
-- 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₁
⊢ IsClosed Z₂

Tactic:
have hZ₂ : IsClosed Z₂ := isClosed_closure.prod (T1Space.t1 false)
-- 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₂
⊢ IsClosed Z

Tactic:
have hZ : IsClosed Z := hZ₁.union hZ₂
-- 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)
⊢ Continuous f

Tactic:
have f_cont : Continuous f := continuous_fst.comp continuous_subtype_val
-- 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
x : X
pos : ∀ (hx : x ∈ U), ∃ (a : (↑Z : Type u)), f a = x
neg : ∀ (hx : x ∉ U), ∃ (a : (↑Z : Type u)), f a = x
⊢ ∃ (a : (↑Z : Type u)), f a = x

Tactic:
by_cases hx : x ∈ U
-- 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
x : X
hx : x ∈ U
⊢ ∃ (a : (↑Z : Type u)), f a = x

Tactic:
⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩

Premises used: Set.mem_singleton, subset_closure, Prod.mk, Subtype.mk, And.intro, Exists.intro, Bool.false, Or.inr, rfl
-- 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
x : X
hx : x ∈ U
⊢ ∃ (a : (↑Z : Type u)), f a = x

Tactic:
exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩
-- 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
x : X
hx : x ∉ U
⊢ ∃ (a : (↑Z : Type u)), f a = x

Tactic:
⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩

Premises used: Set.mem_singleton, Prod.mk, Subtype.mk, Bool.true, And.intro, Exists.intro, Or.inl, rfl
-- 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
x : X
hx : x ∉ U
⊢ ∃ (a : (↑Z : Type u)), f a = x

Tactic:
exact ⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩
-- 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
⊢ Surjective f

Tactic:
have f_sur : Surjective f := by
    intro x
    by_cases hx : x ∈ U
    · exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩
    · exact ⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩
-- 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
⊢ CompactSpace.{u} (↑Z : Type u)

Tactic:
haveI : CompactSpace Z := isCompact_iff_compactSpace.mp hZ.isCompact
-- 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)
obtain : ∀ (g : X → (↑Z : Type u)) (hg : Continuous g) (g_sec : f ∘ g = id), IsOpen (closure U)
⊢ IsOpen (closure U)

Tactic:
obtain ⟨g, hg, g_sec⟩ := h continuous_id f_cont f_sur

Premises used: continuous_id
-- 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
⊢ Continuous φ

Tactic:
have hφ : Continuous φ := continuous_subtype_val.comp hg
-- 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 φ
⊢ ∀ (x : X), (φ x).1 = x

Tactic:
have hφ₁ : ∀ x, (φ x).1 = x := congr_fun g_sec
-- 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 : IsClosed (g ⁻¹' Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z₁ ∪ Z₂) ⁻¹' Z₁)
rw₁ : (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅
⊢ IsOpen (closure U)

Tactic:
rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl,
      ← preimage_subtype_coe_eq_compl Subset.rfl]

Premises used: Set.preimage_comp, Set.Subset.rfl, Set.preimage_subtype_coe_eq_compl, Set.preimage_compl, isClosed_compl_iff