Theorem: CompHaus.Gleason (ExtrDisc/Basic.lean)

State before:
X : CompHaus
⊢ Projective X ↔ ExtremallyDisconnected ↑X.toTop
Tactic:
constructor
State after:
case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop

case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X

State before:
case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop
Tactic:
intro h
State after:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toTop

State before:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toTop
Tactic:
show ExtremallyDisconnected X.toExtrDisc
State after:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected (CoeSort.coe (toExtrDisc X))

State before:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected (CoeSort.coe (toExtrDisc X))
Tactic:
infer_instance
State after:
no goals

State before:
case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X
Tactic:
intro h
State after:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
⊢ Projective X

State before:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
⊢ Projective X
Tactic:
let X' : ExtrDisc := ⟨X⟩
State after:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : ExtrDisc := ExtrDisc.mk X
⊢ Projective X

State before:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : ExtrDisc := ExtrDisc.mk X
⊢ Projective X
Tactic:
show Projective X'.compHaus
State after:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : ExtrDisc := ExtrDisc.mk X
⊢ Projective X'.compHaus

State before:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : ExtrDisc := ExtrDisc.mk X
⊢ Projective X'.compHaus
Tactic:
apply ExtrDisc.instProjectiveCompHausCategoryCompHaus
State after:
no goals