Theorem: TopCat.isOpen_iso (Profinite/Epi.lean)

State before:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
h : IsOpen U
⊢ IsOpen (↑f.hom '' U)
Tactic:
let ff := TopCat.homeoOfIso f
State after:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
h : IsOpen U
ff : ↑X ≃ₜ ↑Y := homeoOfIso f
⊢ IsOpen (↑f.hom '' U)

State before:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
h : IsOpen U
ff : ↑X ≃ₜ ↑Y := homeoOfIso f
⊢ IsOpen (↑f.hom '' U)
Tactic:
rw [← Homeomorph.isOpen_image ff] at h
State after:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
ff : ↑X ≃ₜ ↑Y := homeoOfIso f
h : IsOpen (↑ff '' U)
⊢ IsOpen (↑f.hom '' U)

State before:
X Y : TopCat
U : Set ↑X
f : X ≅ Y
ff : ↑X ≃ₜ ↑Y := homeoOfIso f
h : IsOpen (↑ff '' U)
⊢ IsOpen (↑f.hom '' U)
Tactic:
assumption
State after:
no goals