[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
⊢ IsTotallySeparated univ
[PROOFSTEP]
intro x _ y _ hxy
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
[PROOFSTEP]
obtain ⟨U, V, hUV⟩ := T2Space.t2 x y hxy
[GOAL]
case intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
[PROOFSTEP]
use closure U
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ∃ v, IsOpen (closure U) ∧ IsOpen v ∧ x ∈ closure U ∧ y ∈ v ∧ univ ⊆ closure U ∪ v ∧ Disjoint (closure U) v
[PROOFSTEP]
use(closure U)ᶜ
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ IsOpen (closure U) ∧
    IsOpen (closure U)ᶜ ∧
      x ∈ closure U ∧ y ∈ (closure U)ᶜ ∧ univ ⊆ closure U ∪ (closure U)ᶜ ∧ Disjoint (closure U) (closure U)ᶜ
[PROOFSTEP]
refine
  ⟨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⟩
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ IsOpen (closure U)ᶜ
[PROOFSTEP]
simp only [isOpen_compl_iff, isClosed_closure]
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ univ ⊆ closure U ∪ (closure U)ᶜ
[PROOFSTEP]
simp only [Set.union_compl_self, Set.subset_univ]
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ y ∈ (closure U)ᶜ
[PROOFSTEP]
simp only [Set.mem_compl_iff]
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ¬y ∈ closure U
[PROOFSTEP]
rw [mem_closure_iff]
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
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 → Set.Nonempty (o ∩ U)
[PROOFSTEP]
push_neg
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ∃ o, IsOpen o ∧ y ∈ o ∧ ¬Set.Nonempty (o ∩ U)
[PROOFSTEP]
refine' ⟨V, ⟨hUV.2.1, hUV.2.2.2.1, _⟩⟩
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ¬Set.Nonempty (V ∩ U)
[PROOFSTEP]
rw [Set.nonempty_iff_ne_empty]
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ¬V ∩ U ≠ ∅
[PROOFSTEP]
simp only [not_not]
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ V ∩ U = ∅
[PROOFSTEP]
rw [← Set.disjoint_iff_inter_eq_empty, disjoint_comm]
[GOAL]
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ Disjoint U V
[PROOFSTEP]
exact hUV.2.2.2.2
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ CompactT2.Projective (StoneCech X)
[PROOFSTEP]
intro Y Z _tsY _tsZ _csY _t2Y _csZ _csZ f g hf hg g_sur
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let s : Z → Y := fun z => Classical.choose <| g_sur z
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : 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 => choose (_ : ∃ a, g a = z)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have hs : g ∘ s = id := funext fun z => Classical.choose_spec (g_sur z)
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : 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 => choose (_ : ∃ a, g a = z)
hs : g ∘ s = id
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let t := s ∘ f ∘ stoneCechUnit
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : 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 => choose (_ : ∃ a, g a = z)
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have ht : Continuous t := continuous_of_discreteTopology
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : 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 => choose (_ : ∃ a, g a = z)
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let h : StoneCech X → Y := stoneCechExtend ht
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : 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 => choose (_ : ∃ a, g a = z)
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have hh : Continuous h := continuous_stoneCechExtend ht
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : 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 => choose (_ : ∃ a, g a = z)
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
refine' ⟨h, hh, denseRange_stoneCechUnit.equalizer (hg.comp hh) hf _⟩
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : 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 => choose (_ : ∃ a, g a = z)
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
⊢ (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
[PROOFSTEP]
rw [comp.assoc, stoneCechExtend_extends ht, ← comp.assoc, hs, comp.left_id]
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
⊢ ExtremallyDisconnected X
[PROOFSTEP]
refine' { open_closure := fun U hU => _ }
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
⊢ IsOpen (closure U)
[PROOFSTEP]
let Z₁ : Set (X × Bool) := Uᶜ ×ˢ { true }
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
⊢ IsOpen (closure U)
[PROOFSTEP]
let Z₂ : Set (X × Bool) := closure U ×ˢ { false }
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
⊢ IsOpen (closure U)
[PROOFSTEP]
let Z : Set (X × Bool) := Z₁ ∪ Z₂
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
⊢ IsOpen (closure U)
[PROOFSTEP]
have hZ₁₂ : Disjoint Z₁ Z₂ := disjoint_left.2 fun x hx₁ hx₂ => by cases hx₁.2.symm.trans hx₂.2
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
x : X × Bool
hx₁ : x ∈ Z₁
hx₂ : x ∈ Z₂
⊢ False
[PROOFSTEP]
cases hx₁.2.symm.trans hx₂.2
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
⊢ IsOpen (closure U)
[PROOFSTEP]
have hZ₁ : IsClosed Z₁ := hU.isClosed_compl.prod (T1Space.t1 _)
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
⊢ IsOpen (closure U)
[PROOFSTEP]
have hZ₂ : IsClosed Z₂ := isClosed_closure.prod (T1Space.t1 false)
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
⊢ IsOpen (closure U)
[PROOFSTEP]
have hZ : IsClosed Z := hZ₁.union hZ₂
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
⊢ IsOpen (closure U)
[PROOFSTEP]
let f : Z → X := Prod.fst ∘ Subtype.val
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
⊢ IsOpen (closure U)
[PROOFSTEP]
have f_cont : Continuous f := continuous_fst.comp continuous_subtype_val
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
⊢ IsOpen (closure U)
[PROOFSTEP]
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⟩
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
⊢ Surjective f
[PROOFSTEP]
intro x
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
⊢ ∃ a, f a = x
[PROOFSTEP]
by_cases hx : x ∈ U
[GOAL]
case pos
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
hx : x ∈ U
⊢ ∃ a, f a = x
[PROOFSTEP]
exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩
[GOAL]
case neg
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
hx : ¬x ∈ U
⊢ ∃ a, f a = x
[PROOFSTEP]
exact ⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
⊢ IsOpen (closure U)
[PROOFSTEP]
haveI : CompactSpace Z := isCompact_iff_compactSpace.mp hZ.isCompact
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
⊢ IsOpen (closure U)
[PROOFSTEP]
obtain ⟨g, hg, g_sec⟩ := h continuous_id f_cont f_sur
[GOAL]
case intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
⊢ IsOpen (closure U)
[PROOFSTEP]
let φ := Subtype.val ∘ g
[GOAL]
case intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
⊢ IsOpen (closure U)
[PROOFSTEP]
have hφ : Continuous φ := continuous_subtype_val.comp hg
[GOAL]
case intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
⊢ IsOpen (closure U)
[PROOFSTEP]
have hφ₁ : ∀ x, (φ x).1 = x := congr_fun g_sec
[GOAL]
case intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
⊢ IsOpen (closure U)
[PROOFSTEP]
suffices closure U = φ ⁻¹' Z₂
  by
  rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl, ← preimage_subtype_coe_eq_compl Subset.rfl]
  · exact hZ₁.preimage hφ
  · rw [hZ₁₂.inter_eq, inter_empty]
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
this : closure U = φ ⁻¹' Z₂
⊢ IsOpen (closure U)
[PROOFSTEP]
rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl, ← preimage_subtype_coe_eq_compl Subset.rfl]
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
this : closure U = φ ⁻¹' Z₂
⊢ IsClosed (g ⁻¹' (Subtype.val ⁻¹' Z₁))
[PROOFSTEP]
exact hZ₁.preimage hφ
[GOAL]
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
this : closure U = φ ⁻¹' Z₂
⊢ (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅
[PROOFSTEP]
rw [hZ₁₂.inter_eq, inter_empty]
[GOAL]
case intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
⊢ closure U = φ ⁻¹' Z₂
[PROOFSTEP]
refine' (closure_minimal _ <| hZ₂.preimage hφ).antisymm fun x hx => _
[GOAL]
case intro.intro.refine'_1
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
⊢ U ⊆ φ ⁻¹' Z₂
[PROOFSTEP]
intro x hx
[GOAL]
case intro.intro.refine'_1
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
x : X
hx : x ∈ U
⊢ x ∈ φ ⁻¹' Z₂
[PROOFSTEP]
have : φ x ∈ Z₁ ∪ Z₂ :=
  (g x).2
    -- Porting note: Originally `simpa [hx, hφ₁] using this`
[GOAL]
case intro.intro.refine'_1
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
x : X
hx : x ∈ U
this : φ x ∈ Z₁ ∪ Z₂
⊢ x ∈ φ ⁻¹' Z₂
[PROOFSTEP]
cases' this with hφ hφ
[GOAL]
case intro.intro.refine'_1.inl
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ✝ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
x : X
hx : x ∈ U
hφ : φ x ∈ Z₁
⊢ x ∈ φ ⁻¹' Z₂
[PROOFSTEP]
exact ((hφ₁ x ▸ hφ.1) hx).elim
[GOAL]
case intro.intro.refine'_1.inr
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ✝ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
x : X
hx : x ∈ U
hφ : φ x ∈ Z₂
⊢ x ∈ φ ⁻¹' Z₂
[PROOFSTEP]
exact hφ
[GOAL]
case intro.intro.refine'_2
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
x : X
hx : x ∈ φ ⁻¹' Z₂
⊢ x ∈ closure U
[PROOFSTEP]
rw [← hφ₁ x]
[GOAL]
case intro.intro.refine'_2
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × 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 → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).fst = x
x : X
hx : x ∈ φ ⁻¹' Z₂
⊢ (φ x).fst ∈ closure U
[PROOFSTEP]
exact hx.1
[GOAL]
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
⊢ ∃ E, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π '' E₀ ≠ univ
[PROOFSTEP]
let S : Set <| Set D := {E : Set D | IsClosed E ∧ π '' E = univ}
[GOAL]
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
⊢ ∃ E, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π '' E₀ ≠ univ
[PROOFSTEP]
suffices ∀ (C : Set <| Set D) (_ : C ⊆ S) (_ : IsChain (· ⊆ ·) C), ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
  by
  rcases zorn_superset S this with ⟨E, ⟨E_closed, E_surj⟩, E_min⟩
  refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
  intro E₀ E₀_min E₀_closed
  contrapose! E₀_min
  exact eq_univ_of_coe_eq <| E_min E₀ ⟨E₀_closed.trans E_closed, image_coe_eq_restrict_image ▸ E₀_min⟩ coe_subset
[GOAL]
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ (C : Set (Set D)), C ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) C → ∃ s, s ∈ S ∧ ∀ (c : Set D), c ∈ C → s ⊆ c
⊢ ∃ E, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π '' E₀ ≠ univ
[PROOFSTEP]
rcases zorn_superset S this with ⟨E, ⟨E_closed, E_surj⟩, E_min⟩
[GOAL]
case intro.intro.intro
X : Type u
inst✝⁵ : TopologicalSpace X
A D E✝ : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E✝
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ (C : Set (Set D)), C ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) C → ∃ s, s ∈ S ∧ ∀ (c : Set D), c ∈ C → s ⊆ c
E : Set D
E_min : ∀ (a : Set D), a ∈ S → a ⊆ E → a = E
E_closed : IsClosed E
E_surj : π '' E = univ
⊢ ∃ E, CompactSpace ↑E ∧ π '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π '' E₀ ≠ univ
[PROOFSTEP]
refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
[GOAL]
case intro.intro.intro
X : Type u
inst✝⁵ : TopologicalSpace X
A D E✝ : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E✝
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ (C : Set (Set D)), C ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) C → ∃ s, s ∈ S ∧ ∀ (c : Set D), c ∈ C → s ⊆ c
E : Set D
E_min : ∀ (a : Set D), a ∈ S → a ⊆ E → a = E
E_closed : IsClosed E
E_surj : π '' E = univ
⊢ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π '' E₀ ≠ univ
[PROOFSTEP]
intro E₀ E₀_min E₀_closed
[GOAL]
case intro.intro.intro
X : Type u
inst✝⁵ : TopologicalSpace X
A D E✝ : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E✝
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ (C : Set (Set D)), C ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) C → ∃ s, s ∈ S ∧ ∀ (c : Set D), c ∈ C → s ⊆ c
E : Set D
E_min : ∀ (a : Set D), a ∈ S → a ⊆ E → a = E
E_closed : IsClosed E
E_surj : π '' E = univ
E₀ : Set ↑E
E₀_min : E₀ ≠ univ
E₀_closed : IsClosed E₀
⊢ restrict E π '' E₀ ≠ univ
[PROOFSTEP]
contrapose! E₀_min
[GOAL]
case intro.intro.intro
X : Type u
inst✝⁵ : TopologicalSpace X
A D E✝ : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E✝
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ (C : Set (Set D)), C ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) C → ∃ s, s ∈ S ∧ ∀ (c : Set D), c ∈ C → s ⊆ c
E : Set D
E_min : ∀ (a : Set D), a ∈ S → a ⊆ E → a = E
E_closed : IsClosed E
E_surj : π '' E = univ
E₀ : Set ↑E
E₀_closed : IsClosed E₀
E₀_min : restrict E π '' E₀ = univ
⊢ E₀ = univ
[PROOFSTEP]
exact eq_univ_of_coe_eq <| E_min E₀ ⟨E₀_closed.trans E_closed, image_coe_eq_restrict_image ▸ E₀_min⟩ coe_subset
[GOAL]
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
⊢ ∀ (C : Set (Set D)), C ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) C → ∃ s, s ∈ S ∧ ∀ (c : Set D), c ∈ C → s ⊆ c
[PROOFSTEP]
intro C C_sub C_chain
[GOAL]
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
⊢ ∃ s, s ∈ S ∧ ∀ (c : Set D), c ∈ C → s ⊆ c
[PROOFSTEP]
refine
  ⟨iInter (fun c : C => c), ⟨isClosed_iInter fun ⟨_, h⟩ => (C_sub h).left, ?_⟩, fun c hc _ h => mem_iInter.mp h ⟨c, hc⟩⟩
    -- prove intersection of chain is mapped onto $A$
[GOAL]
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
⊢ π '' ⋂ (c : ↑C), ↑c = univ
[PROOFSTEP]
by_cases hC : Nonempty C
[GOAL]
case pos
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
⊢ π '' ⋂ (c : ↑C), ↑c = univ
[PROOFSTEP]
refine
  eq_univ_of_forall fun a =>
    inter_nonempty_iff_exists_left.mp
      ?_
        -- apply Cantor's intersection theorem
[GOAL]
case pos
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
a : A
⊢ Set.Nonempty ((⋂ (c : ↑C), ↑c) ∩ fun a_1 => π a_1 = a)
[PROOFSTEP]
refine
  iInter_inter (ι := C) (π ⁻¹' { a }) _ ▸
    IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ ?_ (fun c => ?_) (fun c => IsClosed.isCompact ?_)
      (fun c => ?_)
[GOAL]
case pos.refine_1
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
a : A
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => ↑i ∩ π ⁻¹' {a}
[PROOFSTEP]
replace C_chain : IsChain (· ⊇ ·) C := C_chain.symm
[GOAL]
case pos.refine_1
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
hC : Nonempty ↑C
a : A
C_chain : IsChain (fun x x_1 => x ⊇ x_1) C
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => ↑i ∩ π ⁻¹' {a}
[PROOFSTEP]
have : ∀ s t : Set D, s ⊇ t → _ ⊇ _ := fun _ _ => inter_subset_inter_left <| π ⁻¹' { a }
[GOAL]
case pos.refine_1
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
hC : Nonempty ↑C
a : A
C_chain : IsChain (fun x x_1 => x ⊇ x_1) C
this : ∀ (s t : Set D), s ⊇ t → s ∩ π ⁻¹' {a} ⊇ t ∩ π ⁻¹' {a}
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => ↑i ∩ π ⁻¹' {a}
[PROOFSTEP]
exact (directedOn_iff_directed.mp C_chain.directedOn).mono_comp (· ⊇ ·) this
[GOAL]
case pos.refine_2
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ Set.Nonempty (↑c ∩ π ⁻¹' {a})
[PROOFSTEP]
rw [← image_inter_nonempty_iff, (C_sub c.mem).right, univ_inter]
[GOAL]
case pos.refine_2
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ Set.Nonempty {a}
[PROOFSTEP]
exact singleton_nonempty a
[GOAL]
case pos.refine_3
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ π ⁻¹' {a})
case pos.refine_4
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ π ⁻¹' {a})
[PROOFSTEP]
all_goals exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage π_cont
[GOAL]
case pos.refine_3
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ π ⁻¹' {a})
[PROOFSTEP]
exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage π_cont
[GOAL]
case pos.refine_4
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ π ⁻¹' {a})
[PROOFSTEP]
exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage π_cont
[GOAL]
case neg
X : Type u
inst✝⁵ : TopologicalSpace X
A D E : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace D
inst✝² : TopologicalSpace E
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x x_1 => x ⊆ x_1) C
hC : ¬Nonempty ↑C
⊢ π '' ⋂ (c : ↑C), ↑c = univ
[PROOFSTEP]
rw [@iInter_of_empty _ _ <| not_nonempty_iff.mp hC, image_univ_of_surjective π_surj]
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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ᶜ)ᶜ
[PROOFSTEP]
by_cases G_empty : G = ∅
[GOAL]
case pos
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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ᶜ)ᶜ
[PROOFSTEP]
simpa only [G_empty, image_empty] using empty_subset _
[GOAL]
case neg
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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ᶜ)ᶜ
[PROOFSTEP]
intro a ha
[GOAL]
case neg
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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ᶜ)ᶜ
[PROOFSTEP]
rw [mem_closure_iff]
  -- let $N$ be a neighbourhood of $a$
[GOAL]
case neg
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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
⊢ ∀ (o : Set A), IsOpen o → a ∈ o → Set.Nonempty (o ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
intro N N_open hN
[GOAL]
case neg
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
rcases(G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩
[GOAL]
case neg.intro.intro
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
have nonempty : (G ∩ ρ ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr hN⟩
[GOAL]
case neg.intro.intro
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
have is_open : IsOpen <| G ∩ ρ ⁻¹' N := hG.inter <| N_open.preimage ρ_cont
[GOAL]
case neg.intro.intro
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
have ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ := zorn_subset _ (compl_ne_univ.mpr nonempty) is_open.isClosed_compl
[GOAL]
case neg.intro.intro
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
rcases nonempty_compl.mpr ne_univ with
  ⟨x, hx⟩
    -- prove $x \in N \cap (A \setminus \rho(E \setminus G))$
[GOAL]
case neg.intro.intro.intro
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
have hx' : x ∈ (ρ '' Gᶜ)ᶜ := fun h => hx <| image_subset ρ (by simp) h
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
h : x ∈ ρ '' Gᶜ
⊢ Gᶜ ⊆ (G ∩ ρ ⁻¹' N)ᶜ
[PROOFSTEP]
simp
[GOAL]
case neg.intro.intro.intro
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : x ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
rcases ρ_surj x with ⟨y, rfl⟩
[GOAL]
case neg.intro.intro.intro.intro
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
have hy : y ∈ G ∩ ρ ⁻¹' N := by simpa using mt (mem_image_of_mem ρ) <| mem_compl hx
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ y ∈ G ∩ ρ ⁻¹' N
[PROOFSTEP]
simpa using mt (mem_image_of_mem ρ) <| mem_compl hx
[GOAL]
case neg.intro.intro.intro.intro
X : Type u
inst✝³ : TopologicalSpace X
A D E : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace D
inst✝ : 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 : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
hy : y ∈ G ∩ ρ ⁻¹' N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
[PROOFSTEP]
exact ⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩
[GOAL]
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
⊢ Injective ρ
[PROOFSTEP]
intro x₁ x₂ hρx
[GOAL]
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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₂
[PROOFSTEP]
by_contra hx
[GOAL]
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
rcases t2_separation hx with
  ⟨G₁, G₂, G₁_open, G₂_open, hx₁, hx₂, disj⟩
    -- prove $A \setminus \rho(E - G_1)$ and $A \setminus \rho(E - G_2)$ are disjoint
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
have G₁_comp : IsCompact G₁ᶜ := IsClosed.isCompact G₁_open.isClosed_compl
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
have G₂_comp : IsCompact G₂ᶜ := IsClosed.isCompact G₂_open.isClosed_compl
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
have G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ := (G₁_comp.image ρ_cont).isClosed.isOpen_compl
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
have G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ := (G₂_comp.image ρ_cont).isClosed.isOpen_compl
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
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]
    -- apply Lemma 2.2 to prove their closures are disjoint
[GOAL]
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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₂ᶜ)ᶜ
[PROOFSTEP]
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]
  -- apply Lemma 2.2 to prove their closures are disjoint
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
have disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ) :=
  disjoint_closure_of_disjoint_IsOpen disj' G₁_open' G₂_open'
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
have hx₁' :=
  image_subset_closure_compl_image_compl_of_isOpen ρ_cont ρ_surj zorn_subset G₁_open <| mem_image_of_mem ρ hx₁
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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
[PROOFSTEP]
have hx₂' :=
  image_subset_closure_compl_image_compl_of_isOpen ρ_cont ρ_surj zorn_subset G₂_open <| mem_image_of_mem ρ hx₂
[GOAL]
case intro.intro.intro.intro.intro.intro
X : Type u
inst✝⁷ : TopologicalSpace X
A D E : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace D
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : 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₁ᶜ)ᶜ
hx₂' : ρ x₂ ∈ closure (ρ '' G₂ᶜ)ᶜ
⊢ False
[PROOFSTEP]
exact disj''.ne_of_mem hx₁' hx₂' hρx
[GOAL]
X : Type u
inst✝⁶ : TopologicalSpace X
A D E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : ExtremallyDisconnected A
inst✝¹ : CompactSpace A
inst✝ : T2Space A
⊢ Projective A
[PROOFSTEP]
intro B C _ _ _ _ _ _ φ f φ_cont f_cont f_surj
[GOAL]
X : Type u
inst✝¹² : TopologicalSpace X
A D E : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
let D : Set <| A × B := {x | φ x.fst = f x.snd}
[GOAL]
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
have D_comp : CompactSpace D :=
  isCompact_iff_compactSpace.mp (isClosed_eq (φ_cont.comp continuous_fst) (f_cont.comp continuous_snd)).isCompact
[GOAL]
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
let π₁ : D → A := Prod.fst ∘ Subtype.val
[GOAL]
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
have π₁_cont : Continuous π₁ := continuous_fst.comp continuous_subtype_val
[GOAL]
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
have π₁_surj : π₁.Surjective := fun a => ⟨⟨⟨a, _⟩, (f_surj <| φ a).choose_spec.symm⟩, rfl⟩
[GOAL]
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
rcases exists_compact_surjective_zorn_subset π₁_cont π₁_surj with
  ⟨E, _, E_onto, E_min⟩
    -- apply Lemma 2.3 to get homeomorphism $\pi_1|_E : E \to A$
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
let ρ : E → A := E.restrict π₁
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
have ρ_cont : Continuous ρ := π₁_cont.continuousOn.restrict
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
have ρ_surj : ρ.Surjective := fun a => by rcases(E_onto ▸ mem_univ a : a ∈ π₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩;
  exact ⟨⟨d, hd⟩, rfl⟩
[GOAL]
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
a : A
⊢ ∃ a_1, ρ a_1 = a
[PROOFSTEP]
rcases(E_onto ▸ mem_univ a : a ∈ π₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩
[GOAL]
case intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
d : ↑D
hd : d ∈ E
⊢ ∃ a, ρ a = π₁ d
[PROOFSTEP]
exact ⟨⟨d, hd⟩, rfl⟩
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
let ρ' := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
let π₂ : D → B := Prod.snd ∘ Subtype.val
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
π₂ : ↑D → B := Prod.snd ∘ Subtype.val
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
have π₂_cont : Continuous π₂ := continuous_snd.comp continuous_subtype_val
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
π₂ : ↑D → B := Prod.snd ∘ Subtype.val
π₂_cont : Continuous π₂
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
[PROOFSTEP]
refine ⟨E.restrict π₂ ∘ ρ'.symm, ⟨π₂_cont.continuousOn.restrict.comp ρ'.symm.continuous, ?_⟩⟩
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
π₂ : ↑D → B := Prod.snd ∘ Subtype.val
π₂_cont : Continuous π₂
⊢ f ∘ restrict E π₂ ∘ ↑(Homeomorph.symm ρ') = φ
[PROOFSTEP]
suffices f ∘ E.restrict π₂ = φ ∘ ρ' by rw [← comp.assoc, this, comp.assoc, Homeomorph.self_comp_symm, comp.right_id]
[GOAL]
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
π₂ : ↑D → B := Prod.snd ∘ Subtype.val
π₂_cont : Continuous π₂
this : f ∘ restrict E π₂ = φ ∘ ↑ρ'
⊢ f ∘ restrict E π₂ ∘ ↑(Homeomorph.symm ρ') = φ
[PROOFSTEP]
rw [← comp.assoc, this, comp.assoc, Homeomorph.self_comp_symm, comp.right_id]
[GOAL]
case intro.intro.intro
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
π₂ : ↑D → B := Prod.snd ∘ Subtype.val
π₂_cont : Continuous π₂
⊢ f ∘ restrict E π₂ = φ ∘ ↑ρ'
[PROOFSTEP]
ext x
[GOAL]
case intro.intro.intro.h
X : Type u
inst✝¹² : TopologicalSpace X
A D✝ E✝ : Type u
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : TopologicalSpace D✝
inst✝⁹ : TopologicalSpace E✝
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.fst = f x.snd}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → restrict E π₁ '' E₀ ≠ univ
ρ : ↑E → A := restrict E π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
π₂ : ↑D → B := Prod.snd ∘ Subtype.val
π₂_cont : Continuous π₂
x : ↑E
⊢ (f ∘ restrict E π₂) x = (φ ∘ ↑ρ') x
[PROOFSTEP]
exact x.val.mem.symm
[GOAL]
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (π i)
⊢ ExtremallyDisconnected ((i : ι) × π i)
[PROOFSTEP]
constructor
[GOAL]
case open_closure
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (π i)
⊢ ∀ (U : Set ((i : ι) × π i)), IsOpen U → IsOpen (closure U)
[PROOFSTEP]
intro s hs
[GOAL]
case open_closure
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : IsOpen s
⊢ IsOpen (closure s)
[PROOFSTEP]
rw [isOpen_sigma_iff] at hs ⊢
[GOAL]
case open_closure
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
⊢ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' closure s)
[PROOFSTEP]
intro i
[GOAL]
case open_closure
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
⊢ IsOpen (Sigma.mk i ⁻¹' closure s)
[PROOFSTEP]
rcases h₀ i with ⟨h₀⟩
[GOAL]
case open_closure.mk
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
⊢ IsOpen (Sigma.mk i ⁻¹' closure s)
[PROOFSTEP]
have h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
[GOAL]
case h₁
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
⊢ IsOpen (closure (Sigma.mk i ⁻¹' s))
[PROOFSTEP]
apply h₀
[GOAL]
case h₁.a
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
⊢ IsOpen (Sigma.mk i ⁻¹' s)
[PROOFSTEP]
exact hs i
[GOAL]
case open_closure.mk
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
⊢ IsOpen (Sigma.mk i ⁻¹' closure s)
[PROOFSTEP]
suffices h₂ : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)
[GOAL]
case open_closure.mk
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
h₂ : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)
⊢ IsOpen (Sigma.mk i ⁻¹' closure s)
[PROOFSTEP]
rwa [h₂]
[GOAL]
case h₂
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
⊢ Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)
[PROOFSTEP]
apply IsOpenMap.preimage_closure_eq_closure_preimage
[GOAL]
case h₂.hf
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
⊢ IsOpenMap (Sigma.mk i)
case h₂.hfc
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
⊢ Continuous (Sigma.mk i)
[PROOFSTEP]
intro U _
[GOAL]
case h₂.hf
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
U : Set (π i)
a✝ : IsOpen U
⊢ IsOpen (Sigma.mk i '' U)
[PROOFSTEP]
rw [isOpen_sigma_iff]
[GOAL]
case h₂.hf
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
U : Set (π i)
a✝ : IsOpen U
⊢ ∀ (i_1 : ι), IsOpen (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' U))
[PROOFSTEP]
intro j
[GOAL]
case h₂.hf
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
U : Set (π i)
a✝ : IsOpen U
j : ι
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' U))
[PROOFSTEP]
by_cases ij : i = j
[GOAL]
case pos
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
U : Set (π i)
a✝ : IsOpen U
j : ι
ij : i = j
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' U))
[PROOFSTEP]
rw [← ij]
[GOAL]
case pos
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
U : Set (π i)
a✝ : IsOpen U
j : ι
ij : i = j
⊢ IsOpen (Sigma.mk i ⁻¹' (Sigma.mk i '' U))
[PROOFSTEP]
rw [sigma_mk_preimage_image_eq_self]
[GOAL]
case pos
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
U : Set (π i)
a✝ : IsOpen U
j : ι
ij : i = j
⊢ IsOpen U
[PROOFSTEP]
assumption
[GOAL]
case neg
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
U : Set (π i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' U))
[PROOFSTEP]
rw [sigma_mk_preimage_image' ij]
[GOAL]
case neg
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
U : Set (π i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen ∅
[PROOFSTEP]
apply isOpen_empty
[GOAL]
case h₂.hfc
X : Type u
inst✝¹ : TopologicalSpace X
ι : Type ?u.17123
π : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (π i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (π i)
s : Set ((i : ι) × π i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (π i)), IsOpen U → IsOpen (closure U)
h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s))
⊢ Continuous (Sigma.mk i)
[PROOFSTEP]
continuity
