awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑X : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (range (ι := (↑Y : Type u))
        (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
            (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
have mp : Eq (α := Set (↑c.pt : Type u))
  (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
    (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
      (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
    (range (ι := (↑X : Type u))
      (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
            C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
        (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
  (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑Y : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
Tactic: conv_rhs => rw [Set.range_comp]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑X : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (range (ι := (↑Y : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
have mp : Eq (α := Set (↑c.pt : Type u))
  (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
    (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
      (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
    (range (ι := (↑X : Type u))
      (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
            C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
        (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
  (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
    (⇑(homeoOfIso (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y))).symm :
      (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
    (range (ι := (↑Y : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u)))ᶜ)
Tactic: erw [← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso
            (binaryCofanIsColimit X Y)).symm.bijective, Set.compl_range_inr, Set.image_comp]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
mp :
  Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑X : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(homeoOfIso (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y))).symm :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑Y : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u)))ᶜ)
⊢ Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑X : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (range (ι := (↑Y : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
have mp₁ : Eq (α := Set (↑c.pt : Type u))
  (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
    (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
      (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
    (range (ι := (↑X : Type u))
      (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
            C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
        (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
  (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
    (⇑(homeoOfIso (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y))).symm :
      (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
    (range Sum.inl))
Tactic: erw [← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso
            (binaryCofanIsColimit X Y)).symm.bijective, Set.compl_range_inr, Set.image_comp]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst f g
have rw : pullbackFst f g = (pullbackIsoProdSubtype f g).inv ≫ pullback.fst f g
Tactic: rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_fst]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
rw : pullbackFst f g = (pullbackIsoProdSubtype f g).inv ≫ pullback.fst f g
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst f g
have rw₁ : pullbackFst f g = pullbackFst f g
Tactic: rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_fst]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackSnd f g = pullback.snd f g
have rw : pullbackSnd f g = (pullbackIsoProdSubtype f g).inv ≫ pullback.snd f g
Tactic: rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_snd]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
rw : pullbackSnd f g = (pullbackIsoProdSubtype f g).inv ≫ pullback.snd f g
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackSnd f g = pullback.snd f g
have rw₁ : pullbackSnd f g = pullbackSnd f g
Tactic: rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_snd]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := Set (↑(X ⨯ 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) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
        (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
    {x : (↑(X ⨯ Y) : Type u) |
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                X ⨯ Y) (prod.fst ≫ f) :
              (a : (↑(X ⨯ 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 :=
                X ⨯ Y) (prod.snd ≫ g) :
              (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
            x :
          (↑Z : Type u))}
have h : ∀ (x : (↑(X ⨯ Y) : Type u)),
  Membership.mem (γ := Set (↑(X ⨯ 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) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
          (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
      x ↔
    Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
      {x : (↑(X ⨯ Y) : Type u) |
        Eq (α := (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  X ⨯ Y) (prod.fst ≫ f) :
                (a : (↑(X ⨯ 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 :=
                  X ⨯ Y) (prod.snd ≫ g) :
                (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
              x :
            (↑Z : Type 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
x : (↑(X ⨯ Y) : Type u)
⊢ Membership.mem (γ := Set (↑(X ⨯ 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) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
          (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
      x ↔
    Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
      {x : (↑(X ⨯ Y) : Type u) |
        Eq (α := (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  X ⨯ Y) (prod.fst ≫ f) :
                (a : (↑(X ⨯ 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 :=
                  X ⨯ Y) (prod.snd ≫ g) :
                (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
              x :
            (↑Z : Type u))}
      x
have h : Membership.mem (γ := Set (↑(X ⨯ 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) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
        (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
    x →
  Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
    {x : (↑(X ⨯ Y) : Type u) |
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                X ⨯ Y) (prod.fst ≫ f) :
              (a : (↑(X ⨯ 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 :=
                X ⨯ Y) (prod.snd ≫ g) :
              (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
            x :
          (↑Z : Type 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
y : (↑(pullback f g) : Type u)
⊢ Membership.mem (α := (↑(X ⨯ Y) : Type u)) (γ := Set (↑(X ⨯ Y) : Type u))
    {x : (↑(X ⨯ Y) : Type u) |
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                X ⨯ Y) (prod.fst ≫ f) :
              (a : (↑(X ⨯ 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 :=
                X ⨯ Y) (prod.snd ≫ g) :
              (a : (↑(X ⨯ 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) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u))
        y :
      (↑(X ⨯ Y) : Type u))
have h : Eq (α := (↑Z : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g)
          (CategoryStruct.comp (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) (prod.fst ≫ f)) :
        (a : (↑(pullback f g) : 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) (X :=
          pullback f g)
          (CategoryStruct.comp (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) (prod.snd ≫ g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Z : Type u))
      y :
    (↑Z : Type u))
Tactic: simp only [← ConcreteCategory.comp_apply, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
⊢ (fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
        (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
            ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
          { p : X × Y // f p.1 = g p.2 }))
      ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
          (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ : { x : X // x ∈ f ⁻¹' Set.range g }))
        x) =
    x
have a : (↑((fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
            (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
                ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) sorry) sorry :
              { p : X × Y // f p.1 = g p.2 }))
          ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
              (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 sorry :
                { x : X // x ∈ f ⁻¹' Set.range g }))
            x)) :
      X × Y).1 =
  (↑x : X × Y).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
a :
  (↑((fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
              (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
                  ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
                { p : X × Y // f p.1 = g p.2 }))
            ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
                (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ :
                  { x : X // x ∈ f ⁻¹' Set.range g }))
              x)) :
        X × Y).1 =
    (↑x : X × Y).1
⊢ (fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
        (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
            ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
          { p : X × Y // f p.1 = g p.2 }))
      ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
          (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ : { x : X // x ∈ f ⁻¹' Set.range g }))
        x) =
    x
have a₁ : (↑((fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
            (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
                ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) sorry) sorry :
              { p : X × Y // f p.1 = g p.2 }))
          ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
              (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 sorry :
                { x : X // x ∈ f ⁻¹' Set.range g }))
            x)) :
      X × Y).2 =
  (↑x : X × Y).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
⊢ (↑((fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
              (Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2)
                  ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯) ⋯ :
                { p : X × Y // f p.1 = g p.2 }))
            ((fun (x : { p : X × Y // f p.1 = g p.2 }) ↦
                (Subtype.mk (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g) (↑x : X × Y).1 ⋯ :
                  { x : X // x ∈ f ⁻¹' Set.range g }))
              x)) :
        X × Y).2 =
    (↑x : X × Y).2
have a : Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) sorry = (↑x : X × Y).2
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
⊢ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯ = (↑x : X × Y).2
have a : g (Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) sorry) = g (↑x : X × Y).2
Tactic: apply hg.injective
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
x : { p : X × Y // f p.1 = g p.2 }
⊢ g (Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) ⋯) = g (↑x : X × Y).2
have h : g (Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X × Y).1) sorry) = f (↑x : X × Y).1
Tactic: convert! x.prop
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
    Subtype.mk (p := fun (p : X × Y) ↦ f p.1 = g p.2) ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
      ⋯
have h : Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
  ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) sorry)
Tactic: apply Continuous.subtype_mk
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦
    ((↑x : X), Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
have h : Continuous[instTopologicalSpaceSubtype, inst_3]
  (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) sorry)
Tactic: refine continuous_subtype_val.prodMk <| hg.isInducing.continuous_iff.mpr ?_
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, inst_3]
    (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
have h : Eq (α := { x : X // x ∈ f ⁻¹' Set.range g } → Z)
  (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) sorry)
  (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g))
Tactic: convert! hf.comp continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X_1 Y_1 Z_1 : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
f : X → Z
hf : Continuous[inst_1, inst_3] f
g : Y → Z
hg : IsEmbedding g
⊢ Eq (α := { x : X // x ∈ f ⁻¹' Set.range g } → Z)
    (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) ⋯)
    (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g))
have h : ∀ (x : { x : X // x ∈ f ⁻¹' Set.range g }),
  (g ∘ fun (x : (↑(f ⁻¹' Set.range g) : Type u_1)) ↦ Exists.choose (p := fun (a : Y) ↦ g a = f (↑x : X)) sorry) x =
    (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' Set.range g)) x
Tactic: ext x