-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (goal)
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
⊢ 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))
have rw : ∀
  (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 sorry) :
          (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
Tactic: rw [Function.bijective_iff_existsUnique]