Theorem: CategoryTheory.clopen_extremallyDisconnected (ExtrDisc/Pullback.lean)

State before:
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
⊢ ExtremallyDisconnected ↑U
Tactic:
constructor
State after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
⊢ ∀ (U_1 : Set ↑U), IsOpen U_1 → IsOpen (closure U_1)

State before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
⊢ ∀ (U_1 : Set ↑U), IsOpen U_1 → IsOpen (closure U_1)
Tactic:
intro V hV
State after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
⊢ IsOpen (closure V)

State before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
⊢ IsOpen (closure V)
Tactic:
have hV' : IsOpen (Subtype.val '' V) := hU.1.openEmbedding_subtype_val.isOpenMap V hV
State after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
⊢ IsOpen (closure V)

State before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
⊢ IsOpen (closure V)
Tactic:
have := ExtremallyDisconnected.open_closure _ hV'
State after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (closure (Subtype.val '' V))
⊢ IsOpen (closure V)

State before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (closure (Subtype.val '' V))
⊢ IsOpen (closure V)
Tactic:
rw [hU.2.closedEmbedding_subtype_val.closure_image_eq V] at this
State after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
⊢ IsOpen (closure V)

State before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
⊢ IsOpen (closure V)
Tactic:
suffices hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' (closure V))
State after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
⊢ IsOpen (closure V)

case hhU
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
⊢ closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)

State before:
case hhU
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
⊢ closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
Tactic:
exact ((closure V).preimage_image_eq Subtype.coe_injective).symm
State after:
no goals

State before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
⊢ IsOpen (closure V)
Tactic:
rw [hhU]
State after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
⊢ IsOpen (Subtype.val ⁻¹' (Subtype.val '' closure V))

State before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
⊢ IsOpen (Subtype.val ⁻¹' (Subtype.val '' closure V))
Tactic:
exact isOpen_induced this
State after:
no goals