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)
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:
exact 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
-- 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 :
  ∀ (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 π π],
    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))
⊢ EqualizerCondition P

Tactic:
apply EqualizerCondition.mk

Premises used: CategoryTheory.regularTopology.EqualizerCondition.mk
-- 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 :
  ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst_4 : 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) ⋯)
X B : C
π : X ⟶ B
inst_1 : EffectiveEpi π
inst_2 : HasPullback π π
⊢ 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:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
e : Equivalence.{v_1, v_3, u_1, u_3} C E
⊢ EqualizerCondition P ↔ EqualizerCondition (e.op.inverse ⋙ P)

Tactic:
⟨fun h ↦ equalizerCondition_precomp_of_preservesPullback P e.inverse h, fun h ↦
    equalizerCondition_of_natIso (e.op.funInvIdAssoc P)
      (equalizerCondition_precomp_of_preservesPullback (e.op.inverse ⋙ P) e.functor h)⟩

Premises used: CategoryTheory.regularTopology.equalizerCondition_precomp_of_preservesPullback, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.op, CategoryTheory.Equivalence.functor, CategoryTheory.Equivalence.funInvIdAssoc, Iff.intro, CategoryTheory.regularTopology.equalizerCondition_of_natIso, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
h₁ :
  ∀
    (Z :
      (Presieve.category.{v_1, u_1} (C := C) (X := B)
          (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ),
    Nonempty.{v_1 + 1} (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ Z)
h₂ :
  ∀
    ⦃Z :
      (Presieve.category.{v_1, u_1} (C := C) (X := B)
          (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ⦄
    (i j : op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ Z),
    ∃ (a : op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯) ⟶ Z),
      i =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)) ≫
            a ∧
        j =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯)) ≫
            a
⊢ Initial (D :=
    (Presieve.category.{v_1, u_1} (C := C) (X := B)
        (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
    (parallelPair (X := op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯))
      (Y := op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯))
      (Quiver.Hom.op
        (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)))
      (Quiver.Hom.op
        (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯))))

Tactic:
apply Limits.parallelPair_initial_mk

Premises used: CategoryTheory.Limits.parallelPair_initial_mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
h₁ :
  ∀ ⦃Y : C⦄ (i : Unit)
    (f :
      Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
            Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).left ⟶
        X)
    (hh :
      f ≫ π =
        Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
            Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).hom),
    Nonempty.{v_1 + 1}
      (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ op Z)
⊢ Nonempty.{v_1 + 1}
    (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ op Z)

Tactic:
obtain ⟨_, f, g, ⟨⟩, hh⟩ := Z.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
Y : C
i : Unit
f :
  Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).left ⟶
    X
hh :
  f ≫ π =
    Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).hom
X' : Presieve.category.{v_1, u_1} (C := C) (X := B)
  (ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
    | PUnit.unit => π) :=
  categoryMk
    (ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
      | PUnit.unit => π)
    π ⋯
f' : Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
      Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).left ⟶
  X'.obj (P := fun (f : Over.{v_1, u_1} B) ↦
      ofArrows (fun (x : Unit) ↦ X)
        (fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
          | PUnit.unit => π)
        f.hom).left :=
  f
⊢ Nonempty.{v_1 + 1}
    (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ op Z)

Tactic:
⟨(ObjectProperty.homMk (Over.homMk f')).op⟩

Premises used: Quiver.Hom.op, Nonempty.intro, CategoryTheory.Over.homMk, CategoryTheory.ObjectProperty.homMk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
Y : C
i : Unit
f :
  Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).left ⟶
    X
hh :
  f ≫ π =
    Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).hom
X' : Presieve.category.{v_1, u_1} (C := C) (X := B)
  (ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
    | PUnit.unit => π) :=
  categoryMk
    (ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
      | PUnit.unit => π)
    π ⋯
f' : Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
      Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).left ⟶
  X'.obj (P := fun (f : Over.{v_1, u_1} B) ↦
      ofArrows (fun (x : Unit) ↦ X)
        (fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
          | PUnit.unit => π)
        f.hom).left :=
  f
⊢ Nonempty.{v_1 + 1}
    (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ op Z)

Tactic:
exact ⟨(ObjectProperty.homMk (Over.homMk f')).op⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
h₂ :
  ∀
    (i :
      unop (op Z) ⟶ unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯)))
    (j : op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ op Z),
    ∃ (a :
      op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯) ⟶ op Z),
      op i =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)) ≫
            a ∧
        j =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯)) ≫
            a
⊢ ∀ (i j : op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ op Z),
    ∃ (a :
      op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯) ⟶ op Z),
      i =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)) ≫
            a ∧
        j =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯)) ≫
            a

Tactic:
⟨i⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
i : unop (op Z) ⟶ unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯))
h₂ :
  ∀
    (j :
      unop (op Z) ⟶ unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯))),
    ∃ (a :
      op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯) ⟶ op Z),
      op i =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)) ≫
            a ∧
        op j =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯)) ≫
            a
⊢ ∀ (j : op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯) ⟶ op Z),
    ∃ (a :
      op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯) ⟶ op Z),
      op i =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)) ≫
            a ∧
        j =
          Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
                Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯)) ≫
            a

Tactic:
⟨j⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
i j : unop (op Z) ⟶ unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯))
⊢ Over.Hom.left i.hom ≫
      (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom)
          (unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯)))).hom =
    (unop (op Z)).obj (P := fun (f : Over.{v_1, u_1} B) ↦
        Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).hom

Tactic:
have hi := Over.w i.hom
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
i j : unop (op Z) ⟶ unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯))
hi :
  Over.Hom.left i.hom ≫
      (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom)
          (unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯)))).hom =
    (unop (op Z)).obj (P := fun (f : Over.{v_1, u_1} B) ↦
        Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).hom
⊢ Over.Hom.left j.hom ≫
      (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom)
          (unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯)))).hom =
    (unop (op Z)).obj (P := fun (f : Over.{v_1, u_1} B) ↦
        Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).hom

Tactic:
have hj := Over.w j.hom
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
i j : unop (op Z) ⟶ unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯))
hi :
  Over.Hom.left i.hom ≫ π =
    Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        ∃ (Y : C) (h : f.left ⟶ Y) (g : Y ⟶ B),
          ofArrows (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ π) g ∧ h ≫ g = f.hom).hom
hj :
  Over.Hom.left j.hom ≫ π =
    Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        ∃ (Y : C) (h : f.left ⟶ Y) (g : Y ⟶ B),
          ofArrows (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ π) g ∧ h ≫ g = f.hom).hom
⊢ Over.Hom.left i.hom ≫ π = Over.Hom.left j.hom ≫ π

Tactic:
simp [hi, hj]
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
i j : unop (op Z) ⟶ unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯))
hi :
  Over.Hom.left i.hom ≫ π =
    Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        ∃ (Y : C) (h : f.left ⟶ Y) (g : Y ⟶ B),
          ofArrows (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ π) g ∧ h ≫ g = f.hom).hom
hj :
  Over.Hom.left j.hom ≫ π =
    Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        ∃ (Y : C) (h : f.left ⟶ Y) (g : Y ⟶ B),
          ofArrows (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ π) g ∧ h ≫ g = f.hom).hom
ij : (unop (op Z)).obj (P := fun (f : Over.{v_1, u_1} B) ↦
      Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).left ⟶
  c.pt :=
  PullbackCone.IsLimit.lift hc (Over.Hom.left i.hom) (Over.Hom.left j.hom) ⋯
⊢ ∃ (a : op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯) ⟶ op Z),
    op i =
        Quiver.Hom.op
            (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
              Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)) ≫
          a ∧
      op j =
        Quiver.Hom.op
            (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
              Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯)) ≫
          a

Tactic:
⟨Quiver.Hom.op (ObjectProperty.homMk (Over.homMk ij)), ?_, ?_⟩

Premises used: Quiver.Hom.op, CategoryTheory.Over.homMk, And.intro, CategoryTheory.ObjectProperty.homMk, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z :
  Presieve.category.{v_1, u_1} (C := C) (X := B) (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))
i j : unop (op Z) ⟶ unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) π ⋯))
hi :
  Over.Hom.left i.hom ≫ π =
    Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        ∃ (Y : C) (h : f.left ⟶ Y) (g : Y ⟶ B),
          ofArrows (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ π) g ∧ h ≫ g = f.hom).hom
hj :
  Over.Hom.left j.hom ≫ π =
    Z.obj (P := fun (f : Over.{v_1, u_1} B) ↦
        ∃ (Y : C) (h : f.left ⟶ Y) (g : Y ⟶ B),
          ofArrows (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ π) g ∧ h ≫ g = f.hom).hom
ij : (unop (op Z)).obj (P := fun (f : Over.{v_1, u_1} B) ↦
      Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom).left ⟶
  c.pt :=
  PullbackCone.IsLimit.lift hc (Over.Hom.left i.hom) (Over.Hom.left j.hom) ⋯
h₂ :
  op i =
    CategoryStruct.comp (Y :=
      op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯))
      (Quiver.Hom.op
        (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)))
      (Quiver.Hom.op
        (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk ij ⋯)))
h₃ :
  op j =
    CategoryStruct.comp (Y :=
      op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯))
      (Quiver.Hom.op
        (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯)))
      (Quiver.Hom.op
        (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
          Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk ij ⋯)))
⊢ ∃ (a : op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯) ⟶ op Z),
    op i =
        Quiver.Hom.op
            (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
              Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.fst ⋯)) ≫
          a ∧
      op j =
        Quiver.Hom.op
            (ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦
              Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π) f.hom) (Over.homMk c.snd ⋯)) ≫
          a

Tactic:
refine ⟨Quiver.Hom.op (ObjectProperty.homMk (Over.homMk ij)), ?_, ?_⟩