Theorem: TotallyDisconnectedSpace.ofIso (Profinite/Epi.lean)

State before:
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
⊢ TotallyDisconnectedSpace ↑Y
Tactic:
have surj' : Function.Surjective f.hom
State after:
case surj'
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
⊢ Function.Surjective ↑f.hom

X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
⊢ TotallyDisconnectedSpace ↑Y

State before:
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
⊢ TotallyDisconnectedSpace ↑Y
Tactic:
have inj' : Function.Injective f.hom
State after:
case inj'
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
⊢ Function.Injective ↑f.hom

X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ TotallyDisconnectedSpace ↑Y

State before:
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ TotallyDisconnectedSpace ↑Y
Tactic:
constructor
State after:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ IsTotallyDisconnected Set.univ

State before:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ IsTotallyDisconnected Set.univ
Tactic:
unfold _root_.IsTotallyDisconnected
State after:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ ∀ (t : Set ↑Y), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t

State before:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
⊢ ∀ (t : Set ↑Y), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
Tactic:
intro t _ ht₂
State after:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
⊢ Set.Subsingleton t

State before:
case isTotallyDisconnected_univ
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
⊢ Set.Subsingleton t
Tactic:
apply Set.subsingleton_of_preimage surj'
State after:
case isTotallyDisconnected_univ.hs
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)

State before:
case isTotallyDisconnected_univ.hs
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)
Tactic:
replace k := k.isTotallyDisconnected_univ
State after:
case isTotallyDisconnected_univ.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : IsTotallyDisconnected Set.univ
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)

State before:
case isTotallyDisconnected_univ.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : IsTotallyDisconnected Set.univ
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)
Tactic:
unfold _root_.IsTotallyDisconnected at k
State after:
case isTotallyDisconnected_univ.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)

State before:
case isTotallyDisconnected_univ.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)
Tactic:
apply k
State after:
case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ ↑f.hom ⁻¹' t ⊆ Set.univ

case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected (↑f.hom ⁻¹' t)

State before:
case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ ↑f.hom ⁻¹' t ⊆ Set.univ

case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected (↑f.hom ⁻¹' t)
Tactic:
tauto
State after:
case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected (↑f.hom ⁻¹' t)

State before:
case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected (↑f.hom ⁻¹' t)
Tactic:
apply IsPreconnected.preimage_of_open_map
State after:
case isTotallyDisconnected_univ.hs.a.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected t

case isTotallyDisconnected_univ.hs.a.hinj
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Function.Injective ↑f.hom

case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom

State before:
case isTotallyDisconnected_univ.hs.a.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected t

case isTotallyDisconnected_univ.hs.a.hinj
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Function.Injective ↑f.hom

case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Tactic:
assumption
State after:
case isTotallyDisconnected_univ.hs.a.hinj
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Function.Injective ↑f.hom

case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom

State before:
case isTotallyDisconnected_univ.hs.a.hinj
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Function.Injective ↑f.hom

case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Tactic:
assumption
State after:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom

State before:
case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Tactic:
tauto
State after:
no goals

State before:
case surj'
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
⊢ Function.Surjective ↑f.hom
Tactic:
apply (TopCat.homeoOfIso f).surjective
State after:
no goals

State before:
case inj'
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
⊢ Function.Injective ↑f.hom
Tactic:
apply (TopCat.homeoOfIso f).injective
State after:
no goals

State before:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom
Tactic:
unfold IsOpenMap
State after:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ ∀ (U : Set ↑X), IsOpen U → IsOpen (↑f.hom '' U)

State before:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ ∀ (U : Set ↑X), IsOpen U → IsOpen (↑f.hom '' U)
Tactic:
intro U hU
State after:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
U : Set ↑X
hU : IsOpen U
⊢ IsOpen (↑f.hom '' U)

State before:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
U : Set ↑X
hU : IsOpen U
⊢ IsOpen (↑f.hom '' U)
Tactic:
apply TopCat.isOpen_iso _ hU
State after:
no goals