-- 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
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))
⊢ ∀
    (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

Tactic:
rw [Function.bijective_iff_existsUnique] at hP

Premises used: Function.bijective_iff_existsUnique