awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Basic (hypothesis)
Goal:
P : TopCat.{u} → Prop
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf :
  IsIso (X :=
    Functor.obj
      (forget (CompHausLike P) (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)))
      A)
    (CategoryTheory.Functor.map
      (forget (CompHausLike P) (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)
⊢ IsIso f
have hf₁ : Function.Bijective (α :=
  (fun (X : Type u) ↦ X)
    (Functor.obj
      (forget (CompHausLike P) (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)))
      A))
  (β :=
  (fun (X : Type u) ↦ X)
    (Functor.obj
      (forget (CompHausLike P) (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)))
      B))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryTheory.Functor.map
          (forget (CompHausLike P) (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 : Type u) ↦ X) ((forget (CompHausLike P)).obj A)) →
      (fun (X : Type u) ↦ X) ((forget (CompHausLike P)).obj B))
Tactic: rw [isIso_iff_bijective] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Cartesian (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
inst : HasProp P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))
⊢ IsLimit (X.productCone (P := P) Y)
have refine : ∀ (x : BinaryFan X Y) (x_1 : x.pt ⟶ of P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
  (h₁ : x_1 ≫ ofHom P { toFun := Prod.fst, continuous_toFun := sorry } = x.fst)
  (h₂ : x_1 ≫ ofHom P { toFun := Prod.snd, continuous_toFun := sorry } = x.snd),
  x_1 =
    (fun (s : BinaryFan X Y) ↦
        (ofHom P
            {
              toFun := fun (x : (↑s.1.1 : 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)) s.fst :
                      (a :
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                            (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left })) →
                        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) ((pair X Y).obj { as := WalkingPair.left }))
                    x,
                  (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)) s.snd :
                      (a :
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                            (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })) →
                        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) ((pair X Y).obj { as := WalkingPair.right }))
                    x),
              continuous_toFun := sorry } :
          of P (↑s.1.1 : Type u) ⟶ of P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))))
      x
Tactic: refine BinaryFan.isLimitMk (fun s ↦ ofHom _ { toFun x := (s.fst x, s.snd x) })
    (by rfl_cat) (by rfl_cat) fun _ _ h₁ h₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Cartesian (goal)
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
inst : HasProp P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u))
⊢ IsColimit (X.coproductCocone (P := P) Y)
have refine : ∀ (x : BinaryCofan X Y) (x_1 : of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)) ⟶ x.pt)
  (h₁ : ofHom P { toFun := Sum.inl, continuous_toFun := sorry } ≫ x_1 = x.inl)
  (h₂ : ofHom P { toFun := Sum.inr, continuous_toFun := sorry } ≫ x_1 = x.inr),
  x_1 =
    (fun (s : BinaryCofan X Y) ↦
        (ofHom P
            {
              toFun :=
                Sum.elim
                  (⇑(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)) s.inl) :
                    (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) ((pair X Y).obj { as := WalkingPair.left })) →
                      (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                        (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }))
                  (⇑(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)) s.inr) :
                    (a :
                        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) ((pair X Y).obj { as := WalkingPair.right })) →
                      (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                        (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })),
              continuous_toFun := sorry } :
          of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)) ⟶ of P (↑s.1.1 : Type u)))
      x
Tactic: refine BinaryCofan.isColimitMk (fun s ↦ ofHom _ { toFun := Sum.elim s.inl s.inr })
    (by rfl_cat) (by rfl_cat) fun _ _ h₁ h₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.EffectiveEpi (goal)
Goal:
P : TopCat.{u} → Prop
B X : CompHausLike P
π : X ⟶ B
hπ :
  Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    (⇑(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)) π) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
W : CompHausLike P
e : X ⟶ W
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
hab :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    ((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)) π :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
        a :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    ((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)) π :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
        b :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
⊢ Eq (α := of P (↑X.1 : Type u) ⟶ B) (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π)
    (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π)
have h₁ : ∀ (a_1 : (↑((of P (↑X.1 : Type u)).toTop (P := P)) : Type u)),
  Eq (α := (↑(B.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 := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := sorry } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.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 := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := sorry } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.toTop (P := P)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.EffectiveEpi (goal)
Goal:
P : TopCat.{u} → Prop
B X : CompHausLike P
π : X ⟶ B
hπ :
  Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    (⇑(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)) π) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
W : CompHausLike P
e : X ⟶ W
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a b : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
hab :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    ((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)) π :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
        a :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    ((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)) π :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
        b :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
⊢ Eq (α := of P (↑X.1 : Type u) ⟶ B) (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π)
    (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π)
have h₁ : ∀ (a_1 : (↑((of P (↑X.1 : Type u)).toTop (P := P)) : Type u)),
  Eq (α := (↑(B.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 := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := sorry } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.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 := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := sorry } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.toTop (P := P)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.EffectiveEpi (goal)
Goal:
P : TopCat.{u} → Prop
B X : CompHausLike P
π : X ⟶ B
hπ :
  Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    (⇑(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)) π) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
W : CompHausLike P
e : X ⟶ W
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
⊢ g = ofHom P (⋯.lift (TopCat.Hom.hom e.hom) ⋯)
have suffices : g =
  ofHom P
    ((sorry.liftEquiv :
        (a :
            { g : C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X, (↑W.toTop : Type u)) //
              Function.FactorsThrough
                (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
                (⇑(ConcreteCategory.hom π) :
                  (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                    (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) }) →
          C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B, (↑W.toTop : Type u)))
      (Subtype.mk (p :=
        fun (g : C((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X, (↑(W.toTop (P := P)) : Type u))) ↦
        Function.FactorsThrough (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B) (γ := (↑(W.toTop (P := P)) : Type u))
          (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : 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)) π) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B))
        (TopCat.Hom.hom e.hom) sorry))
Tactic: suffices g = ofHom _
        ((IsQuotientMap.of_surjective_continuous hπ π.hom.hom.continuous).liftEquiv ⟨e.hom.hom,
      fun a b hab ↦ CategoryTheory.congr_fun
        (h
          (ofHom _ ⟨fun _ ↦ a, continuous_const⟩)
          (ofHom _ ⟨fun _ ↦ b, continuous_const⟩)
          (by ext; exact hab))
        a⟩) by assumption
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.EffectiveEpi (goal)
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (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)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
⊢ ∃ (W : CompHausLike P) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ π = h ≫ f
have refine : Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (pullback (P := P) f π)) (β :=
  (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
  (⇑(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 := pullback (P := P) f π) (pullback.fst (P := P) f π)) :
    (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (pullback f π)) →
      (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
Tactic: refine ⟨pullback f π, pullback.fst f π, ⟨⟨effectiveEpiStruct _ ?_⟩⟩, pullback.snd f π,
      (pullback.condition _ _).symm⟩
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.EffectiveEpi (goal)
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (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)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
y : (↑(X.toTop (P := P)) : Type u)
⊢ ∃ (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (pullback (P := P) f π)),
    (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 := pullback (P := P) f π) (pullback.fst (P := P) f π) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (pullback f π)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        a =
      y
have obtain : ∀ (z : (↑(Z.toTop (P := P)) : Type u))
  (hz :
    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)) π :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
          z :
        (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)
          y :
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)),
  ∃ (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) (pullback (P := P) f π)),
    (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 := pullback (P := P) f π) (pullback.fst (P := P) f π) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (pullback f π)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        a =
      y
Tactic: obtain ⟨z, hz⟩ := hs π hπ (f y)
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.EffectiveEpi (hypothesis)
Goal:
P : TopCat.{u} → Prop
inst : HasExplicitPullbacks P
inst_1 : HasExplicitFiniteCoproducts P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (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)
⊢ Precoherent.{u, u + 1} (CompHausLike P)
have this : Preregular.{u, u + 1} (CompHausLike P)
Tactic: have : Preregular (CompHausLike P) := preregular hs
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
B : CompHausLike P
e : (a : α) → X a ⟶ B
⊢ Continuous (Y := (↑B.1 : Type (max u w))) fun (x : (a : α) × (↑((X a).toTop (P := P)) : Type (max u w))) ↦
    match (motive := (a : α) × (↑((X a).toTop (P := P)) : Type (max u w)) → (↑B.1 : Type (max u w))) x with
    | ⟨a, x⟩ =>
      (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (e a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
        x
have hf : ∀ (i : α),
  Continuous (Y := (↑B.1 : Type (max u w))) fun (a : (↑((X i).toTop (P := P)) : Type (max u w))) ↦
    match (motive := (a : α) × (↑((X a).toTop (P := P)) : Type (max u w)) → (↑B.1 : Type (max u w)))
      Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) i a with
    | ⟨a, x⟩ =>
      (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (e a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
        x
Tactic: apply continuous_sigma
-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
B : CompHausLike P
f g : finiteCoproduct.{w, u} (P := P) X ⟶ B
h : ∀ (a : α), ι (P := P) X a ≫ f = ι (P := P) X a ≫ g
⊢ f = g
have h₁ : ∀ (a : α) (x : (↑((X a).toTop (P := P)) : Type (max u w))),
  Eq (α := (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) f :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) g :
          (a : (↑(finiteCoproduct X).toTop : Type (max u w))) → (↑B.toTop : Type (max u w)))
        (Sigma.mk (β := fun (a : α) ↦ (↑((X a).toTop (P := P)) : Type (max u w))) a x) :
      (↑(B.toTop (P := P)) : Type (max u w)))
Tactic: ext ⟨a, x⟩