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
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (SieveCompatible.cone (E := op E) (x :=
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows))
      ⋯ ⟶
    P.mapCone S.arrows.cocone.op) ≃
  { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      t } :=
  homEquivAmalgamation ⋯
⊢ IsAmalgamation.{v₂, v₁, u₁} (P := P ⋙ Functor.obj coyoneda (op E)) (R := S.arrows)
    (↑((eqv :
            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
          π) :
      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
    (↑((eqv' :
            (a : ⋯.cone ⟶ P.mapCone S.arrows.cocone.op) →
              { t : (P ⋙ coyoneda.obj (op E)).obj (op X) //
                (↑((eqv :
                            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                          π) :
                      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows).IsAmalgamation
                  t })
          f₁) :
      (P ⋙ coyoneda.obj (op E)).obj (op X))

Tactic:
exact (eqv' _).2

Premises used: DFunLike.coe, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (SieveCompatible.cone (E := op E) (x :=
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows))
      ⋯ ⟶
    P.mapCone S.arrows.cocone.op) ≃
  { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      t } :=
  homEquivAmalgamation ⋯
⊢ IsAmalgamation.{v₂, v₁, u₁} (P := P ⋙ Functor.obj coyoneda (op E)) (R := S.arrows)
    (↑((eqv :
            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
          π) :
      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
    (↑((eqv' :
            (a : ⋯.cone ⟶ P.mapCone S.arrows.cocone.op) →
              { t : (P ⋙ coyoneda.obj (op E)).obj (op X) //
                (↑((eqv :
                            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                          π) :
                      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows).IsAmalgamation
                  t })
          f₂) :
      (P ⋙ coyoneda.obj (op E)).obj (op X))

Tactic:
(eqv' _).2

Premises used: DFunLike.coe, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (SieveCompatible.cone (E := op E) (x :=
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows))
      ⋯ ⟶
    P.mapCone S.arrows.cocone.op) ≃
  { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      t } :=
  homEquivAmalgamation ⋯
⊢ IsAmalgamation.{v₂, v₁, u₁} (P := P ⋙ Functor.obj coyoneda (op E)) (R := S.arrows)
    (↑((eqv :
            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
          π) :
      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
    (↑((eqv' :
            (a : ⋯.cone ⟶ P.mapCone S.arrows.cocone.op) →
              { t : (P ⋙ coyoneda.obj (op E)).obj (op X) //
                (↑((eqv :
                            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                          π) :
                      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows).IsAmalgamation
                  t })
          f₂) :
      (P ⋙ coyoneda.obj (op E)).obj (op X))

Tactic:
exact (eqv' _).2

Premises used: DFunLike.coe, Subtype.property
-- 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
⊢ IsSheaf J P ↔ ∀ ⦃X : C⦄, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))

Tactic:
⟨fun h _ S hS => (isLimit_iff_isSheafFor P S).2 fun E => h E.unop S hS, fun h E _ S hS =>
    (isLimit_iff_isSheafFor P S).1 (h S hS) (op E)⟩

Premises used: Iff.mpr, Opposite.op, Iff.intro, Iff.mp, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, Opposite.unop
-- 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
⊢ (∀ (E : A), Presieve.IsSeparated.{v₂, v₁, u₁} J (P ⋙ Functor.obj coyoneda (op E))) ↔
    ∀ ⦃X : C⦄,
      ∀ S ∈ (J : (a : C) → Set (Sieve a)) X,
        ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)

Tactic:
⟨fun h _ S hS => (subsingleton_iff_isSeparatedFor P S).2 fun E => h E.unop S hS, fun h E _ S hS =>
    (subsingleton_iff_isSeparatedFor P S).1 (h S hS) (op E)⟩

Premises used: Iff.mpr, Opposite.op, Iff.intro, Iff.mp, Opposite.unop, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
R : Presieve.{v₁, u₁} X
⊢ Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), IsSheafFor (P ⋙ Functor.obj coyoneda E) R

Tactic:
(isLimit_iff_isSheafFor P _).trans (forall_congr' fun _ => (isSheafFor_iff_generate _).symm)

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate, forall_congr', Iff.trans, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, Iff.symm
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : HasPullbacks.{v₁, u₁} C
K : Pretopology.{v₁, u₁} C
simp_rw :
  (∀ (E : A) {X : C}, ∀ R ∈ K.coverings X, IsSheafFor (P ⋙ Functor.obj coyoneda (op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))
⊢ (∀ (E : A), Presieve.IsSheaf.{v₂, v₁, u₁} K.toGrothendieck (P ⋙ Functor.obj coyoneda (op E))) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
simp_rw [isSheaf_pretopology]

Premises used: CategoryTheory.Presieve.isSheaf_pretopology
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : HasPullbacks.{v₁, u₁} C
K : Pretopology.{v₁, u₁} C
⊢ (∀ (E : A) {X : C}, ∀ R ∈ K.coverings X, IsSheafFor (P ⋙ Functor.obj coyoneda (op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
⟨fun h X R hR => (isLimit_iff_isSheafFor_presieve P R).2 fun E => h E.unop R hR,
      fun h E X R hR => (isLimit_iff_isSheafFor_presieve P R).1 (h R hR) (op E)⟩

Premises used: Iff.mpr, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, Opposite.op, Iff.intro, Iff.mp, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : HasPullbacks.{v₁, u₁} C
K : Pretopology.{v₁, u₁} C
⊢ (∀ (E : A) {X : C}, ∀ R ∈ K.coverings X, IsSheafFor (P ⋙ Functor.obj coyoneda (op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
exact
    ⟨fun h X R hR => (isLimit_iff_isSheafFor_presieve P R).2 fun E => h E.unop R hR,
      fun h E X R hR => (isLimit_iff_isSheafFor_presieve P R).1 (h R hR) (op E)⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
E : A
X : C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : IsSheaf J P
S : J.Cover X
x : (I : S.Arrow) → E ⟶ P.obj (op I.Y)
hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), x I₁ ≫ P.map r.g₁.op = x I₂ ≫ P.map r.g₂.op
I : S.Arrow
⊢ hP.amalgamate S x hx ≫ P.map I.f.op = x I

Tactic:
apply (hP _ _ S.condition).valid_glue

Premises used: CategoryTheory.GrothendieckTopology.Cover.condition, CategoryTheory.Presieve.IsSheafFor.valid_glue
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
E : A
X : C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : IsSheaf J P
S : J.Cover X
e₁ e₂ : E ⟶ P.obj (op X)
h : ∀ (I : S.Arrow), e₁ ≫ P.map I.f.op = e₂ ≫ P.map I.f.op
⊢ e₁ = e₂

Tactic:
(hP _ _ S.condition).isSeparatedFor.ext fun Y f hf => h ⟨Y, f, hf⟩

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.GrothendieckTopology.Cover.condition, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk
-- 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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
h₁ :
  ∀
    (I_1 :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S_1 : Sieve.{v₁, u₁} S) ↦ S_1 ∈ (J : (a : C) → Set (Sieve a)) S) (ofArrows X f) hf)),
    x ≫ P.map I_1.f.op = y ≫ P.map I_1.f.op
⊢ x = y

Tactic:
apply hP.hom_ext ⟨_, hf⟩

Premises used: Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
h₁ : Eq (α := E ⟶ P.obj (op Z)) (x ≫ P.map ((f i).op ≫ g.op)) (y ≫ P.map ((f i).op ≫ g.op))
⊢ Eq (α :=
    E ⟶
      P.obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J) (S :=
            Subtype.mk (p := fun (S_1 : Sieve.{v₁, u₁} S) ↦ S_1 ∈ (J : (a : C) → Set (Sieve a)) S) (ofArrows X f) hf)
            { Y := Z, f := g ≫ f i, hf := ⋯ })))
    (x ≫ P.map (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z, f := g ≫ f i, hf := ⋯ })))
    (y ≫ P.map (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z, f := g ≫ f i, hf := ⋯ })))

Tactic:
dsimp
-- 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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
h₁ : x ≫ P.map (f i).op ≫ P.map g.op = y ≫ P.map (f i).op ≫ P.map g.op
h₂ h₃ : y ≫ P.map (f i).op ≫ P.map g.op = y ≫ P.map (f i).op ≫ P.map g.op
⊢ Eq (α := E ⟶ P.obj (op Z)) (x ≫ P.map ((f i).op ≫ g.op)) (y ≫ P.map ((f i).op ≫ g.op))

Tactic:
rw [P.map_comp, reassoc_of% (h i)]

Premises used: CategoryTheory.Functor.map_comp
-- 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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x : (i : I) → E ⟶ P.obj (op (X i))
hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j), a ≫ f i = b ≫ f j → x i ≫ P.map a.op = x j ≫ P.map b.op
⊢ ∃! g : E ⟶ P.obj (op S), ∀ (i : I), g ≫ P.map (f i).op = x i

Tactic:
(Presieve.isSheafFor_arrows_iff _ _).1
    ((Presieve.isSheafFor_iff_generate _).2 (hP E _ hf)) x (fun _ _ _ _ _ w => hx _ _ w)

Premises used: Iff.mpr, CategoryTheory.Presieve.isSheafFor_arrows_iff, CategoryTheory.Presieve.isSheafFor_iff_generate, Iff.mp
-- 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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x : (i : I) → E ⟶ P.obj (op (X i))
hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j), a ≫ f i = b ≫ f j → x i ≫ P.map a.op = x j ≫ P.map b.op
i : I
⊢ hP.amalgamateOfArrows f hf x hx ≫ P.map (f i).op = x i

Tactic:
(hP.existsUnique_amalgamation_ofArrows f hf x hx).choose_spec.1 i

Premises used: Exists.choose_spec, CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows, CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows, And.left
-- 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 P' : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
e : P ≅ P'
⊢ IsSheaf J P ↔ IsSheaf J P'

Tactic:
forall_congr' fun _ =>
    ⟨Presieve.isSheaf_iso J (Functor.isoWhiskerRight e _),
      Presieve.isSheaf_iso J (Functor.isoWhiskerRight e.symm _)⟩

Premises used: CategoryTheory.coyoneda, CategoryTheory.Presieve.isSheaf_iso, Opposite.op, Iff.intro, CategoryTheory.Iso.symm, forall_congr', CategoryTheory.Presheaf.IsSheaf, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.obj
-- 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
X : A
hX : IsTerminal.{v₂, u₂} X
⊢ IsSheaf.{v₁, v₂, u₁, u₂} J (Functor.obj (Functor.const Cᵒᵖ) X)

Tactic:
fun _ _ _ _ _ _ =>
  ⟨hX.from _, fun _ _ _ => hX.hom_ext _ _, fun _ _ => hX.hom_ext _ _⟩

Premises used: CategoryTheory.Presieve.IsSheaf, CategoryTheory.Limits.IsTerminal.from, Opposite, CategoryTheory.coyoneda, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Presieve.IsSheafFor, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, Opposite.op, ExistsUnique, And.intro, Exists.intro, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Functor.const, CategoryTheory.Presheaf.IsSheaf, DFunLike.coe, Opposite.unop, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ Presheaf.IsSheaf J (F.obj (P := Presheaf.IsSheaf J))

Tactic:
F.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
X Y : Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ Eq (α :=
    (Functor.obj
            (sheafToPresheaf J A ⋙
              yoneda ⋙
                Functor.obj
                  (Functor.whiskeringLeft (Sheaf.{v₁, v₂, u₁, u₂} J A)ᵒᵖ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A)ᵒᵖ
                    (Type (max u₁ v₂)))
                  (Functor.op (sheafToPresheaf J A)))
            X).obj
        (op Y) ≅
      Functor.obj (Functor.obj yoneda X) (op Y))
    ((Iso.app sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf X).app (op Y))
    (Equiv.toIso (Equiv.symm Sheaf.homEquiv))

Tactic:
rfl

Premises used: TypeCat.Fun.comp, Equiv.toIso, CategoryTheory.ObjectProperty.homMk, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
X Y : Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ (Iso.app sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf (op X)).app Y =
    Equiv.toIso (Equiv.symm Sheaf.homEquiv)

Tactic:
rfl

Premises used: TypeCat.Fun.comp, Equiv.toIso, CategoryTheory.ObjectProperty.homMk, CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F G : Sheaf.{v₁, v₂, u₁, u₂} J A
f : F ⟶ G
h : Mono f.hom
⊢ Mono f

Tactic:
(sheafToPresheaf J A).mono_of_mono_map h

Premises used: CategoryTheory.Functor.mono_of_mono_map, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F G : Sheaf.{v₁, v₂, u₁, u₂} J A
f : F ⟶ G
h : Epi f.hom
⊢ Epi f

Tactic:
(sheafToPresheaf J A).epi_of_epi_map h

Premises used: CategoryTheory.Functor.epi_of_epi_map, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
mp : Presheaf.IsSheaf J P → Presieve.IsSheaf J P
mpr : Presieve.IsSheaf J P → Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J P ↔ Presieve.IsSheaf J P

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presheaf.IsSheaf J P
⊢ Presieve.IsSheaf J P

Tactic:
Presieve.isSheaf_iso J ?_ (hP (PUnit))

Premises used: CategoryTheory.Presieve.isSheaf_iso, PUnit
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presheaf.IsSheaf J P
mp : P ⋙ Functor.obj coyoneda (op PUnit.{w + 1}) ≅ P
⊢ Presieve.IsSheaf J P

Tactic:
refine Presieve.isSheaf_iso J ?_ (hP (PUnit))

Premises used: CategoryTheory.Presieve.isSheaf_iso, PUnit
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presheaf.IsSheaf J P
⊢ P ⋙ Functor.obj coyoneda (op PUnit.{w + 1}) ≅ P

Tactic:
exact Functor.isoWhiskerLeft _ Coyoneda.punitIso ≪≫ P.rightUnitor

Premises used: CategoryTheory.Coyoneda.punitIso, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.isoWhiskerLeft
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y), z.IsAmalgamation (R := S.arrows) t

Tactic:
⟨↾fun x => (hP S hS).amalgamate (fun Z f hf ↦
      (ConcreteCategory.hom (z f hf)) x) ?_, ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, TypeCat.ofHom, CategoryTheory.Presieve.IsSheafFor.amalgamate, ExistsUnique, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
mpr :
  ∀ (x : unop (op X)),
    Presieve.FamilyOfElements.Compatible.{w, v₁, u₁} (P := P) (R := S.arrows)
      fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x
mpr₁ :
  (fun (t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)) ↦ z.IsAmalgamation (R := S.arrows) t)
    (↾fun (x : unop (op X)) ↦
      ⋯.amalgamate (R := S.arrows)
        (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
        ⋯)
mpr₂ :
  ∀ (y : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)),
    (fun (t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)) ↦ z.IsAmalgamation (R := S.arrows) t) y →
      y =
        ↾fun (x : unop (op X)) ↦
          ⋯.amalgamate (R := S.arrows)
            (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
            ⋯
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y), z.IsAmalgamation (R := S.arrows) t

Tactic:
refine ⟨↾fun x => (hP S hS).amalgamate (fun Z f hf ↦
      (ConcreteCategory.hom (z f hf)) x) ?_, ?_, ?_⟩