awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono f ↔
    Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
have mp : Mono f →
  Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
mp :
  Mono f →
    Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
⊢ Mono f ↔
    Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
have mpr : Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
  Mono f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (↑(X.toTop (P := P)) : Type u)
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₁ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₂ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
g₁ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₂, continuous_toFun := ⋯ }
⊢ g₁ ≫ f = g₂ ≫ f
have h₁ : ∀ (a : (↑(X.toTop (P := P)) : Type u)),
  Eq (α := (↑(Y.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (g₁ ≫ f) :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
        a :
      (↑(Y.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (g₂ ≫ f) :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
        a :
      (↑(Y.toTop (P := P)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (hypothesis)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (↑(X.toTop (P := P)) : Type u)
h :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₁ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        x₂ :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
g₁ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ x₂, continuous_toFun := ⋯ }
⊢ x₁ = x₂
have this : g₁ ≫ f = g₂ ≫ f
Tactic: have : g₁ ≫ f = g₂ ≫ f := by ext; exact h
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Function.Injective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
    Mono f
have mpr : Mono (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)) →
  Mono f
Tactic: rw [← CategoryTheory.ofHom_mono_iff_injective]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
⊢ Continuous (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    (⇑E.symm :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
have rw : ∀ (s : Set ((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)),
  IsClosed s →
    IsClosed (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
      ((⇑E.symm :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) ⁻¹'
        s)
Tactic: rw [continuous_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
S : Set ((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hS : IsClosed S
⊢ IsClosed (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((⇑E.symm :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) ⁻¹'
      S)
have rw : IsClosed (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
  ((⇑E :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) ''
    S)
Tactic: rw [← E.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (hypothesis)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
⊢ IsIso f
have hE : Continuous (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y) (Y :=
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
  (⇑E.symm :
    (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
Tactic: have hE : Continuous E.symm := by
    rw [continuous_iff_isClosed]
    intro S hS
    rw [← E.image_eq_preimage_symm]
    exact isClosedMap f S hS
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
hE :
  Continuous (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    (⇑E.symm :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
⊢ IsIso f
have refine_1 : Eq (α := X ⟶ X)
  (f ≫
      ofHom P
        {
          toFun :=
            (⇑E.symm :
              (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
          continuous_toFun := hE } :
    X ⟶ X)
  (𝟙 X : X ⟶ X)
Tactic: refine ⟨⟨ofHom _ ⟨E.symm, hE⟩, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
hE :
  Continuous (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    (⇑E.symm :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
refine_1 :
  Eq (α := X ⟶ X)
    (f ≫
        ofHom P
          {
            toFun :=
              (⇑E.symm :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
            continuous_toFun := hE } :
      X ⟶ X)
    (𝟙 X : X ⟶ X)
⊢ IsIso f
have refine_2 : Eq (α := Y ⟶ Y)
  (ofHom P
        {
          toFun :=
            (⇑E.symm :
              (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
          continuous_toFun := hE } ≫
      f :
    Y ⟶ Y)
  (𝟙 Y : Y ⟶ Y)
Tactic: refine ⟨⟨ofHom _ ⟨E.symm, hE⟩, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
hE :
  Continuous (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    (⇑E.symm :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
⊢ Eq (α := X ⟶ X)
    (f ≫
        ofHom P
          {
            toFun :=
              (⇑E.symm :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
            continuous_toFun := hE } :
      X ⟶ X)
    (𝟙 X : X ⟶ X)
have refine_1 : ∀ (x : (↑(X.toTop (P := P)) : Type u)),
  Eq (α := (↑(X.toTop (P := P)) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) (Y := X)
              (f ≫
                  ofHom P
                    {
                      toFun :=
                        (⇑E.symm :
                          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
                      continuous_toFun := hE } :
                X ⟶ X) :
            C((↑(X.toTop (P := P)) : Type u), (↑(X.toTop (P := P)) : Type u))) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑(X.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (𝟙 X) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑(X.toTop (P := P)) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij :
  Function.Bijective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
E : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X ≃
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y :=
  Equiv.ofBijective
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) f) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
    bij
hE :
  Continuous (X := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y) (Y :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    (⇑E.symm :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
⊢ Eq (α := Y ⟶ Y)
    (ofHom P
          {
            toFun :=
              (⇑E.symm :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
            continuous_toFun := hE } ≫
        f :
      Y ⟶ Y)
    (𝟙 Y : Y ⟶ Y)
have refine_2 : ∀ (x : (↑(Y.toTop (P := P)) : Type u)),
  Eq (α := (↑(Y.toTop (P := P)) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) (X := Y)
              (ofHom P
                    {
                      toFun :=
                        (⇑E.symm :
                          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X),
                      continuous_toFun := hE } ≫
                  f :
                Y ⟶ Y) :
            C((↑(Y.toTop (P := P)) : Type u), (↑(Y.toTop (P := P)) : Type u))) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑(Y.toTop (P := P)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
            (↑(X.toTop (P := P)) : Type u)) (𝟙 Y) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑(Y.toTop (P := P)) : Type u))
Tactic: ext x