awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y S : TopCat
f : X ⟶ S
H :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
g : Y ⟶ S
⊢ IsOpenEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.snd f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
have h : Eq (α := (↑(pullback f g) : Type u) → (↑Y : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
        pullback f g) (pullback.snd f g)) :
    (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
  (Function.comp (β := (↑(pullback (𝟙 S) g) : Type u))
    (⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) : (a : (↑(pullback (𝟙 S) g) : Type u)) → (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (Y := pullback (𝟙 S) g) (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) sorry sorry)) :
      (a : (↑(pullback f g) : Type u)) → (↑(pullback (𝟙 S) g) : Type u)))
Tactic: convert!
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₂ := 𝟙 Y) f g (𝟙 _) g H
        (homeoOfIso (Iso.refl _)).isOpenEmbedding (𝟙 _) rfl (by simp))
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑S : Type u))
⊢ IsOpenEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.fst f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
have h : Eq (α := (↑(pullback f g) : Type u) → (↑X : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
        pullback f g) (pullback.fst f g)) :
    (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
  (Function.comp (β := (↑(pullback f (𝟙 S)) : Type u))
    (⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) : (a : (↑(pullback f (𝟙 S)) : Type u)) → (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (Y := pullback f (𝟙 S)) (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) sorry sorry)) :
      (a : (↑(pullback f g) : Type u)) → (↑(pullback f (𝟙 S)) : Type u)))
Tactic: convert!
    (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₁ := 𝟙 X) f g f (𝟙 _)
        (homeoOfIso (Iso.refl _)).isOpenEmbedding H (𝟙 _) rfl (by simp))
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
H₂ :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑S : Type u))
⊢ IsOpenEmbedding (X := (↑(limit (cospan f g)) : Type u)) (Y := (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
have h : (↑((cospan f g).obj WalkingCospan.one) : Type u) = (↑S : Type u) →
  Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (Function.comp (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
Tactic: convert! H₂.comp (snd_isOpenEmbedding_of_left H₁ g)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
H₂ :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑S : Type u))
e_2 : (↑((cospan f g).obj WalkingCospan.one) : Type u) = (↑S : Type u)
⊢ Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (Function.comp (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
have h : Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
        limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) :
    (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
        pullback f g) (pullback.snd f g ≫ g)) :
    (a : (↑(pullback f g) : Type u)) → (↑S : Type u))
Tactic: rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑S : Type u))
H :
  Subset (α := Set (↑S : Type u))
    (Set.range (ι := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑S : Type u)))
    (Set.range (ι := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u)))
x : (↑X : Type u)
⊢ Membership.mem (γ := Set (↑X : Type u))
    (Set.range (ι := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.fst f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u)))
    x
have rw : Membership.mem (γ := Set (↑X : Type u))
  {x : (↑X : Type u) |
    ∃ (y : (↑Y : Type u)),
      Eq (α := (↑S : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑X : Type u)) → (↑S : Type u))
            x :
          (↑S : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
              (a : (↑Y : Type u)) → (↑S : Type u))
            y :
          (↑S : Type u))}
  x
Tactic: rw [pullback_fst_range]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y S : TopCat
f : X ⟶ S
hf :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
g : Y ⟶ S
H :
  Subset (α := Set (↑S : Type u))
    (Set.range (ι := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u)))
    (Set.range (ι := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑S : Type u)))
x : (↑Y : Type u)
⊢ Membership.mem (γ := Set (↑Y : Type u))
    (Set.range (ι := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
    x
have rw : Membership.mem (γ := Set (↑Y : Type u))
  {y : (↑Y : Type u) |
    ∃ (x : (↑X : Type u)),
      Eq (α := (↑S : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
              (a : (↑X : Type u)) → (↑S : Type u))
            x :
          (↑S : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
              (a : (↑Y : Type u)) → (↑S : Type u))
            y :
          (↑S : Type u))}
  x
Tactic: rw [pullback_snd_range]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
⊢ Eq (α := Set (↑Y : Type u))
    (Set.image (α := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (pullback.fst f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
        U))
    (Set.preimage (β := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Z : Type u)) ''
        U))
have h : ∀ (x : (↑Y : Type u)),
  Membership.mem (γ := Set (↑Y : Type u))
      (Set.image (α := (↑(pullback f g) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f g) (pullback.fst f g)) :
            (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
          U))
      x ↔
    Membership.mem (γ := Set (↑Y : Type u))
      (Set.preimage (β := (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
            (a : (↑X : Type u)) → (↑Z : Type u)) ''
          U))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
⊢ Membership.mem (γ := Set (↑Y : Type u))
      (Set.image (α := (↑(pullback f g) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f g) (pullback.fst f g)) :
            (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
          U))
      x ↔
    Membership.mem (γ := Set (↑Y : Type u))
      (Set.preimage (β := (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
            (a : (↑X : Type u)) → (↑Z : Type u)) ''
          U))
      x
have h : Membership.mem (γ := Set (↑Y : Type u))
    (Set.image (α := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (pullback.fst f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
        U))
    x →
  Membership.mem (γ := Set (↑Y : Type u))
    (Set.preimage (β := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Z : Type u)) ''
        U))
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
y : (↑X : Type u)
hy : y ∈ U
eq :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
⊢ Membership.mem (γ := Set (↑Y : Type u))
    (Set.image (α := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (pullback.fst f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
        U))
    x
have h : Membership.mem (α := (↑(pullback f g) : Type u)) (γ := Set (↑(pullback f g) : Type u))
  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.fst f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
    U)
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (pullbackIsoProdSubtype f g).inv :
        (a :
            (↑(of
                  { p : (↑X : Type u) × (↑Y : Type u) //
                    (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                      (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) :
              Type u)) →
          (↑(pullback f g) : Type u))
      (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
        Eq (α := (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                (a : (↑X : Type u)) → (↑Z : Type u))
              p.1 :
            (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                (a : (↑Y : Type u)) → (↑Z : Type u))
              p.2 :
            (↑Z : Type u)))
        (y, x) eq) :
    (↑(pullback f g) : Type u))
Tactic: refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
y : (↑X : Type u)
hy : y ∈ U
eq :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.fst f g) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f g).inv :
            (a :
                { p : (↑X : Type u) × (↑Y : Type u) //
                  (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                    (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) →
              (↑(pullback f g) : Type u))
          (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
            Eq (α := (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑Z : Type u))
                  p.1 :
                (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑Z : Type u))
                  p.2 :
                (↑Z : Type u)))
            (y, x) eq) :
        (↑(pullback f g) : Type u)) =
    y
have h : (↑(Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
          Eq (α := (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                  (a : (↑X : Type u)) → (↑Z : Type u))
                p.1 :
              (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                  (a : (↑Y : Type u)) → (↑Z : Type u))
                p.2 :
              (↑Z : Type u)))
          (y, x) eq) :
      (↑X : Type u) × (↑Y : Type u)).1 =
  y
Tactic: rw [pullbackIsoProdSubtype_inv_fst_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
y : (↑X : Type u)
hy : y ∈ U
eq :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.snd f g) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f g).inv :
            (a :
                (↑(of
                      { p : (↑X : Type u) × (↑Y : Type u) //
                        (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                          (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) :
                  Type u)) →
              (↑(pullback f g) : Type u))
          (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
            Eq (α := (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑Z : Type u))
                  p.1 :
                (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑Z : Type u))
                  p.2 :
                (↑Z : Type u)))
            (y, x) eq) :
        (↑(pullback f g) : Type u)) =
    x
have h : (↑(Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
          Eq (α := (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                  (a : (↑X : Type u)) → (↑Z : Type u))
                p.1 :
              (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                  (a : (↑Y : Type u)) → (↑Z : Type u))
                p.2 :
              (↑Z : Type u)))
          (y, x) eq) :
      (↑X : Type u) × (↑Y : Type u)).2 =
  x
Tactic: rw [pullbackIsoProdSubtype_inv_snd_apply]