-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves (hypothesis)
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)
hP :
  ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] (c : PullbackCone π π) (x : IsLimit c),
    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))
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) ⋯))
have 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 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 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))
Tactic: specialize hP X B π c hc
Cleared hypotheses: hP