-- 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 :
  ∀ (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
b : P.obj (op X)
hb :
  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)))}
    b
a : P.obj (op B)
ha₁ :
  (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)))
      a =
    b
ha₂ :
  ∀ (y : P.obj (op B)),
    (fun (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)
        y →
      y = a
y : P.obj (op B)
h :
  (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 =
    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
⊢ (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

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

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