-- 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 :
  ∀
    (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)))
h₁ :
  Eq (α := (PullbackCone.mk (W := pullback π π) (pullback.fst π π) (pullback.snd π π) ⋯).pt ⟶ X)
    (Iso.hom (IsLimit.conePointUniqueUpToIso (pullbackIsPullback π π) hc) ≫ c.fst) (pullback.fst π π)
hb' :
  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 π π))))
        b :
      (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 π π))))
        b :
      (fun (X : Type u_4) ↦ X) (P.obj (op (pullback π π))))
obtain :
  ∀ (a : P.obj (op B))
    (ha₁ :
      Eq (α :=
        (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))
            a :
          (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))
        (Subtype.mk (p := fun (x : P.obj (op X)) ↦
            Membership.mem (γ := Set (P.obj (op 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 π π))))}
              x)
            b hb' :
          { x : P.obj (op X) //
            Membership.mem (γ := Set (P.obj (op 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 π π))))}
              x }))
    (ha₂ :
      ∀ (y : (fun (X : Type u_4) ↦ X) (P.obj (op B))),
        (fun (a : (fun (X : Type u_4) ↦ X) (P.obj (op B))) ↦
              Eq (α :=
                (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))
                    a :
                  (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))
                (Subtype.mk (p := fun (x : P.obj (op X)) ↦
                    Membership.mem (γ := Set (P.obj (op 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 π π))))}
                      x)
                    b hb' :
                  { x : P.obj (op X) //
                    Membership.mem (γ := Set (P.obj (op 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 π π))))}
                      x }))
            y →
          y = a),
    ∃! 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
⊢ ∃! 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

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := hP ⟨b, hb'⟩

Premises used: Subtype.mk