awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
hP : IsSheaf J P
X : C
S : J.Cover X
rw :
  (hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) →
    {X : C} → (S : J.Cover X) → IsLimit (S.multifork P)
⊢ IsLimit (S.multifork P)

Tactic:
rw [Presheaf.isSheaf_iff_multifork] at hP

Premises used: CategoryTheory.Presheaf.isSheaf_iff_multifork
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
⊢ IsLimit (S.multifork P)

Tactic:
exact (hP X S).some

Premises used: Nonempty.some
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
rw :
  (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
⊢ IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)

Tactic:
rw [isSheaf_iff_multifork]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_multifork
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)

Tactic:
forall₂_congr fun X S => ⟨?_, ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
refine_1 :
  ∀ (X : C) (S : J.Cover X),
    Nonempty (IsLimit (S.multifork P)) → IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
refine_2 :
  ∀ (X : C) (S : J.Cover X),
    IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P) → Nonempty (IsLimit (S.multifork P))
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)

Tactic:
refine forall₂_congr fun X S => ⟨?_, ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsLimit (S.multifork P)
e : P.obj (op X) ≅ multiequalizer (S.index P) := h.conePointUniqueUpToIso (limit.isLimit (S.index P).multicospan)
⊢ IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)

Tactic:
(inferInstance : IsIso e.hom)

Premises used: inferInstance, CategoryTheory.Limits.limit.lift
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsLimit (S.multifork P)
e : P.obj (op X) ≅ multiequalizer (S.index P) := h.conePointUniqueUpToIso (limit.isLimit (S.index P).multicospan)
⊢ IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)

Tactic:
exact (inferInstance : IsIso e.hom)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
⊢ Nonempty (IsLimit (S.multifork P))

Tactic:
⟨IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ?_ ?_)⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
refine_2 : (limit.cone (S.index P).multicospan).pt ≅ (S.multifork P).pt
refine_2₁ :
  ∀ (j : WalkingMulticospan S.shape),
    (limit.cone (S.index P).multicospan).π.app j =
      Iso.hom (Iso.symm (asIso (S.toMultiequalizer P))) ≫ (S.multifork P).π.app j
⊢ Nonempty (IsLimit (S.multifork P))

Tactic:
refine ⟨IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ?_ ?_)⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
⊢ (limit.cone (S.index P).multicospan).pt ≅ (S.multifork P).pt

Tactic:
apply (@asIso _ _ _ _ _ h).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
a : WalkingMulticospan S.shape
refine_2 :
  Iso.hom (Iso.symm (asIso (S.toMultiequalizer P))) ≫ (S.multifork P).π.app a =
    (limit.cone (S.index P).multicospan).π.app a
⊢ (limit.cone (S.index P).multicospan).π.app a =
    Iso.hom (Iso.symm (asIso (S.toMultiequalizer P))) ≫ (S.multifork P).π.app a

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
a : WalkingMulticospan S.shape
⊢ Iso.hom (Iso.symm (asIso (S.toMultiequalizer P))) ≫ (S.multifork P).π.app a =
    (limit.cone (S.index P).multicospan).π.app a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : HasProducts A
inst_3 : HasPullbacks.{v₁, u₁} C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
w₁ :
  Eq (α :=
    P.obj (op U) ⟶
      Functor.obj (C := Discrete (((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }))
        (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
          P.obj
            (op
              (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
        {
          as :=
            (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
              Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) })
    (P.map (Quiver.Hom.op (pullback.snd f g ≫ g))) (P.map g.op ≫ P.map (Quiver.Hom.op (pullback.snd f g)))
⊢ Eq (α :=
    P.obj (op U) ⟶
      Functor.obj (C := Discrete (((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }))
        (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
          P.obj
            (op
              (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
        {
          as :=
            (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
              Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) })
    (P.map f.op ≫ P.map (Quiver.Hom.op (pullback.fst f g))) (P.map g.op ≫ P.map (Quiver.Hom.op (pullback.snd f g)))

Tactic:
rw [← P.map_comp, ← op_comp, pullback.condition]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : HasProducts A
inst_3 : HasPullbacks.{v₁, u₁} C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ Eq (α :=
    P.obj (op U) ⟶
      Functor.obj (C := Discrete (((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }))
        (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
          P.obj
            (op
              (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
        {
          as :=
            (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
              Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) })
    (P.map (Quiver.Hom.op (pullback.snd f g ≫ g))) (P.map g.op ≫ P.map (Quiver.Hom.op (pullback.snd f g)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U_1 : C
R_1 : Presieve.{v₁, u₁} U_1
P_1 : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
inst_4 : HasProducts A
inst_5 : HasProducts A'
inst_6 : HasPullbacks.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : A ⥤ Type (max v₁ u₁)
inst_7 : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve.{v₁, u₁} U
e : parallelPair (X := s.obj (firstObj R P)) (Y := s.obj (secondObj R P)) (s.map (firstMap R P))
    (s.map (secondMap R P)) ≅
  parallelPair (Y := Equalizer.Presieve.SecondObj (P ⋙ s) R) (Equalizer.Presieve.firstMap (P ⋙ s) R)
    (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext
    (PreservesProduct.iso s fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
      P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f }))))
    (PreservesProduct.iso s fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
      P.obj
        (op
          (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
            (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
    ⋯ ⋯
refine :
  IsLimit (F :=
      parallelPair (X := s.obj (firstObj R P)) (Y := s.obj (secondObj R P)) (s.map (firstMap R P))
        (s.map (secondMap R P)))
      (Fork.ofι (s.map (forkMap R P)) ⋯) ≃
    IsLimit (F :=
      parallelPair (Y := Equalizer.Presieve.SecondObj (P ⋙ s) R) (Equalizer.Presieve.firstMap (P ⋙ s) R)
        (Equalizer.Presieve.secondMap (P ⋙ s) R))
      (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯)
⊢ IsLimit (F := parallelPair (X := firstObj R P) (Y := secondObj R P) (firstMap R P) (secondMap R P) ⋙ s)
      (s.mapCone (Fork.ofι (forkMap R P) ⋯)) ≃
    IsLimit (F :=
      parallelPair (Y := Equalizer.Presieve.SecondObj (P ⋙ s) R) (Equalizer.Presieve.firstMap (P ⋙ s) R)
        (Equalizer.Presieve.secondMap (P ⋙ s) R))
      (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯)

Tactic:
refine Equiv.trans (isLimitMapConeForkEquiv _ _) ?_

Premises used: Equiv.trans, CategoryTheory.Limits.isLimitMapConeForkEquiv
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U_1 : C
R_1 : Presieve.{v₁, u₁} U_1
P_1 : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
inst_4 : HasProducts A
inst_5 : HasProducts A'
inst_6 : HasPullbacks.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : A ⥤ Type (max v₁ u₁)
inst_7 : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve.{v₁, u₁} U
e : parallelPair (X := s.obj (firstObj R P)) (Y := s.obj (secondObj R P)) (s.map (firstMap R P))
    (s.map (secondMap R P)) ≅
  parallelPair (Y := Equalizer.Presieve.SecondObj (P ⋙ s) R) (Equalizer.Presieve.firstMap (P ⋙ s) R)
    (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext
    (PreservesProduct.iso s fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
      P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f }))))
    (PreservesProduct.iso s fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
      P.obj
        (op
          (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
            (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
    ⋯ ⋯
refine :
  Iso.hom (Iso.refl ((Cone.postcompose e.hom).obj (Fork.ofι (s.map (forkMap R P)) ⋯)).pt) ≫
      Fork.ι (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯) =
    Fork.ι ((Cone.postcompose e.hom).obj (Fork.ofι (s.map (forkMap R P)) ⋯))
⊢ IsLimit (F :=
      parallelPair (X := s.obj (firstObj R P)) (Y := s.obj (secondObj R P)) (s.map (firstMap R P))
        (s.map (secondMap R P)))
      (Fork.ofι (s.map (forkMap R P)) ⋯) ≃
    IsLimit (F :=
      parallelPair (Y := Equalizer.Presieve.SecondObj (P ⋙ s) R) (Equalizer.Presieve.firstMap (P ⋙ s) R)
        (Equalizer.Presieve.secondMap (P ⋙ s) R))
      (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯)

Tactic:
refine (IsLimit.postcomposeHomEquiv e _).symm.trans
    (IsLimit.equivIsoLimit (Fork.ext (Iso.refl _) ?_))

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, Equiv.trans, CategoryTheory.Iso.refl, CategoryTheory.Limits.IsLimit.equivIsoLimit, CategoryTheory.Limits.Fork.ext, Equiv.symm
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U_1 : C
R_1 : Presieve.{v₁, u₁} U_1
P_1 : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
inst_4 : HasProducts A
inst_5 : HasProducts A'
inst_6 : HasPullbacks.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : A ⥤ Type (max v₁ u₁)
inst_7 : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve.{v₁, u₁} U
e : parallelPair (X := s.obj (firstObj R P)) (Y := s.obj (secondObj R P)) (s.map (firstMap R P))
    (s.map (secondMap R P)) ≅
  parallelPair (Y := Equalizer.Presieve.SecondObj (P ⋙ s) R) (Equalizer.Presieve.firstMap (P ⋙ s) R)
    (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext
    (PreservesProduct.iso s fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
      P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f }))))
    (PreservesProduct.iso s fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
      P.obj
        (op
          (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
            (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
    ⋯ ⋯
dsimp :
  Eq (α := s.obj (P.obj (op U)) ⟶ Equalizer.FirstObj (P ⋙ s) R)
    (𝟙 (s.obj (P.obj (op U))) ≫
      Pi.lift (f := fun (f : (Y : C) × { f : Y ⟶ U // R f }) ↦
        s.obj (P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ U // R f }))))) fun (f : (Y : C) × { f : Y ⟶ U // R f }) ↦
        s.map (P.map (↑(f.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : f.fst ⟶ U).op))
    (CategoryStruct.comp (Y := s.obj (firstObj R P))
      (s.map
        (Pi.lift fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
          P.map (↑(f.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : f.fst ⟶ U).op))
      (piComparison s fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
        P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f })))))
⊢ Iso.hom (Iso.refl ((Cone.postcompose e.hom).obj (Fork.ofι (s.map (forkMap R P)) ⋯)).pt) ≫
      Fork.ι (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯) =
    Fork.ι ((Cone.postcompose e.hom).obj (Fork.ofι (s.map (forkMap R P)) ⋯))

Tactic:
dsimp [Equalizer.forkMap, forkMap, e, Fork.ι]

Premises used: CategoryTheory.Presheaf.forkMap, CategoryTheory.Equalizer.forkMap, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U_1 : C
R_1 : Presieve.{v₁, u₁} U_1
P_1 : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
inst_4 : HasProducts A
inst_5 : HasProducts A'
inst_6 : HasPullbacks.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : A ⥤ Type (max v₁ u₁)
inst_7 : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve.{v₁, u₁} U
e : parallelPair (X := s.obj (firstObj R P)) (Y := s.obj (secondObj R P)) (s.map (firstMap R P))
    (s.map (secondMap R P)) ≅
  parallelPair (Y := Equalizer.Presieve.SecondObj (P ⋙ s) R) (Equalizer.Presieve.firstMap (P ⋙ s) R)
    (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext
    (PreservesProduct.iso s fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
      P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f }))))
    (PreservesProduct.iso s fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
      P.obj
        (op
          (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
            (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
    ⋯ ⋯
⊢ Eq (α := s.obj (P.obj (op U)) ⟶ Equalizer.FirstObj (P ⋙ s) R)
    (𝟙 (s.obj (P.obj (op U))) ≫
      Pi.lift (f := fun (f : (Y : C) × { f : Y ⟶ U // R f }) ↦
        s.obj (P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ U // R f }))))) fun (f : (Y : C) × { f : Y ⟶ U // R f }) ↦
        s.map (P.map (↑(f.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : f.fst ⟶ U).op))
    (CategoryStruct.comp (Y := s.obj (firstObj R P))
      (s.map
        (Pi.lift fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
          P.map (↑(f.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : f.fst ⟶ U).op))
      (piComparison s fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
        P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f })))))

Tactic:
simp only [id_comp, map_lift_piComparison]

Premises used: CategoryTheory.Limits.map_lift_piComparison, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
mp : IsSheaf J P' → IsSheaf' J P'
mpr : IsSheaf' J P' → IsSheaf J P'
⊢ IsSheaf J P' ↔ IsSheaf' J P'

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf J P'
U : C
R : Presieve.{v₁, u₁} U
hR : generate R ∈ (J : (a : C) → Set (Sieve a)) U
⊢ Nonempty
    (IsLimit (F := parallelPair (X := firstObj R P') (Y := secondObj R P') (firstMap R P') (secondMap R P'))
      (Fork.ofι (forkMap R P') ⋯))

Tactic:
⟨?_⟩

Premises used: Nonempty.intro
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf J P'
U : C
R : Presieve.{v₁, u₁} U
hR : generate R ∈ (J : (a : C) → Set (Sieve a)) U
mp :
  IsLimit (F := parallelPair (X := firstObj R P') (Y := secondObj R P') (firstMap R P') (secondMap R P'))
    (Fork.ofι (forkMap R P') ⋯)
⊢ Nonempty
    (IsLimit (F := parallelPair (X := firstObj R P') (Y := secondObj R P') (firstMap R P') (secondMap R P'))
      (Fork.ofι (forkMap R P') ⋯))

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf J P'
U : C
R : Presieve.{v₁, u₁} U
hR : generate R ∈ (J : (a : C) → Set (Sieve a)) U
mp :
  (X : A'ᵒᵖ) →
    IsLimit (F :=
      parallelPair (X := firstObj R P') (Y := secondObj R P') (firstMap R P') (secondMap R P') ⋙ Functor.obj coyoneda X)
      (Functor.mapCone (Functor.obj coyoneda X) (Fork.ofι (forkMap R P') ⋯))
⊢ IsLimit (F := parallelPair (X := firstObj R P') (Y := secondObj R P') (firstMap R P') (secondMap R P'))
    (Fork.ofι (forkMap R P') ⋯)

Tactic:
apply coyonedaJointlyReflectsLimits

Premises used: CategoryTheory.coyonedaJointlyReflectsLimits
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf J P'
U : C
R : Presieve.{v₁, u₁} U
hR : generate R ∈ (J : (a : C) → Set (Sieve a)) U
X : A'ᵒᵖ
⊢ Presieve.IsSheafFor (P' ⋙ Functor.obj coyoneda X) (generate R).arrows

Tactic:
have q : Presieve.IsSheafFor (P' ⋙ coyoneda.obj X) _ := h X.unop _ hR
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf J P'
U : C
R : Presieve.{v₁, u₁} U
hR : generate R ∈ (J : (a : C) → Set (Sieve a)) U
X : A'ᵒᵖ
q : Presieve.IsSheafFor (P' ⋙ Functor.obj coyoneda X) (generate R).arrows
⊢ Presieve.IsSheafFor (P' ⋙ Functor.obj coyoneda X) R

Tactic:
rw [← Presieve.isSheafFor_iff_generate] at q

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A' : Type u₂
inst_1 : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology.{v₁, u₁} C
P' : Cᵒᵖ ⥤ A'
inst_2 : HasProducts A'
inst_3 : HasPullbacks.{v₁, u₁} C
h : IsSheaf J P'
U : C
R : Presieve.{v₁, u₁} U
hR : generate R ∈ (J : (a : C) → Set (Sieve a)) U
X : A'ᵒᵖ
q : Presieve.IsSheafFor (P' ⋙ Functor.obj coyoneda X) R
⊢ Nonempty
    (IsLimit (F :=
      parallelPair (Y := Equalizer.Presieve.SecondObj (P' ⋙ Functor.obj coyoneda X) R)
        (Equalizer.Presieve.firstMap (P' ⋙ Functor.obj coyoneda X) R)
        (Equalizer.Presieve.secondMap (P' ⋙ Functor.obj coyoneda X) R))
      (Fork.ofι (Equalizer.forkMap (P' ⋙ Functor.obj coyoneda X) R) ⋯))

Tactic:
rw [Equalizer.Presieve.sheaf_condition] at q

Premises used: CategoryTheory.Equalizer.Presieve.sheaf_condition