X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
⊢ IsIso f
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
⊢ IsIso f
let E := Equiv.ofBijective _ bij
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
⊢ IsIso f
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
⊢ IsIso f
have hE : Continuous E.symm := by
  rw [continuous_iff_isClosed]
  intro S hS
  rw [← E.image_eq_preimage]
  exact isClosedMap f S hS
case refine'_1
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
⊢ f ≫ ContinuousMap.mk ↑E.symm = 𝟙 X

case refine'_2
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
⊢ ContinuousMap.mk ↑E.symm ≫ f = 𝟙 Y
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
⊢ IsIso f
refine' ⟨⟨⟨E.symm, hE⟩, _, _⟩⟩
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
⊢ ∀ (s : Set ((forget CompHaus).obj X)), IsClosed s → IsClosed (↑E.symm ⁻¹' s)
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
⊢ Continuous ↑E.symm
rw [continuous_iff_isClosed]
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
S : Set ((forget CompHaus).obj X)
hS : IsClosed S
⊢ IsClosed (↑E.symm ⁻¹' S)
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
⊢ ∀ (s : Set ((forget CompHaus).obj X)), IsClosed s → IsClosed (↑E.symm ⁻¹' s)
intro S hS
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
S : Set ((forget CompHaus).obj X)
hS : IsClosed S
⊢ IsClosed (↑E '' S)
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
S : Set ((forget CompHaus).obj X)
hS : IsClosed S
⊢ IsClosed (↑E.symm ⁻¹' S)
rw [← E.image_eq_preimage]
no goals
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
S : Set ((forget CompHaus).obj X)
hS : IsClosed S
⊢ IsClosed (↑E '' S)
exact isClosedMap f S hS
case refine'_1.w
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
x : (forget CompHaus).obj X
⊢ (forget CompHaus).map (f ≫ ContinuousMap.mk ↑E.symm) x = (forget CompHaus).map (𝟙 X) x
case refine'_1
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
⊢ f ≫ ContinuousMap.mk ↑E.symm = 𝟙 X
ext x
no goals
case refine'_1.w
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
x : (forget CompHaus).obj X
⊢ (forget CompHaus).map (f ≫ ContinuousMap.mk ↑E.symm) x = (forget CompHaus).map (𝟙 X) x
apply E.symm_apply_apply
case refine'_2.w
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
x : (forget CompHaus).obj Y
⊢ (forget CompHaus).map (ContinuousMap.mk ↑E.symm ≫ f) x = (forget CompHaus).map (𝟙 Y) x
case refine'_2
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
⊢ ContinuousMap.mk ↑E.symm ≫ f = 𝟙 Y
ext x
no goals
case refine'_2.w
X✝ : Type ?u.4524
inst✝² : TopologicalSpace X✝
inst✝¹ : CompactSpace X✝
inst✝ : T2Space X✝
X Y : CompHaus
f : X ⟶ Y
bij : Function.Bijective ((forget CompHaus).map f)
E : (forget CompHaus).obj X ≃ (forget CompHaus).obj Y := Equiv.ofBijective ((forget CompHaus).map f) bij
hE : Continuous ↑E.symm
x : (forget CompHaus).obj Y
⊢ (forget CompHaus).map (ContinuousMap.mk ↑E.symm ≫ f) x = (forget CompHaus).map (𝟙 Y) x
apply E.apply_symm_apply