-- Mathlib/Topology/Category/CompHausLike/Basic.lean
theorem isIso_of_bijective {X Y : CompHausLike.{u} P} (f : X ⟶ Y) (bij : Function.Bijective f) :
    IsIso f

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
S : Set ((fun X => ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E.symm ⁻¹' S)

Tactic:
rw [← E.image_eq_preimage]

Result:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
S : Set ((fun X => ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E '' S)

Proof state:
case refine_1.h.h
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
x : ↑X.toTop
⊢ (ConcreteCategory.hom (f ≫ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE })) x = (ConcreteCategory.hom (𝟙 X)) x

Tactic:
apply E.symm_apply_apply

Result:
no goals

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ ∀ (s : Set ((fun X => ↑X.toTop) X)), IsClosed s → IsClosed (⇑E.symm ⁻¹' s)

Tactic:
intro S hS

Result:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
S : Set ((fun X => ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E.symm ⁻¹' S)

Proof state:
case refine_1
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ f ≫ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } = 𝟙 X

Tactic:
ext x

Result:
case refine_1.h.h
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
x : ↑X.toTop
⊢ (ConcreteCategory.hom (f ≫ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE })) x = (ConcreteCategory.hom (𝟙 X)) x

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ Continuous ⇑E.symm

Tactic:
rw [continuous_iff_isClosed]

Result:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ ∀ (s : Set ((fun X => ↑X.toTop) X)), IsClosed s → IsClosed (⇑E.symm ⁻¹' s)

Proof state:
case refine_2.h.h
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
x : ↑Y.toTop
⊢ (ConcreteCategory.hom (ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f)) x = (ConcreteCategory.hom (𝟙 Y)) x

Tactic:
apply E.apply_symm_apply

Result:
no goals

Proof state:
case refine_2
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f = 𝟙 Y

Tactic:
ext x

Result:
case refine_2.h.h
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
x : ↑Y.toTop
⊢ (ConcreteCategory.hom (ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f)) x = (ConcreteCategory.hom (𝟙 Y)) x

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
⊢ IsIso f

Tactic:
let E := Equiv.ofBijective _ bij

Result:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ IsIso f

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ IsIso f

Tactic:
refine ⟨⟨ofHom _ ⟨E.symm, hE⟩, ?_, ?_⟩⟩

Result:
case refine_1
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ f ≫ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } = 𝟙 X

case refine_2
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f = 𝟙 Y

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
S : Set ((fun X => ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E '' S)

Tactic:
exact isClosedMap f S hS

Result:
no goals

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ IsIso f

Tactic:
have hE : Continuous E.symm := by
  rw [continuous_iff_isClosed]
  intro S hS
  rw [← E.image_eq_preimage]
  exact isClosedMap f S hS

Result:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X => ↑X.toTop) X ≃ (fun X => ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ IsIso f