awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (↑Y : Type u)
⊢ Eq (α := Set (↑X : 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.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) (X :=
              pullback f g) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : 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) f) :
        (a : (↑X : Type u)) → (↑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)) ''
        U))
have h : ∀ (x : (↑X : Type u)),
  Membership.mem (γ := Set (↑X : 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.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) (X :=
                pullback f g) (pullback.snd f g)) :
            (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)) ⁻¹'
          U))
      x ↔
    Membership.mem (γ := Set (↑X : Type u))
      (Set.preimage (β := (↑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))
        ((⇑(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)) ''
          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 (↑Y : Type u)
x : (↑X : Type u)
⊢ Membership.mem (γ := Set (↑X : 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.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) (X :=
                pullback f g) (pullback.snd f g)) :
            (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)) ⁻¹'
          U))
      x ↔
    Membership.mem (γ := Set (↑X : Type u))
      (Set.preimage (β := (↑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))
        ((⇑(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)) ''
          U))
      x
have h : Membership.mem (γ := Set (↑X : 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.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) (X :=
              pullback f g) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)) ⁻¹'
        U))
    x →
  Membership.mem (γ := Set (↑X : Type u))
    (Set.preimage (β := (↑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))
      ((⇑(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)) ''
        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 (↑Y : Type u)
x : (↑X : Type u)
y : (↑Y : 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) g :
          (a : (↑Y : 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) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
⊢ Membership.mem (γ := Set (↑X : 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.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) (X :=
              pullback f g) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : 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.snd f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑Y : 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)))
        (x, y) sorry) :
    (↑(pullback f g) : Type u))
Tactic: refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq.symm⟩, ?_, ?_⟩
-- 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 (↑Y : Type u)
x : (↑X : Type u)
y : (↑Y : 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) g :
          (a : (↑Y : 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) f :
          (a : (↑X : 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 :
                { 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)))
            (x, y) ⋯) :
        (↑(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)))
          (x, y) sorry) :
      (↑X : Type u) × (↑Y : Type u)).2 =
  y
Tactic: rw [pullbackIsoProdSubtype_inv_snd_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 (↑Y : Type u)
x : (↑X : Type u)
y : (↑Y : 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) g :
          (a : (↑Y : 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) f :
          (a : (↑X : 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 :
                (↑(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)))
            (x, y) ⋯) :
        (↑(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)))
          (x, y) sorry) :
      (↑X : Type u) × (↑Y : Type u)).1 =
  x
Tactic: rw [pullbackIsoProdSubtype_inv_fst_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
⊢ IsOpen U ↔
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U)
have rw : (∀ (j : WalkingParallelPair),
    IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑((parallelPair f g).obj j) : Type u)) →
            (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
        U)) ↔
  IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)
Tactic: rw [isOpen_iff_of_isColimit _ hc]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
⊢ (∀ (j : WalkingParallelPair),
      IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑((parallelPair f g).obj j) : Type u)) →
              (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
          U)) ↔
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U)
have mp : (∀ (j : WalkingParallelPair),
    IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑((parallelPair f g).obj j) : Type u)) →
            (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
        U)) →
  IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
mp :
  (∀ (j : WalkingParallelPair),
      IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑((parallelPair f g).obj j) : Type u)) →
              (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
          U)) →
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U)
⊢ (∀ (j : WalkingParallelPair),
      IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑((parallelPair f g).obj j) : Type u)) →
              (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
          U)) ↔
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U)
have mpr : IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U) →
  ∀ (j : WalkingParallelPair),
    IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑((parallelPair f g).obj j) : Type u)) →
            (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
        U)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
h :
  IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)
⊢ IsOpen (X := (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app WalkingParallelPair.zero)) :
        (a : (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u)) →
          (↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.zero) : Type u)) ⁻¹'
      U)
have mpr : IsOpen (X := (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u))
  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          ((parallelPair f g).map WalkingParallelPairHom.left ≫ c.ι.app WalkingParallelPair.one)) :
      (a : (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u)) →
        (↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.zero) : Type u)) ⁻¹'
    U)
Tactic: rw [← c.w .left]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ IsQuotientMap (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
      (a : (↑Y : Type u)) → (↑c.pt : Type u))
have rw : IsCoinducing (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
      (a : (↑Y : Type u)) → (↑c.pt : Type u)) ∧
  Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
      (a : (↑Y : Type u)) → (↑c.pt : Type u))
Tactic: rw [isQuotientMap_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ IsCoinducing (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ∧
    Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u))
have refine_1 : ∀ (s : Set (↑c.pt : Type u)),
  IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        s) ↔
    IsOpen s
Tactic: refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
refine_1 :
  ∀ (s : Set (↑c.pt : Type u)),
    IsOpen (X := (↑Y : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
            (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
          s) ↔
      IsOpen s
⊢ IsCoinducing (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ∧
    Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u))
have refine_2 : Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
    (a : (↑Y : Type u)) → (↑c.pt : Type u))
Tactic: refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.OpenNhds (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
x_1 : (↑X : Type u)
U V W : OpenNhds x_1
x_2 : (↑X : Type u)
x : OpenNhds x_2
⊢ x ≤ Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x_2 ∈ U) ⊤ trivial
have mk : ∀ (val : Opens (↑X : Type u)) (property : x_2 ∈ val),
  LE.le (α := OpenNhds x_2) (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x_2 ∈ U) val property)
    (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x_2 ∈ U) ⊤ trivial)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Sphere (goal)
Goal:
n : ℕ
t : Set (ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
h : IsOpen t
s : Set (↑(Metric.closedBall 0 1) : Type)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs :
  Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
      r =
    s
hst : ULift.down ⁻¹' s = t
⊢ IsOpen (X := ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type))
    ((fun (x : ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type)) ↦
        match (motive :=
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type)) x with
        | { down := ⟨p, hp⟩ } =>
          {
            down :=
              Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p ⋯ }) ⁻¹'
      t)
have rw : ∃ (t : Set (↑(Metric.sphere 0 1) : Type)),
  IsOpen t ∧
    ULift.down ⁻¹' t =
      Set.preimage (β := ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
        (fun (x : ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type)) ↦
          match (motive :=
            ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type)) x with
          | { down := ⟨p, hp⟩ } =>
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p sorry })
        (ULift.down ⁻¹'
          Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
            r)
Tactic: rw [isOpen_induced_iff, ← hst, ← hrs]