-- 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 :
  ∀
    (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)),
    ∃! a : (fun (X : Type u_4) ↦ X) (P.obj (op B)),
      (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))
          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)))
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 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))
        a :
      (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))
    (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 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)))}
          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 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)))}
          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 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))
                a :
              (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))
            (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 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)))}
                  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 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)))}
                  x }))
        y →
      y = a
y : P.obj (op B)
h :
  (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)))
      y =
    b
⊢ Eq (α :=
    (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))
        y :
      (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))
    (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 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)))}
          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 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)))}
          x })

Tactic:
simpa [mapToEqualizer, Subtype.ext_iff] using h

Premises used: CategoryTheory.regularTopology.mapToEqualizer, Subtype.ext_iff