[GOAL]
X : CompHaus
inst✝ : Projective X
⊢ ExtremallyDisconnected ↑X.toTop
[PROOFSTEP]
apply CompactT2.Projective.extremallyDisconnected
[GOAL]
case h
X : CompHaus
inst✝ : Projective X
⊢ CompactT2.Projective ↑X.toTop
[PROOFSTEP]
intro A B _ _ _ _ _ _ f g hf hg hsurj
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : CompactSpace (TopCat.of A) := by assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
⊢ CompactSpace ↑(TopCat.of A)
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this : CompactSpace ↑(TopCat.of A)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : T2Space (TopCat.of A) := by assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this : CompactSpace ↑(TopCat.of A)
⊢ T2Space ↑(TopCat.of A)
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝ : CompactSpace ↑(TopCat.of A)
this : T2Space ↑(TopCat.of A)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : CompactSpace (TopCat.of B) := by assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝ : CompactSpace ↑(TopCat.of A)
this : T2Space ↑(TopCat.of A)
⊢ CompactSpace ↑(TopCat.of B)
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝¹ : CompactSpace ↑(TopCat.of A)
this✝ : T2Space ↑(TopCat.of A)
this : CompactSpace ↑(TopCat.of B)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : T2Space (TopCat.of B) := by assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝¹ : CompactSpace ↑(TopCat.of A)
this✝ : T2Space ↑(TopCat.of A)
this : CompactSpace ↑(TopCat.of B)
⊢ T2Space ↑(TopCat.of B)
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let A' : CompHaus := ⟨TopCat.of A⟩
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let B' : CompHaus := ⟨TopCat.of B⟩
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let f' : X ⟶ B' := ⟨f, hf⟩
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
let g' : A' ⟶ B' := ⟨g, hg⟩
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
have : Epi g' := by
  rw [CompHaus.epi_iff_surjective]
  assumption
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
⊢ Epi g'
[PROOFSTEP]
rw [CompHaus.epi_iff_surjective]
[GOAL]
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝² : CompactSpace ↑(TopCat.of A)
this✝¹ : T2Space ↑(TopCat.of A)
this✝ : CompactSpace ↑(TopCat.of B)
this : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
⊢ Function.Surjective ↑g'
[PROOFSTEP]
assumption
[GOAL]
case h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
obtain ⟨h, hh⟩ := Projective.factors f' g'
[GOAL]
case h.intro
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
⊢ ∃ h, Continuous h ∧ g ∘ h = f
[PROOFSTEP]
refine ⟨h, h.2, ?_⟩
[GOAL]
case h.intro
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
⊢ g ∘ ↑h = f
[PROOFSTEP]
ext t
[GOAL]
case h.intro.h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
t : ↑X.toTop
⊢ (g ∘ ↑h) t = f t
[PROOFSTEP]
apply_fun (fun e => e t) at hh 
[GOAL]
case h.intro.h
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous f
hg : Continuous g
hsurj : Function.Surjective g
this✝³ : CompactSpace ↑(TopCat.of A)
this✝² : T2Space ↑(TopCat.of A)
this✝¹ : CompactSpace ↑(TopCat.of B)
this✝ : T2Space ↑(TopCat.of B)
A' : CompHaus := mk (TopCat.of A)
B' : CompHaus := mk (TopCat.of B)
f' : X ⟶ B' := ContinuousMap.mk f
g' : A' ⟶ B' := ContinuousMap.mk g
this : Epi g'
h : X ⟶ A'
t : ↑X.toTop
hh : ↑(h ≫ g') t = ↑f' t
⊢ (g ∘ ↑h) t = f t
[PROOFSTEP]
exact hh
