awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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
⊢ 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:
simp only [Functor.comp_map, op_map, Quiver.Hom.unop_op, ← map_comp, ← op_comp, c.condition]

Premises used: CategoryTheory.op_comp, Quiver.Hom.unop_op, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.op_map
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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 π
refine_2₁ : IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)
⊢ IsLimit (Fork.ofι (P.map (F.map π).op) ⋯)

Tactic:
refine (hP (F.map π) (PullbackCone.mk (F.map c.fst) (F.map c.snd) ?_) ?_).some

Premises used: CategoryTheory.Limits.PullbackCone.fst, Nonempty.some, CategoryTheory.Functor.map, CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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
⊢ F.map c.fst ≫ F.map π = F.map c.snd ≫ F.map π

Tactic:
simp only [← map_comp, c.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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
⊢ c.fst = Iso.hom (Iso.refl c.pt) ≫ (PullbackCone.mk c.fst c.snd ⋯).fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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
⊢ c.snd = Iso.hom (Iso.refl c.pt) ≫ (PullbackCone.mk c.fst c.snd ⋯).snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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 (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)

Tactic:
exact (isLimitMapConePullbackConeEquiv F c.condition)
        (isLimitOfPreserves F (hc.ofIsoLimit (PullbackCone.ext (Iso.refl _) (by simp) (by simp))))

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Iso.refl, CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, CategoryTheory.Limits.PullbackCone.ext, CategoryTheory.Limits.IsLimit.ofIsoLimit, DFunLike.coe, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
W X B : C
f : X ⟶ B
g₁ g₂ : W ⟶ X
w : g₁ ≫ f = g₂ ≫ f
t : P.obj (op B)
⊢ Membership.mem (α := P.obj (op X)) (γ := Set (P.obj (op X)))
    {x : P.obj (op X) |
      Eq (α := (fun (X : Type u_4) ↦ X) (P.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
              (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op W)))
            x :
          (fun (X : Type u_4) ↦ X) (P.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
              (a : (fun (X : Type u_4) ↦ X) (P.obj (op X))) → (fun (X : Type u_4) ↦ X) (P.obj (op W)))
            x :
          (fun (X : Type u_4) ↦ X) (P.obj (op W)))}
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) → (fun (X : Type u_4) ↦ X) (P.obj (op X)))
        t :
      (fun (X : Type u_4) ↦ X) (P.obj (op X)))

Tactic:
simp only [Set.mem_setOf_eq, ← comp_apply, ← Functor.map_comp, ← op_comp, w]

Premises used: CategoryTheory.op_comp, Set.mem_setOf_eq, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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
⊢ Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) ⋯))

Tactic:
specialize hP π _ hc
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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) ⋯))
⊢ ∀ (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

Premises used: CategoryTheory.Limits.Types.type_equalizer_iff_unique
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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 π
inst_2 : 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))

Tactic:
bijective_mapToEqualizer_pullback' hP _ (pullback.isLimit _ _)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback', Set.Mem, setOf, CategoryTheory.Limits.pullback.isLimit, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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 π] (c : PullbackCone π π) (x : 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))
X B : C
π : X ⟶ B
_ : ∀ [EffectiveEpi π], SingleEqualizerCondition P π
⊢ ∀ [EffectiveEpi π], SingleEqualizerCondition P π

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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 π] (c : PullbackCone π π) (x : 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))
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))

Tactic:
specialize hP X B π c hc
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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))
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
⊢ Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique]

Premises used: CategoryTheory.Limits.Types.type_equalizer_iff_unique
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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_2 : 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
_ : ∀ [EffectiveEpi π], SingleEqualizerCondition P π
⊢ ∀ [EffectiveEpi π], SingleEqualizerCondition P π

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
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
⊢ HasPullback π π

Tactic:
have : HasPullback π π := ⟨c, hc⟩