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
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₂ :
  i =
    CategoryStruct.comp (Y :=
      unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯)))
      (Quiver.Hom.unop
        (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 ⋯))))
      (Quiver.Hom.unop
        (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 ⋯))))
⊢ 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 ⋯)))

Tactic:
congr
-- 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) ⋯
⊢ i =
    CategoryStruct.comp (Y :=
      unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯)))
      (Quiver.Hom.unop
        (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 ⋯))))
      (Quiver.Hom.unop
        (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 ⋯))))

Tactic:
aesop
-- 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₂ :
  j =
    CategoryStruct.comp (Y :=
      unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯)))
      (Quiver.Hom.unop
        (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 ⋯))))
      (Quiver.Hom.unop
        (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 ⋯))))
⊢ 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 ⋯)))

Tactic:
congr
-- 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) ⋯
⊢ j =
    CategoryStruct.comp (Y :=
      unop (op (categoryMk (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)) (c.fst ≫ π) ⋯)))
      (Quiver.Hom.unop
        (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 ⋯))))
      (Quiver.Hom.unop
        (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:
aesop
-- 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
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve.{v_1, u_1} B := Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : Functor.{0, v_2, 0, u_2} WalkingParallelPair D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
⊢ H.Initial

Tactic:
have : H.Initial := parallelPair_pullback_initial π c hc
-- 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
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve.{v_1, u_1} B := Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : Functor.{0, v_2, 0, u_2} WalkingParallelPair D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
⊢ (H ⋙ F).map WalkingParallelPairHom.left ≫ Iso.hom (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) ≫ G.map WalkingParallelPairHom.left

Tactic:
aesop
-- 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
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve.{v_1, u_1} B := Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : Functor.{0, v_2, 0, u_2} WalkingParallelPair D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
⊢ (H ⋙ F).map WalkingParallelPairHom.right ≫ Iso.hom (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) ≫ G.map WalkingParallelPairHom.right

Tactic:
aesop
-- 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
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve.{v_1, u_1} B := Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : Functor.{0, v_2, 0, u_2} WalkingParallelPair D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
i : H ⋙ F ≅ G :=
  parallelPair.ext (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) ⋯
    ⋯
refine :
  (Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯) ≅
    Cone.whisker H
      (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))
⊢ IsLimit (Fork.ofι (P.map π.op) ⋯) ≃
    IsLimit (J :=
      (Presieve.category.{v_1, u_1} (C := C) (X := B)
          (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
      (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))

Tactic:
refine (IsLimit.equivOfNatIsoOfIso i.symm _ _ ?_).trans (Functor.Initial.isLimitWhiskerEquiv H _)

Premises used: CategoryTheory.Functor.Initial.isLimitWhiskerEquiv, Equiv.trans, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- 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
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve.{v_1, u_1} B := Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : Functor.{0, v_2, 0, u_2} WalkingParallelPair D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
i : H ⋙ F ≅ G :=
  parallelPair.ext (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) ⋯
    ⋯
refine :
  ∀ (j : WalkingParallelPair),
    ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).π.app j =
      Iso.hom (Iso.refl ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).pt) ≫
        (Cone.whisker H
                (P.mapCone
                  (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))).π.app
          j
⊢ (Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯) ≅
    Cone.whisker H
      (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))

Tactic:
refine Cone.ext (Iso.refl _) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- 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
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve.{v_1, u_1} B := Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : Functor.{0, v_2, 0, u_2} WalkingParallelPair D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
i : H ⋙ F ≅ G :=
  parallelPair.ext (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) ⋯
    ⋯
⊢ ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).π.app WalkingParallelPair.zero =
    Iso.hom (Iso.refl ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).pt) ≫
      (Cone.whisker H
              (P.mapCone
                (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))).π.app
        WalkingParallelPair.zero

Tactic:
aesop
-- 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
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve.{v_1, u_1} B := Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (P := fun (f : Over.{v_1, u_1} B) ↦ S f.hom) (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : Functor.{0, v_2, 0, u_2} WalkingParallelPair D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
i : H ⋙ F ≅ G :=
  parallelPair.ext (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)) (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)) ⋯
    ⋯
⊢ ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).π.app WalkingParallelPair.one =
    Iso.hom (Iso.refl ((Cone.postcompose i.symm.hom).obj (Fork.ofι (P.map π.op) ⋯)).pt) ≫
      (Cone.whisker H
              (P.mapCone
                (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))).π.app
        WalkingParallelPair.one

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
X B : C
π : X ⟶ B
inst_2 : HasPullback π π
mp :
  SingleEqualizerCondition P π →
    Nonempty
      (IsLimit (J :=
        (Presieve.category.{v_1, u_1} (C := C) (X := B)
            (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
        (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))))))
mpr :
  Nonempty
      (IsLimit (J :=
        (Presieve.category.{v_1, u_1} (C := C) (X := B)
            (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
        (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))) →
    SingleEqualizerCondition P π
⊢ SingleEqualizerCondition P π ↔
    Nonempty
      (IsLimit (J :=
        (Presieve.category.{v_1, u_1} (C := C) (X := B)
            (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
        (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))))))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
X B : C
π : X ⟶ B
inst_2 : HasPullback π π
h : SingleEqualizerCondition P π
⊢ Nonempty
    (IsLimit (J :=
      (Presieve.category.{v_1, u_1} (C := C) (X := B)
          (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
      (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))))))

Tactic:
⟨isLimit_forkOfι_equiv _ _ _ (pullbackIsPullback π π) (h _ (pullbackIsPullback π π)).some⟩

Premises used: Nonempty.some, CategoryTheory.Limits.pullbackIsPullback, Nonempty.intro, CategoryTheory.regularTopology.isLimit_forkOfι_equiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
X B : C
π : X ⟶ B
inst_2 : HasPullback π π
h : SingleEqualizerCondition P π
⊢ Nonempty
    (IsLimit (J :=
      (Presieve.category.{v_1, u_1} (C := C) (X := B)
          (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
      (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π))))))

Tactic:
exact ⟨isLimit_forkOfι_equiv _ _ _ (pullbackIsPullback π π) (h _ (pullbackIsPullback π π)).some⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
X B : C
π : X ⟶ B
inst_2 : HasPullback π π
h :
  IsLimit (J :=
    (Presieve.category.{v_1, u_1} (C := C) (X := B)
        (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
    (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))
⊢ SingleEqualizerCondition P π

Tactic:
fun c hc ↦ ⟨(isLimit_forkOfι_equiv _ _ _ hc).symm h⟩

Premises used: Nonempty.intro, CategoryTheory.regularTopology.isLimit_forkOfι_equiv, Equiv.symm, CategoryTheory.regularTopology.SingleEqualizerCondition, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
X B : C
π : X ⟶ B
inst_2 : HasPullback π π
h :
  IsLimit (J :=
    (Presieve.category.{v_1, u_1} (C := C) (X := B)
        (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))ᵒᵖ)
    (P.mapCone (Cocone.op (cocone (Sieve.arrows (Sieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ π)))))
⊢ SingleEqualizerCondition P π

Tactic:
exact fun c hc ↦ ⟨(isLimit_forkOfι_equiv _ _ _ hc).symm h⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : Preregular.{v_1, u_1} C
inst_3 : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
rw :
  EqualizerCondition F ↔
    ∀ ⦃X : C⦄ (R : Presieve.{v_1, u_1} X),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
          (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) R →
        Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
⊢ EqualizerCondition F ↔ Presheaf.IsSheaf (Coverage.toGrothendieck (regularCoverage C)) F

Tactic:
rw [Presheaf.isSheaf_iff_isLimit_coverage]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : Preregular.{v_1, u_1} C
inst_3 : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
mp :
  EqualizerCondition F →
    ∀ ⦃X : C⦄ (R : Presieve.{v_1, u_1} X),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
          (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) R →
        Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
mpr :
  (∀ ⦃X : C⦄ (R : Presieve.{v_1, u_1} X),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
          (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) R →
        Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))) →
    EqualizerCondition F
⊢ EqualizerCondition F ↔
    ∀ ⦃X : C⦄ (R : Presieve.{v_1, u_1} X),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
          (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) R →
        Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : Preregular.{v_1, u_1} C
inst_3 : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
hF : EqualizerCondition F
X Y : C
f : Y ⟶ X
right : EffectiveEpi f
⊢ Nonempty
    (IsLimit (J :=
      (Presieve.category.{v_1, u_1} (C := C) (X := X)
          (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))))ᵒᵖ)
      (F.mapCone
        (Cocone.op (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))))))

Tactic:
(equalizerConditionMap_iff_nonempty_isLimit F f).1 (hF f)

Premises used: CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, Iff.mp