awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F_1 G_1 : Functor.{v, v', u, u'} Cᵒᵖ A
F G : Sheaf.{v, v', u, u'} J A
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
φ :
  Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A) (Functor.obj (J.overPullback A (unop X)) F)
    (Functor.obj (J.overPullback A (unop X)) G)
⊢ Eq (α :=
    Quiver.Hom (V := (Over.{v, u} (unop Z))ᵒᵖ ⥤ A)
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
        (Functor.obj (J.overPullback A (unop Z)) F))
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
        (Functor.obj (J.overPullback A (unop Z)) G)))
    (InducedCategory.Hom.hom
        (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾Functor.map (J.overMapPullback A (f ≫ g).unop))) φ) :
      Quiver.Hom (V := (Over.{v, u} (unop Z))ᵒᵖ ⥤ A)
        (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
          (Functor.obj (J.overPullback A (unop Z)) F))
        (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
          (Functor.obj (J.overPullback A (unop Z)) G)))
    (InducedCategory.Hom.hom
        (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (CategoryStruct.comp (Y :=
              Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
                (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G))
              (↾Functor.map (J.overMapPullback A f.unop) :
                Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
                    (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G) ⟶
                  Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
                    (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G))
              (↾Functor.map (J.overMapPullback A g.unop) :
                Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
                    (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G) ⟶
                  Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Z)) (J.over (unop Z)) A)
                    (Functor.obj (J.overPullback A (unop Z)) F) (Functor.obj (J.overPullback A (unop Z)) G))))
          φ) :
      Quiver.Hom (V := (Over.{v, u} (unop Z))ᵒᵖ ⥤ A)
        (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
          (Functor.obj (J.overPullback A (unop Z)) F))
        (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
          (Functor.obj (J.overPullback A (unop Z)) G)))

Tactic:
exact ConcreteCategory.congr_hom ((presheafHom F.1 G.1).map_comp f g) φ.1

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.presheafHom, CategoryTheory.Functor.map_comp, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
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 ⟶ G
X : Cᵒᵖ
⊢ Eq (α := (sheafHom F G).obj (P := Presheaf.IsSheaf J).obj X)
    ((↑(((sheafHomSectionsEquiv F G).symm : (a : F ⟶ G) → (↑(sheafHom F G).obj.sections : Type (max (max u v) v'))) φ) :
        (j : Cᵒᵖ) → (sheafHom F G).obj.obj j)
      X)
    (Functor.map (J.overPullback A (unop X)) φ)

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hp : IsSheaf J P
R : Presieve.{v, u} X
hr : generate R ∈ (J : (a : C) → Set (Sieve a)) X
⊢ IsSheafFor P R

Tactic:
(isSheafFor_iff_generate R).2 <| hp _ hr

Premises used: Iff.mpr, CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
J₁ J₂ : GrothendieckTopology.{v, u} C
⊢ J₁ ≤ J₂ → IsSheaf J₂ P → IsSheaf J₁ P

Tactic:
fun h t _ S hS => t S (h _ hS)

Premises used: CategoryTheory.Presieve.IsSheaf
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
J₁ J₂ : GrothendieckTopology.{v, u} C
⊢ J₁ ≤ J₂ → IsSeparated J₂ P → IsSeparated J₁ P

Tactic:
fun h hP _ S hS ↦ hP S <| h _ hS

Premises used: CategoryTheory.Presieve.IsSeparated
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
h : IsSheaf J P
⊢ IsSeparated J P

Tactic:
fun _ S hS => (h S hS).isSeparatedFor

Premises used: CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.Presieve.IsSeparated
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
h : IsSeparated J P
h' :
  ∀ (X : C),
    ∀ S ∈ (J : (a : C) → Set (Sieve a)) X,
      ∀ (x : FamilyOfElements P S.arrows),
        x.Compatible (R := S.arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := S.arrows) t
⊢ IsSheaf J P

Tactic:
fun _ S hS ↦ (h S hS).isSheafFor <| h' _ S hS

Premises used: CategoryTheory.Presieve.IsSheaf, CategoryTheory.Presieve.IsSeparatedFor.isSheafFor
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v, w', u, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      (((e : P₁.obj (op X) ≃ P₂.obj (op X)) : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          (((e : P₁.obj (op Y) ≃ P₂.obj (op Y)) : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
hP₁ : IsSheaf J P₁
⊢ IsSheaf J P₂

Tactic:
fun _ R hR ↦
  isSheafFor_of_nat_equiv e he (hP₁ R hR)

Premises used: CategoryTheory.Presieve.IsSheaf, CategoryTheory.Presieve.isSheafFor_of_nat_equiv
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v, w', u, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
⊢ IsSheaf J P₁ ↔ IsSheaf J P₂

Tactic:
simp only [Presieve.IsSheaf, Presieve.isSheafFor_iff_of_nat_equiv e he]

Premises used: CategoryTheory.Presieve.IsSheaf, CategoryTheory.Presieve.isSheafFor_iff_of_nat_equiv
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
J : GrothendieckTopology.{v, u} C
P' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
i : P ≅ P'
h : IsSheaf J P
⊢ IsSheaf J P'

Tactic:
fun _ S hS => isSheafFor_iso i (h S hS)

Premises used: CategoryTheory.Presieve.IsSheaf, CategoryTheory.Presieve.isSheafFor_iso
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
J : GrothendieckTopology.{v, u} C
P' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
i : P ≅ P'
hP : IsSeparated J P
⊢ IsSeparated J P'

Tactic:
fun _ S hS ↦ isSeparatedFor_iso i (hP S hS)

Premises used: CategoryTheory.Presieve.isSeparatedFor_iso, CategoryTheory.Presieve.IsSeparated
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
h : ∀ {X : C}, ∀ S ∈ (J : (a : C) → Set (Sieve a)) X, YonedaSheafCondition P S
⊢ IsSheaf J P

Tactic:
fun _ _ hS =>
  isSheafFor_iff_yonedaSheafCondition.2 (h _ hS)

Premises used: CategoryTheory.Presieve.IsSheaf, Iff.mpr, CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
mp : IsSheaf K.toGrothendieck P → ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
mpr : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) → IsSheaf K.toGrothendieck P
⊢ IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
PJ : IsSheaf K.toGrothendieck P
X : C
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
mp : IsSheafFor P (generate R).arrows
⊢ IsSheafFor P R

Tactic:
rw [isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
PJ : IsSheaf K.toGrothendieck P
X : C
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
⊢ IsSheafFor P (generate R).arrows

Tactic:
apply PJ (Sieve.generate R) ⟨_, hR, le_generate R⟩

Premises used: CategoryTheory.Sieve.le_generate, And.intro, Exists.intro, CategoryTheory.Sieve.generate
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
a a₁ a₂ a₃ : R ≤ S.arrows
⊢ generate R ≤ S

Tactic:
rwa [generate_le_iff]

Premises used: CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ (generate R).arrows ≤ S.arrows

Tactic:
have gRS : ⇑(generate R) ≤ S := by
      apply giGenerate.gc.monotone_u
      rwa [generate_le_iff]
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
apply : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f (generate R)).arrows
⊢ IsSheafFor P S.arrows

Tactic:
apply isSheafFor_subsieve P gRS _

Premises used: CategoryTheory.Presieve.isSheafFor_subsieve
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
rw : IsSheafFor P (pullbackArrows f R)
⊢ IsSheafFor P (Sieve.pullback f (generate R)).arrows

Tactic:
rw [← pullbackArrows_comm, ← isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate, CategoryTheory.Sieve.pullbackArrows_comm
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (pullbackArrows f R)

Tactic:
PK (pullbackArrows f R) (K.pullbacks f R hR)

Premises used: CategoryTheory.Presieve.pullbackArrows, CategoryTheory.Pretopology.pullbacks
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (pullbackArrows f R)

Tactic:
exact PK (pullbackArrows f R) (K.pullbacks f R hR)

Premises used: CategoryTheory.Presieve.pullbackArrows, CategoryTheory.Pretopology.pullbacks
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
⊢ ∀ S ∈ (⊥ : (a : C) → Set (Sieve a)) X, IsSheafFor P S.arrows

Tactic:
simp [isSheafFor_top]

Premises used: CategoryTheory.Presieve.isSheafFor_top
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v, u} X
⊢ IsSheafFor (P ⋙ uliftFunctor.{w', w}) R ↔ IsSheafFor P R

Tactic:
(isSheafFor_iff_of_nat_equiv (fun _ => Equiv.ulift.symm) (fun _ _ _ _ => rfl)).symm

Premises used: CategoryTheory.Presieve.isSheafFor_iff_of_nat_equiv, Iff.symm
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
J : GrothendieckTopology.{v, u} C
⊢ IsSheaf J (P ⋙ uliftFunctor.{w', w}) ↔ IsSheaf J P

Tactic:
(isSheaf_iff_of_nat_equiv (fun _ => Equiv.ulift.symm) (fun _ _ _ _ => rfl)).symm

Premises used: CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv, Iff.symm
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
J : GrothendieckTopology.{v, u} C
h rwa rwa₁ rwa₂ rwa₃ : IsSheaf J P
⊢ IsSheaf J (P ⋙ uliftFunctor.{w', w})

Tactic:
rwa [isSheaf_comp_uliftFunctor_iff]

Premises used: CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iff
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
J J₂ : GrothendieckTopology.{v, u} C
R : Presieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) R
hx : x.Compatible (R := R)
g₁ g₂ : R.category
F : g₁ ⟶ g₂
dsimp :
  Over.Hom.left F.hom ≫ x g₂.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ =
    x g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ ≫ 𝟙 W
⊢ R.diagram.map F ≫ x g₂.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ =
    x g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ ≫ Functor.map (Functor.obj (Functor.const R.category) W) F

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
J J₂ : GrothendieckTopology.{v, u} C
R : Presieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) R
hx : x.Compatible (R := R)
g₁ g₂ : R.category
F : g₁ ⟶ g₂
rw :
  Over.Hom.left F.hom ≫ x g₂.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ =
    𝟙 (unop (op g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).left)) ≫
      x g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯
⊢ Over.Hom.left F.hom ≫ x g₂.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ =
    x g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ ≫ 𝟙 W

Tactic:
rw [comp_id, ← id_comp (x g₁.obj.hom g₁.property)]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Category.comp_id, CategoryTheory.Over.hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
J J₂ : GrothendieckTopology.{v, u} C
R : Presieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) R
hx : x.Compatible (R := R)
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ F.hom.1 ≫ g₂.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom =
    𝟙 (unop (op g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).left)) ≫
      g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
J J₂ : GrothendieckTopology.{v, u} C
R : Presieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) R
hx : x.Compatible (R := R)
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ Over.Hom.left F.hom ≫ x g₂.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ =
    𝟙 (unop (op g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).left)) ≫
      x g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯

Tactic:
exact hx _ _ _ _ (by simp)
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f

Tactic:
have Hs := s.ι.naturality
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
simp :
  Eq (α := Z ⟶ s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (g : Y₁ ⟶ s.pt) ↦ g₁ ≫ g) : (a : Y₁ ⟶ s.pt) → Z ⟶ s.pt)
        (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁) :
      Z ⟶ s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (g : Y₂ ⟶ s.pt) ↦ g₂ ≫ g) : (a : Y₂ ⟶ s.pt) → Z ⟶ s.pt)
        (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂) :
      Z ⟶ s.pt)
⊢ Eq (α := (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj yoneda s.pt) (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda s.pt) g₁.op) :
          (a : (fun (X : Type v) ↦ X) ((yoneda.obj s.pt).obj (op Y₁))) →
            (fun (X : Type v) ↦ X) ((yoneda.obj s.pt).obj (op Z)))
        (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁) :
      (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj yoneda s.pt) (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda s.pt) g₂.op) :
          (a : (fun (X : Type v) ↦ X) ((yoneda.obj s.pt).obj (op Y₂))) →
            (fun (X : Type v) ↦ X) ((yoneda.obj s.pt).obj (op Z)))
        (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂) :
      (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj yoneda s.pt) (op Z)))

Tactic:
simp only [yoneda_obj_obj, Opposite.unop_op, yoneda_obj_map, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.yoneda_obj_obj, CategoryTheory.yoneda_obj_map, Opposite.unop_op
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
dsimp :
  Eq (α := Z ⟶ s.pt)
    (g₁ ≫ s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
    (g₂ ≫ s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₂) hf₂))
⊢ Eq (α := Z ⟶ s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (g : Y₁ ⟶ s.pt) ↦ g₁ ≫ g) : (a : Y₁ ⟶ s.pt) → Z ⟶ s.pt)
        (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁) :
      Z ⟶ s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (g : Y₂ ⟶ s.pt) ↦ g₂ ≫ g) : (a : Y₂ ⟶ s.pt) → Z ⟶ s.pt)
        (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂) :
      Z ⟶ s.pt)

Tactic:
dsimp [yonedaFamilyOfElements_fromCocone]

Premises used: CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
⊢ S.arrows (g₁ ≫ f₁)

Tactic:
Sieve.downward_closed S hf₁ g₁

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
⊢ S.arrows (g₁ ≫ f₁)

Tactic:
exact Sieve.downward_closed S hf₁ g₁

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
⊢ S.arrows (g₁ ≫ f₁)

Tactic:
have hgf₁ : S.arrows (g₁ ≫ f₁) := by exact Sieve.downward_closed S hf₁ g₁
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
hgf₁ : S.arrows (g₁ ≫ f₁)
⊢ S.arrows (g₂ ≫ f₂)

Tactic:
Sieve.downward_closed S hf₂ g₂

Premises used: CategoryTheory.Sieve.downward_closed