awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
⊢ y₁ = y₂
have hunique : y₁.app = y₂.app
Tactic: apply NatTrans.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
⊢ y₁.app = y₂.app
have hunique : ∀ (Y : Over.{v, u} X),
  Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
    (y₁.app (op Y)) (y₂.app (op Y))
Tactic: ext ⟨Y : Over X⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
    (y₁.app (op Y)) (y₂.app (op Y))
have hunique : ∀ (j : (Sieve.pullback Y.hom S).arrows.categoryᵒᵖ),
  y₁.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app j =
    y₂.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app j
Tactic: apply (hG Y.hom).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
Z : Over.{v, u} Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶
      ((Sieve.pullback Y.hom S).arrows.diagram.op ⋙ G).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y.left) ↦ (Sieve.pullback Y.hom S).arrows f.hom)
            Z hZ)))
    (y₁.app (op Y) ≫
      (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y.left) ↦ (Sieve.pullback Y.hom S).arrows f.hom)
            Z hZ)))
    (y₂.app (op Y) ≫
      (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y.left) ↦ (Sieve.pullback Y.hom S).arrows f.hom)
            Z hZ)))
have hunique : y₁.app (op Y) ≫ G.map Z.hom.op = y₂.app (op Y) ≫ G.map Z.hom.op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
Z : Over.{v, u} Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
⊢ y₁.app (op Y) ≫ G.map Z.hom.op = y₂.app (op Y) ≫ G.map Z.hom.op
have hunique : (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₁.app (op (Over.mk (Z.hom ≫ Y.hom))) =
  (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
Tactic: refine (y₁.naturality φ.op).symm.trans (Eq.trans ?_ (y₂.naturality φ.op))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
Z : Over.{v, u} Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
⊢ (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₁.app (op (Over.mk (Z.hom ≫ Y.hom))) =
    (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
have hunique : (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ (x (Z.hom ≫ Y.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
  (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
Tactic: rw [(hy₁ _ _ hZ), ← ((hy₂ _ _ hZ))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
Z : Over.{v, u} Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
hunique :
  (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ (x (Z.hom ≫ Y.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
    (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
⊢ (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₁.app (op (Over.mk (Z.hom ≫ Y.hom))) =
    (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
have hunique₁ : (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom))) =
  (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
Tactic: rw [(hy₁ _ _ hZ), ← ((hy₂ _ _ hZ))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
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 : Functor.{v, v', u, u'} Cᵒᵖ A
hG : IsSheaf J G
⊢ IsSheaf J (presheafHom F G)
have rw : Presieve.IsSheaf J (presheafHom F G)
Tactic: rw [isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
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 : Cᵒᵖ
⊢ Eq (α :=
    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 X)) (J.over (unop X)) A)
        (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G))
    (↾Functor.map (J.overMapPullback A (Quiver.Hom.unop (𝟙 X))) :
      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 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 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 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 X)) (J.over (unop X)) A)
          (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G))
have h : ∀
  (φ :
    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)),
  InducedCategory.Hom.hom
      (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (↾Functor.map (J.overMapPullback A (Quiver.Hom.unop (𝟙 X)))))
        φ) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (𝟙
              (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)))).toFun
        φ).hom
Tactic: ext φ : 4
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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
⊢ IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
have mp : IsSheaf K.toGrothendieck P → ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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
⊢ IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
have mpr : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) → IsSheaf K.toGrothendieck P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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 R
have mp : IsSheafFor P (generate R).arrows
Tactic: rw [isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
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
⊢ IsSheafFor P S.arrows
have gRS : (generate R).arrows ≤ S.arrows
Tactic: have gRS : ⇑(generate R) ≤ S := by
      apply giGenerate.gc.monotone_u
      rwa [generate_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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
⊢ IsSheafFor P S.arrows
have apply : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f (generate R)).arrows
Tactic: apply isSheafFor_subsieve P gRS _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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 (Sieve.pullback f (generate R)).arrows
have rw : IsSheafFor P (pullbackArrows f R)
Tactic: rw [← pullbackArrows_comm, ← isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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₂
⊢ 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
have dsimp : Over.Hom.left F.hom ≫ x g₂.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom sorry =
  x g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom sorry ≫ 𝟙 W
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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 ⋯ =
    x g₁.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom ⋯ ≫ 𝟙 W
have rw : Over.Hom.left F.hom ≫ x g₂.obj (P := fun (f : Over.{v, u} X) ↦ R f.hom).hom sorry =
  𝟙 (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 sorry
Tactic: rw [comp_id, ← id_comp (x g₁.obj.hom g₁.property)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
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₂
⊢ 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)))
have 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
Tactic: have Hs := s.ι.naturality
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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
⊢ 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)))
have 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)
Tactic: simp only [yoneda_obj_obj, Opposite.unop_op, yoneda_obj_map, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (goal)
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
⊢ 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)
have 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₂))
Tactic: dsimp [yonedaFamilyOfElements_fromCocone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
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
⊢ 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₂))
have hgf₁ : S.arrows (g₁ ≫ f₁)
Tactic: have hgf₁ : S.arrows (g₁ ≫ f₁) := by exact Sieve.downward_closed S hf₁ g₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
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₁)
⊢ 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₂))
have hgf₂ : S.arrows (g₂ ≫ f₂)
Tactic: have hgf₂ : S.arrows (g₂ ≫ f₂) := by exact Sieve.downward_closed S hf₂ g₂