awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.EffectivelyEnough
inst_5 : Preregular.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
W : D
f' : W ⟶ F.obj X
w_1 : EffectiveEpi f'
i : W ⟶ F.obj Z
w : i ≫ F.map g = f' ≫ F.map f
⊢ EffectiveEpi (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
    (F.map (F.preimage (F.effectiveEpiOver W ≫ f')) :
      F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj X)
have refine_1 : EffectiveEpi (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
  (F.effectiveEpiOver W ≫ f' :
    F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)) ⟶ F.obj X)
Tactic: simp only [Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.EffectivelyEnough
inst_5 : Preregular.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
W : D
f' : W ⟶ F.obj X
w_1 : EffectiveEpi f'
i : W ⟶ F.obj Z
w : i ≫ F.map g = f' ≫ F.map f
⊢ Eq (α := EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)
    (F.preimage (F.effectiveEpiOver W ≫ i) ≫ g :
      EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)
    (F.preimage (F.effectiveEpiOver W ≫ f') ≫ f :
      EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)
have refine_2 : Eq (α := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)) ⟶ F.obj Y)
  (F.map (F.preimage (F.effectiveEpiOver W ≫ i) ≫ g) :
    F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)) ⟶ F.obj Y)
  (F.map (F.preimage (F.effectiveEpiOver W ≫ f') ≫ f) :
    F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)) ⟶ F.obj Y)
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))
have h : P.map (F.map π).op = (F.op ⋙ P).map π.op
Tactic: have h : P.map (F.map π).op = (F.op ⋙ P).map π.op := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))
have refine_1 : P.map (F.map π).op ≫ (F.op ⋙ P).map c.fst.op = P.map (F.map π).op ≫ (F.op ⋙ P).map c.snd.op
Tactic: refine ⟨(IsLimit.equivIsoLimit (ForkOfι.ext ?_ _ h)) ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
refine_1 : P.map (F.map π).op ≫ (F.op ⋙ P).map c.fst.op = P.map (F.map π).op ≫ (F.op ⋙ P).map c.snd.op
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))
have refine_2 : IsLimit (Fork.ofι (P.map (F.map π).op) sorry)
Tactic: refine ⟨(IsLimit.equivIsoLimit (ForkOfι.ext ?_ _ h)) ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ IsLimit (Fork.ofι (P.map (F.map π).op) ⋯)
have refine_2 : F.map c.fst ≫ F.map π = F.map c.snd ≫ F.map π
Tactic: refine (hP (F.map π) (PullbackCone.mk (F.map c.fst) (F.map c.snd) ?_) ?_).some
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
refine_2 : F.map c.fst ≫ F.map π = F.map c.snd ≫ F.map π
⊢ IsLimit (Fork.ofι (P.map (F.map π).op) ⋯)
have refine_2₁ : IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) sorry)
Tactic: refine (hP (F.map π) (PullbackCone.mk (F.map c.fst) (F.map c.snd) ?_) ?_).some
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Function.Bijective (α := (fun (X : Type u_4) ↦ X) (P.obj (op B))) (β :=
    (fun (X : Type u_4) ↦ X)
      (↑{x : P.obj (op X) |
            Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.fst.op) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.snd.op) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))} :
        Type u_4))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (mapToEqualizer P π c.fst c.snd ⋯)) :
      (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) →
        (fun (X : Type u_4) ↦ X)
          (↑{x : P.obj (op X) |
                (ConcreteCategory.hom (P.map c.fst.op) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                    x =
                  (ConcreteCategory.hom (P.map c.snd.op) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                    x} :
            Type u_4))
have hP₁ : Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) sorry))
Tactic: specialize hP π _ hc
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
hP : Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) ⋯))
⊢ Function.Bijective (α := (fun (X : Type u_4) ↦ X) (P.obj (op B))) (β :=
    (fun (X : Type u_4) ↦ X)
      (↑{x : P.obj (op X) |
            Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.fst.op) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.snd.op) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))} :
        Type u_4))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (mapToEqualizer P π c.fst c.snd ⋯)) :
      (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) →
        (fun (X : Type u_4) ↦ X)
          (↑{x : P.obj (op X) |
                (ConcreteCategory.hom (P.map c.fst.op) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                    x =
                  (ConcreteCategory.hom (P.map c.snd.op) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                    x} :
            Type u_4))
have hP₁ : ∀ (y : P.obj (op X)),
  Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.fst.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
          y :
        (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.snd.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
          y :
        (fun (X : Type u_4) ↦ X) (P.obj (op c.pt))) →
    ∃! x : P.obj (op B),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map π.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) → (fun (X : Type u_4) ↦ X) (P.obj (op X)))
          x =
        y
Tactic: rw [Types.type_equalizer_iff_unique] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
hP :
  Function.Bijective (α := (fun (X : Type u_4) ↦ X) (P.obj (op B))) (β :=
    (fun (X : Type u_4) ↦ X)
      (↑{x : P.obj (op X) |
            Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.fst.op) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.snd.op) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))} :
        Type u_4))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (mapToEqualizer P π c.fst c.snd ⋯)) :
      (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) →
        (fun (X : Type u_4) ↦ X)
          (↑{x : P.obj (op X) |
                (ConcreteCategory.hom (P.map c.fst.op) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                    x =
                  (ConcreteCategory.hom (P.map c.snd.op) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
                    x} :
            Type u_4))
⊢ Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) ⋯))
have rw : ∀ (y : P.obj (op X)),
  Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.fst.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
          y :
        (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.snd.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
          y :
        (fun (X : Type u_4) ↦ X) (P.obj (op c.pt))) →
    ∃! x : P.obj (op B),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map π.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) → (fun (X : Type u_4) ↦ X) (P.obj (op X)))
          x =
        y
Tactic: rw [Types.type_equalizer_iff_unique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
hP :
  ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst_3 : HasPullback π π],
    Function.Bijective (α := (fun (X : Type u_4) ↦ X) (P.obj (op B))) (β :=
      (fun (X : Type u_4) ↦ X)
        (↑{x : P.obj (op X) |
              Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst π π))) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                        (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                    x :
                  (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd π π))) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                        (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                    x :
                  (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))} :
          Type u_4))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) :
        (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) →
          (fun (X : Type u_4) ↦ X)
            (↑{x : P.obj (op X) |
                  (ConcreteCategory.hom (P.map (pullback.fst π π).op) :
                        (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                          (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                      x =
                    (ConcreteCategory.hom (P.map (pullback.snd π π).op) :
                        (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                          (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                      x} :
              Type u_4))
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) ⋯))
have this : HasPullback π π
Tactic: have : HasPullback π π := ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  Function.Bijective (α := (fun (X : Type u_4) ↦ X) (P.obj (op B))) (β :=
    (fun (X : Type u_4) ↦ X)
      (↑{x : P.obj (op X) |
            Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst π π))) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                      (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd π π))) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                      (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))} :
        Type u_4))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) :
      (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) →
        (fun (X : Type u_4) ↦ X)
          (↑{x : P.obj (op X) |
                (ConcreteCategory.hom (P.map (pullback.fst π π).op) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                        (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                    x =
                  (ConcreteCategory.hom (P.map (pullback.snd π π).op) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                        (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                    x} :
            Type u_4))
⊢ Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) ⋯))
have rw : ∀ (y : P.obj (op X)),
  Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.fst.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
          y :
        (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.snd.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
          y :
        (fun (X : Type u_4) ↦ X) (P.obj (op c.pt))) →
    ∃! x : P.obj (op B),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map π.op) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) → (fun (X : Type u_4) ↦ X) (P.obj (op X)))
          x =
        y
Tactic: rw [Types.type_equalizer_iff_unique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀
    (b :
      (fun (X : Type u_4) ↦ X)
        (↑{x : P.obj (op X) |
              Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst π π))) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                        (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                    x :
                  (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd π π))) :
                      (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                        (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                    x :
                  (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))} :
          Type u_4)),
    ∃! a : (fun (X : Type u_4) ↦ X) (P.obj (op B)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯) :
            (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) →
              (fun (X : Type u_4) ↦ X)
                (↑{x : P.obj (op X) |
                      (ConcreteCategory.hom (P.map (pullback.fst π π).op) :
                            (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                              (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                          x =
                        (ConcreteCategory.hom (P.map (pullback.snd π π).op) :
                            (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                              (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                          x} :
                  Type u_4))
          a =
        b
b : P.obj (op X)
hb :
  Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.fst.op) :
          (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
        b :
      (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map c.snd.op) :
          (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
        b :
      (fun (X : Type u_4) ↦ X) (P.obj (op c.pt)))
⊢ ∃! x : P.obj (op B),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map π.op) :
          (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) → (fun (X : Type u_4) ↦ X) (P.obj (op X)))
        x =
      b
have h₁ : Eq (α := (PullbackCone.mk (W := pullback π π) (pullback.fst π π) (pullback.snd π π) sorry).pt ⟶ X)
  (Iso.hom (IsLimit.conePointUniqueUpToIso (pullbackIsPullback π π) hc) ≫ c.fst) (pullback.fst π π)
Tactic: have h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst =
    pullback.fst π π := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
X B : C
π : X ⟶ B
inst_1 : HasPullback π π
⊢ Eq (α :=
    P.obj (op B) ⟶
      (↑{x : P.obj (op X) |
            Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst π π))) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                      (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd π π))) :
                    (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) →
                      (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
                  x :
                (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))} :
        Type u_4))
    (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
    (equalizer.lift (P.map π.op) ⋯ ≫
      Iso.hom
        (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))
have rw : Eq (α :=
  P.obj (op B) ⟶
    equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
      (P.map (Quiver.Hom.op (pullback.snd π π))))
  (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) sorry ≫
    Iso.inv (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))
  (equalizer.lift (P.map π.op) sorry)
Tactic: rw [← Iso.comp_inv_eq (α := Types.equalizerIso _ _)]