awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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 (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))
rw :
  ∀ (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
⊢ Nonempty.{u_4 + 2} (IsLimit (Fork.ofι (P.map π.op) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique]

Premises used: CategoryTheory.Limits.Types.type_equalizer_iff_unique
-- 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)))
⊢ Eq (α := (PullbackCone.mk (W := pullback π π) (pullback.fst π π) (pullback.snd π π) ⋯).pt ⟶ X)
    (Iso.hom (IsLimit.conePointUniqueUpToIso (pullbackIsPullback π π) hc) ≫ c.fst) (pullback.fst π π)

Tactic:
simp
-- 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)))
⊢ Eq (α := (PullbackCone.mk (W := pullback π π) (pullback.fst π π) (pullback.snd π π) ⋯).pt ⟶ X)
    (Iso.hom (IsLimit.conePointUniqueUpToIso (pullbackIsPullback π π) hc) ≫ c.fst) (pullback.fst π π)

Tactic:
have h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst =
    pullback.fst π π := by simp
-- 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 : HasPullback π π
⊢ Eq (α := P.obj (op B) ⟶ P.obj (op (pullback π π))) (P.map π.op ≫ P.map (Quiver.Hom.op (pullback.fst π π)))
    (P.map π.op ≫ P.map (Quiver.Hom.op (pullback.snd π π)))

Tactic:
simp only [← Functor.map_comp, ← op_comp, pullback.condition]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition
-- 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 : HasPullback π π
rw :
  Eq (α :=
    P.obj (op B) ⟶
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
    (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
      Iso.inv
        (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))
    (equalizer.lift (P.map π.op) ⋯)
⊢ Eq (α :=
    P.obj (op B) ⟶
      (↑{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))
    (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
    (equalizer.lift (P.map π.op) ⋯ ≫
      Iso.hom
        (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))

Tactic:
rw [← Iso.comp_inv_eq (α := Types.equalizerIso _ _)]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.Types.equalizerIso
-- 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 : HasPullback π π
h :
  CategoryStruct.comp (Y :=
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
      (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
        Iso.inv
          (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))
      (equalizer.ι (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))) =
    CategoryStruct.comp (Y :=
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
      (equalizer.lift (P.map π.op) ⋯)
      (equalizer.ι (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π))))
⊢ Eq (α :=
    P.obj (op B) ⟶
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
    (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
      Iso.inv
        (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))
    (equalizer.lift (P.map π.op) ⋯)

Tactic:
apply equalizer.hom_ext

Premises used: CategoryTheory.Limits.equalizer.hom_ext
-- 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 : HasPullback π π
⊢ CategoryStruct.comp (Y :=
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
      (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
        Iso.inv
          (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))
      (equalizer.ι (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))) =
    CategoryStruct.comp (Y :=
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
      (equalizer.lift (P.map π.op) ⋯)
      (equalizer.ι (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π))))

Tactic:
aesop
-- 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)
mp :
  EqualizerCondition P →
    ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst_2 : HasPullback π π],
      IsIso (Y :=
        equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
          (P.map (Quiver.Hom.op (pullback.snd π π))))
        (equalizer.lift (P.map π.op) ⋯)
mpr :
  (∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst_2 : HasPullback π π],
      IsIso (Y :=
        equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
          (P.map (Quiver.Hom.op (pullback.snd π π))))
        (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P
⊢ EqualizerCondition P ↔
    ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst_2 : HasPullback π π],
      IsIso (Y :=
        equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
          (P.map (Quiver.Hom.op (pullback.snd π π))))
        (equalizer.lift (P.map π.op) ⋯)

Tactic:
constructor
-- 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)
hP : EqualizerCondition P
X B : C
π : X ⟶ B
mp :
  ∀ [EffectiveEpi π] [inst_2 : HasPullback π π],
    IsIso (Y :=
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
      (equalizer.lift (P.map π.op) ⋯)
⊢ ∀ [EffectiveEpi π] [inst_2 : HasPullback π π],
    IsIso (Y :=
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
      (equalizer.lift (P.map π.op) ⋯)

Tactic:
_
-- 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)
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
mp :
  ∀ [inst_2 : HasPullback π π],
    IsIso (Y :=
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
      (equalizer.lift (P.map π.op) ⋯)
⊢ ∀ [inst_2 : HasPullback π π],
    IsIso (Y :=
      equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
        (P.map (Quiver.Hom.op (pullback.snd π π))))
      (equalizer.lift (P.map π.op) ⋯)

Tactic:
_
-- 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)
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
inst_2 : HasPullback π π
⊢ 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 (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))

Tactic:
have h := hP.bijective_mapToEqualizer_pullback π
-- 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)
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
inst_2 : HasPullback π π
h :
  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 (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))
⊢ IsIso (Y :=
    (↑{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))
    (equalizer.lift (P.map π.op) ⋯ ≫
      Iso.hom
        (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))

Tactic:
rw [← isIso_iff_bijective, mapToEqualizer_eq_comp] at h

Premises used: CategoryTheory.isIso_iff_bijective, CategoryTheory.regularTopology.mapToEqualizer_eq_comp
-- 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)
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
inst_2 : HasPullback π π
h :
  IsIso (Y :=
    (↑{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))
    (equalizer.lift (P.map π.op) ⋯ ≫
      Iso.hom
        (Types.equalizerIso (P.map (Quiver.Hom.op (pullback.fst π π))) (P.map (Quiver.Hom.op (pullback.snd π π)))))
⊢ IsIso (Y :=
    equalizer (Y := P.obj (op (pullback π π))) (P.map (Quiver.Hom.op (pullback.fst π π)))
      (P.map (Quiver.Hom.op (pullback.snd π π))))
    (equalizer.lift (P.map π.op) ⋯)

Tactic:
IsIso.of_isIso_comp_right (equalizer.lift (P.map π.op)
      (equalizerCondition_w' P π))
      (Types.equalizerIso _ _).hom

Premises used: Quiver.Hom.op, CategoryTheory.Limits.Types.equalizerIso, CategoryTheory.Limits.equalizer.lift, CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.Functor.map, CategoryTheory.regularTopology.equalizerCondition_w', CategoryTheory.Iso.hom