awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
⊢ Eq (α := P.obj X ⟶ F.obj (R.obj X))
    (NatTrans.app
        ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F)
          (whiskerRight f G ≫ g))
        X :
      P.obj X ⟶ (R ⋙ F).obj X)
    (f.app X ≫
      NatTrans.app ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g) X)
have h : Eq (α := P.obj X ⟶ F.obj (R.obj X))
  (NatTrans.app
      ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F) (whiskerRight f G ≫ g))
      X :
    P.obj X ⟶ (R ⋙ F).obj X)
  (NatTrans.app (f ≫ (Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g) X)
Tactic: rw [← NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
⊢ Eq (α := P.obj X ⟶ F.obj (R.obj X))
    (NatTrans.app
        ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F)
          (whiskerRight f G ≫ g))
        X :
      P.obj X ⟶ (R ⋙ F).obj X)
    (NatTrans.app (f ≫ (Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g) X)
have h : Eq (α := NatTrans P (R ⋙ F))
  ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F) (whiskerRight f G ≫ g) :
    P ⟶ R ⋙ F)
  (f ≫ (Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g : P ⟶ R ⋙ F)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f ⊤).arrows
have rw : Presieve.IsSheafFor (X := Y) P (arrows ⊤)
Tactic: rw [Sieve.pullback_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSheafFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
have rw : Presieve.IsSheafFor P (Sieve.pullback (g ≫ f) S).arrows
Tactic: rw [← pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback g R).arrows
have refine_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z⦄,
  (Sieve.pullback g R).arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows
Tactic: refine Presieve.isSheafFor_trans P (pullback g S) _ (hS Z g) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
refine_1 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z⦄,
    (Sieve.pullback g R).arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback g R).arrows
have refine_2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z⦄,
  (Sieve.pullback g S).arrows f → Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
Tactic: refine Presieve.isSheafFor_trans P (pullback g S) _ (hS Z g) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
h : (Sieve.pullback g R).arrows f
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows
have refine_1 : Presieve.IsSeparatedFor P (Sieve.pullback (f ≫ g) S).arrows
Tactic: rw [← pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
have this : Presieve.IsSheafFor P (Sieve.pullback (𝟙 Y) (Sieve.pullback (f ≫ g) R)).arrows
Tactic: have := hR hf _ (𝟙 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presieve.IsSheaf (canonicalTopology C) P
have rw : Presieve.IsSheaf (canonicalTopology C) (P ⋙ uliftFunctor.{v, w})
Tactic: rw [← Presieve.isSheaf_comp_uliftFunctor_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presieve.IsSheaf (canonicalTopology C) (P ⋙ uliftFunctor.{v, w})
have refine : Presieve.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)
Tactic: refine Presieve.isSheaf_iso (canonicalTopology C) (P ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presieve.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)
have rw : Presheaf.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)
Tactic: rw [← isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presheaf.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)
have refine : Presheaf.IsSheaf.{v, v, u, v + 1} (canonicalTopology C) (Functor.obj yoneda (P ⋙ uliftFunctor.{v, w}).reprX)
Tactic: refine GrothendieckTopology.HasSheafCompose.isSheaf _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presheaf.IsSheaf.{v, v, u, v + 1} (canonicalTopology C) (Functor.obj yoneda (P ⋙ uliftFunctor.{v, w}).reprX)
have rw : Presieve.IsSheaf.{v, v, u} (canonicalTopology C) (Functor.obj yoneda (P ⋙ uliftFunctor.{v, w}).reprX)
Tactic: rw [isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Canonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J_1 J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : C
⊢ Presheaf.IsSheaf J (Functor.obj CategoryTheory.yoneda X)
have rw : Presieve.IsSheaf J (Functor.obj CategoryTheory.yoneda X)
Tactic: rw [isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CartesianMonoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
X Y : Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ Presheaf.IsSheaf J
    (tensorObj (𝒞 := Functor.category) (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))
have apply : IsLimit
  ((Cone.postcompose (pairComp X Y (sheafToPresheaf J A)).inv).obj
    (BinaryFan.mk (P :=
      tensorObj (𝒞 := Functor.category) (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))
      (fst (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))
      (snd (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))))
Tactic: apply isSheaf_of_isLimit (E := (Cone.postcompose (pairComp X Y (sheafToPresheaf J A)).inv).obj
    (BinaryFan.mk (fst X.obj Y.obj) (snd _ _)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CartesianMonoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
⊢ Presheaf.IsSheaf.{v₁, v₂, u₁, u₂} (A := A) J ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A)) (𝒞 := Functor.category))
have apply : IsLimit (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (F := Functor.empty (Sheaf.{v₁, v₂, u₁, u₂} J A) ⋙ sheafToPresheaf J A)
  (Functor.obj
    (Cone.postcompose
      (Iso.inv (Functor.uniqueFromEmpty (Functor.empty (Sheaf.{v₁, v₂, u₁, u₂} J A) ⋙ sheafToPresheaf J A))))
    (asEmptyCone ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A)) (𝒞 := Functor.category))))
Tactic: apply isSheaf_of_isLimit (E := (Cone.postcompose (Functor.uniqueFromEmpty _).inv).obj
    (asEmptyCone (𝟙_ _)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CartesianMonoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
apply :
  IsLimit (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (F := Functor.empty (Sheaf.{v₁, v₂, u₁, u₂} J A) ⋙ sheafToPresheaf J A)
    (Functor.obj
      (Cone.postcompose
        (Iso.inv (Functor.uniqueFromEmpty (Functor.empty (Sheaf.{v₁, v₂, u₁, u₂} J A) ⋙ sheafToPresheaf J A))))
      (asEmptyCone ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A)) (𝒞 := Functor.category))))
⊢ Presheaf.IsSheaf.{v₁, v₂, u₁, u₂} (A := A) J ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A)) (𝒞 := Functor.category))
have apply₁ : Discrete PEmpty.{1} ⥤ Sheaf.{v₁, v₂, u₁, u₂} J A
Tactic: apply isSheaf_of_isLimit (E := (Cone.postcompose (Functor.uniqueFromEmpty _).inv).obj
    (asEmptyCone (𝟙_ _)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X Y : C
f : Y ⟶ X
S : Sieve.{v, u} X
hS : J₁.IsClosed S
Z : C
g : Z ⟶ Y
hg : J₁.Covers (Sieve.pullback f S) g
⊢ J₁.Covers S (g ≫ f)
have rwa : Sieve.pullback (g ≫ f) S ∈ (J₁ : (a : C) → Set (Sieve a)) Z
Tactic: rwa [J₁.covers_iff, Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X Y : C
f : Y ⟶ X
S : Sieve.{v, u} X
hS : J₁.IsClosed S
Z : C
g : Z ⟶ Y
hg : J₁.Covers (Sieve.pullback f S) g
rwa : Sieve.pullback (g ≫ f) S ∈ (J₁ : (a : C) → Set (Sieve a)) Z
⊢ J₁.Covers S (g ≫ f)
have rwa₁ : Sieve.pullback g (Sieve.pullback f S) ∈ (J₁ : (a : C) → Set (Sieve a)) Z
Tactic: rwa [J₁.covers_iff, Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X Y : C
f : Y ⟶ X
S : Sieve.{v, u} X
⊢ J₁.close (Sieve.pullback f S) = Sieve.pullback f (J₁.close S)
have a : J₁.close (Sieve.pullback f S) ≤ Sieve.pullback f (J₁.close S)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X Y : C
f : Y ⟶ X
S : Sieve.{v, u} X
a : J₁.close (Sieve.pullback f S) ≤ Sieve.pullback f (J₁.close S)
⊢ J₁.close (Sieve.pullback f S) = Sieve.pullback f (J₁.close S)
have a₁ : Sieve.pullback f (J₁.close S) ≤ J₁.close (Sieve.pullback f S)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X Y : C
f : Y ⟶ X
S : Sieve.{v, u} X
⊢ J₁.close (Sieve.pullback f S) ≤ Sieve.pullback f (J₁.close S)
have a : J₁.IsClosed (Sieve.pullback f (J₁.close S))
Tactic: refine J₁.le_close_of_isClosed (Sieve.pullback_monotone _ (J₁.le_close S)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X Y : C
f : Y ⟶ X
S : Sieve.{v, u} X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ Sieve.pullback g (Sieve.pullback f S) ∈ (J₁ : (a : C) → Set (Sieve a)) Z
have a : Sieve.pullback (g ≫ f) S ∈ (J₁ : (a : C) → Set (Sieve a)) Z
Tactic: rw [← Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
⊢ J₁.close S = ⊤ ↔ S ∈ (J₁ : (a : C) → Set (Sieve a)) X
have mp : J₁.close S = ⊤ → S ∈ (J₁ : (a : C) → Set (Sieve a)) X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
mp : J₁.close S = ⊤ → S ∈ (J₁ : (a : C) → Set (Sieve a)) X
⊢ J₁.close S = ⊤ ↔ S ∈ (J₁ : (a : C) → Set (Sieve a)) X
have mpr : S ∈ (J₁ : (a : C) → Set (Sieve a)) X → J₁.close S = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
h : J₁.close S = ⊤
⊢ S ∈ (J₁ : (a : C) → Set (Sieve a)) X
have mp : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, Sieve.arrows ⊤ f → Sieve.pullback f S ∈ (J₁ : (a : C) → Set (Sieve a)) Y
Tactic: apply J₁.transitive (J₁.top_mem X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
⊢ J₁.close S = ⊤
have mpr : ⊤ ≤ J₁.close S
Tactic: rw [_root_.eq_top_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor (Functor.closedSieves J₁).toFunctor S.arrows
have rw : Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows ∧
  ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows),
    x.Compatible (R := S.arrows) →
      ∃ (t : (Functor.closedSieves J₁).toFunctor.obj (Opposite.op X)), x.IsAmalgamation (R := S.arrows) t
Tactic: rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows),
      x.Compatible (R := S.arrows) →
        ∃ (t : (Functor.closedSieves J₁).toFunctor.obj (Opposite.op X)), x.IsAmalgamation (R := S.arrows) t
have refine_1 : Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
refine_1 : Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows),
      x.Compatible (R := S.arrows) →
        ∃ (t : (Functor.closedSieves J₁).toFunctor.obj (Opposite.op X)), x.IsAmalgamation (R := S.arrows) t
have refine_2 : ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows),
  x.Compatible (R := S.arrows) →
    ∃ (t : (Functor.closedSieves J₁).toFunctor.obj (Opposite.op X)), x.IsAmalgamation (R := S.arrows) t
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve.{v, u} X
hM :
  Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
    ((Functor.closedSieves J₁).obj (Opposite.op X)) M
N : Sieve.{v, u} X
hN :
  Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
    ((Functor.closedSieves J₁).obj (Opposite.op X)) N
hM₂ :
  x.IsAmalgamation (R := S.arrows)
    (Subtype.mk (p := fun (x : Functor.obj (Functor.sieves C) (Opposite.op X)) ↦
      Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
        ((Functor.closedSieves J₁).obj (Opposite.op X)) x)
      M hM)
hN₂ :
  x.IsAmalgamation (R := S.arrows)
    (Subtype.mk (p := fun (x : Functor.obj (Functor.sieves C) (Opposite.op X)) ↦
      Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
        ((Functor.closedSieves J₁).obj (Opposite.op X)) x)
      N hN)
⊢ Subtype.mk (p := fun (x : Sieve.{v, u} X) ↦ J₁.IsClosed x) M hM =
    Subtype.mk (p := fun (x : Sieve.{v, u} X) ↦ J₁.IsClosed x) N hN
have refine_1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X),
  (↑(Subtype.mk (p := fun (x : Sieve.{v, u} X) ↦ J₁.IsClosed x) M hM) : Sieve X).arrows f ↔
    (↑(Subtype.mk (p := fun (x : Sieve.{v, u} X) ↦ J₁.IsClosed x) N hN) : Sieve X).arrows f
Tactic: ext Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve.{v, u} X
hM :
  Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
    ((Functor.closedSieves J₁).obj (Opposite.op X)) M
N : Sieve.{v, u} X
hN :
  Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
    ((Functor.closedSieves J₁).obj (Opposite.op X)) N
hM₂ :
  x.IsAmalgamation (R := S.arrows)
    (Subtype.mk (p := fun (x : Functor.obj (Functor.sieves C) (Opposite.op X)) ↦
      Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
        ((Functor.closedSieves J₁).obj (Opposite.op X)) x)
      M hM)
hN₂ :
  x.IsAmalgamation (R := S.arrows)
    (Subtype.mk (p := fun (x : Functor.obj (Functor.sieves C) (Opposite.op X)) ↦
      Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
        ((Functor.closedSieves J₁).obj (Opposite.op X)) x)
      N hN)
Y : C
f : Y ⟶ X
⊢ (↑(Subtype.mk (p := fun (x : Sieve.{v, u} X) ↦ J₁.IsClosed x) M hM) : Sieve X).arrows f ↔
    (↑(Subtype.mk (p := fun (x : Sieve.{v, u} X) ↦ J₁.IsClosed x) N hN) : Sieve X).arrows f
have refine_1 : M.arrows f ↔ N.arrows f
Tactic: dsimp only [Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Closed (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve.{v, u} X
hM :
  Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
    ((Functor.closedSieves J₁).obj (Opposite.op X)) M
N : Sieve.{v, u} X
hN :
  Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
    ((Functor.closedSieves J₁).obj (Opposite.op X)) N
hM₂ :
  x.IsAmalgamation (R := S.arrows)
    (Subtype.mk (p := fun (x : Functor.obj (Functor.sieves C) (Opposite.op X)) ↦
      Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
        ((Functor.closedSieves J₁).obj (Opposite.op X)) x)
      M hM)
hN₂ :
  x.IsAmalgamation (R := S.arrows)
    (Subtype.mk (p := fun (x : Functor.obj (Functor.sieves C) (Opposite.op X)) ↦
      Membership.mem (γ := Set (Functor.obj (Functor.sieves C) (Opposite.op X)))
        ((Functor.closedSieves J₁).obj (Opposite.op X)) x)
      N hN)
Y : C
f : Y ⟶ X
⊢ M.arrows f ↔ N.arrows f
have refine_1 : J₁.Covers M f ↔ J₁.Covers N f
Tactic: rw [← J₁.covers_iff_mem_of_isClosed hM, ← J₁.covers_iff_mem_of_isClosed hN]