Theorem: Profinite.EffectiveEpiFamily.CompHaus.TotallyDisconnectedSpace_ofIsIso (Profinite/Epi.lean)

State before:
X✝¹ Y✝ B✝ : Profinite
f✝ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f : X ≅ Y
⊢ TotallyDisconnectedSpace ↑Y.toTop
Tactic:
have f : X.toTop ≅ Y.toTop
State after:
case f
X✝¹ Y✝ B✝ : Profinite
f✝ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f : X ≅ Y
⊢ X.toTop ≅ Y.toTop

X✝¹ Y✝ B✝ : Profinite
f✝¹ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f✝ : X ≅ Y
f : X.toTop ≅ Y.toTop
⊢ TotallyDisconnectedSpace ↑Y.toTop

State before:
X✝¹ Y✝ B✝ : Profinite
f✝¹ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f✝ : X ≅ Y
f : X.toTop ≅ Y.toTop
⊢ TotallyDisconnectedSpace ↑Y.toTop
Tactic:
apply TotallyDisconnectedSpace.ofIso f
State after:
no goals

State before:
case f
X✝¹ Y✝ B✝ : Profinite
f✝ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f : X ≅ Y
⊢ X.toTop ≅ Y.toTop
Tactic:
exact compHausToTop.mapIso f
State after:
no goals