awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.GlobalSections (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type w)
inst_2 : HasGlobalSectionsFunctor J (Type w)
F G : Sheaf J (Type w)
f : F ⟶ G
x : Functor.obj (Γ J (Type w)) F
⊢ Eq (α := (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    ((ΓObjEquivSections J G : (a : (Γ J (Type w)).obj G) → (↑G.obj.sections : Type (max u w)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
            (a : (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj F)) → (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj G))
          x) :
      (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.sectionsFunctor Cᵒᵖ) f.hom) :
          (a : (fun (X : Type (max u w)) ↦ X) ((Functor.sectionsFunctor Cᵒᵖ).obj F.obj)) →
            (fun (X : Type (max u w)) ↦ X) ((Functor.sectionsFunctor Cᵒᵖ).obj G.obj))
        ((ΓObjEquivSections J F : (a : (Γ J (Type w)).obj F) → (↑F.obj.sections : Type (max u w))) x) :
      (fun (X : Type (max u w)) ↦ X) (Functor.obj (Functor.sectionsFunctor Cᵒᵖ) (G.obj (P := Presheaf.IsSheaf J))))
have dsimp : Eq (α := (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
  (((G.obj (P := Presheaf.IsSheaf J).sectionsEquivHom PUnit.{w + 1}).symm :
        (a : (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ G.obj) → (↑G.obj.sections : Type (max u w)))
      ((Equiv.symm ΓHomEquiv :
          (a : PUnit.{w + 1} ⟶ (Γ J (Type w)).obj G) → (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ G.obj)
        (↾uniqueElim (α := fun (a : PUnit.{w + 1}) ↦ Functor.obj (Γ J (Type w)) G)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
                (a : (Γ J (Type w)).obj F) → (Γ J (Type w)).obj G)
              x))) :
    (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
  (({
          toFun := fun (x : (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u w))) ↦
            Subtype.mk (p := fun (x : (j : Cᵒᵖ) → G.obj (P := Presheaf.IsSheaf J).obj j) ↦
              x ∈ G.obj (P := Presheaf.IsSheaf J).sections)
              (fun (j : Cᵒᵖ) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app j) : (a : F.obj.obj j) → G.obj.obj j)
                  ((↑x : (j : Cᵒᵖ) → F.obj.obj j) j))
              sorry } :
        (a : (↑F.obj.sections : Type (max u w))) → (↑G.obj.sections : Type (max u w)))
      (((F.obj (P := Presheaf.IsSheaf J).sectionsEquivHom PUnit.{w + 1}).symm :
          (a : (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ F.obj) → (↑F.obj.sections : Type (max u w)))
        ((Equiv.symm ΓHomEquiv :
            (a : PUnit.{w + 1} ⟶ (Γ J (Type w)).obj F) → (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ F.obj)
          (↾uniqueElim (α := fun (a : PUnit.{w + 1}) ↦ Functor.obj (Γ J (Type w)) F) x))) :
    (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
Tactic: dsimp [ΓObjEquivSections]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.GlobalSections (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
X Y : Sheaf J (Type (max u v))
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (Γ J (Type (max u v))) X ⟶ (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).obj Y)
    (Functor.map (Γ J (Type (max u v))) f ≫
      Iso.hom
        ((fun (F : Sheaf J (Type (max u v))) ↦
            (Equiv.toIso (ΓObjEquivSections J F) :
              Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
          Y))
    (Iso.hom
        ((fun (F : Sheaf J (Type (max u v))) ↦
            (Equiv.toIso (ΓObjEquivSections J F) :
              Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
          X) ≫
      (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).map f)
have h : ∀ (x : Functor.obj (Γ J (Type (max u v))) X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Γ J (Type (max u v))) f ≫
          Iso.hom
            ((fun (F : Sheaf J (Type (max u v))) ↦
                (Equiv.toIso (ΓObjEquivSections J F) :
                  Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (F : Sheaf J (Type (max u v))) ↦
                (Equiv.toIso (ΓObjEquivSections J F) :
                  Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
              X) ≫
          (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).map f))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.GlobalSections (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
X : Type (max u v)
inst_3 : Unique X
X_1 Y : Sheaf J (Type (max u v))
f : X_1 ⟶ Y
⊢ Eq (α :=
    Functor.obj (Γ J (Type (max u v))) X_1 ⟶
      Functor.obj (Functor.obj coyoneda (op (Functor.obj (constantSheaf J (Type (max u v))) X))) Y)
    (Functor.map (Γ J (Type (max u v))) f ≫
      Iso.hom
        ((fun (F : Sheaf J (Type (max u v))) ↦
            (Equiv.toIso (ΓObjEquivHom J F X) :
              Functor.obj (Γ J (Type (max u v))) F ≅ Functor.obj (constantSheaf J (Type (max u v))) X ⟶ F))
          Y))
    (Iso.hom
        ((fun (F : Sheaf J (Type (max u v))) ↦
            (Equiv.toIso (ΓObjEquivHom J F X) :
              Functor.obj (Γ J (Type (max u v))) F ≅ Functor.obj (constantSheaf J (Type (max u v))) X ⟶ F))
          X_1) ≫
      Functor.map (Functor.obj coyoneda (op (Functor.obj (constantSheaf J (Type (max u v))) X))) f)
have h : ∀ (x : Functor.obj (Γ J (Type (max u v))) X_1),
  Eq (α := Functor.obj (Functor.obj coyoneda (op (Functor.obj (constantSheaf J (Type (max u v))) X))) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Γ J (Type (max u v))) f ≫
          Iso.hom
            ((fun (F : Sheaf J (Type (max u v))) ↦
                (Equiv.toIso (ΓObjEquivHom J F X) :
                  Functor.obj (Γ J (Type (max u v))) F ≅ Functor.obj (constantSheaf J (Type (max u v))) X ⟶ F))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (F : Sheaf J (Type (max u v))) ↦
                (Equiv.toIso (ΓObjEquivHom J F X) :
                  Functor.obj (Γ J (Type (max u v))) F ≅ Functor.obj (constantSheaf J (Type (max u v))) X ⟶ F))
              X_1) ≫
          Functor.map (Functor.obj coyoneda (op (Functor.obj (constantSheaf J (Type (max u v))) X))) f))
      x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h :
  Eq (α := (a : C) → Set (Sieve.{v, u} a)) ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X) J₁)
    ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X) J₂)
⊢ J₁ = J₂
have mk : ∀ (sieves : (X : C) → Set (Sieve.{v, u} X)) (top_mem' : ∀ (X : C), ⊤ ∈ sieves X)
  (pullback_stable' : ∀ ⦃X Y : C⦄ ⦃S : Sieve.{v, u} X⦄ (f : Y ⟶ X), S ∈ sieves X → Sieve.pullback f S ∈ sieves Y)
  (transitive' :
    ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
      S ∈ sieves X →
        ∀ (R : Sieve.{v, u} X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X)
  (h :
    Eq (α := (a : C) → Set (Sieve.{v, u} a))
      ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
        { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' })
      ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X) J₂)),
  { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' :
      GrothendieckTopology.{v, u} C } =
    J₂
Tactic: cases J₁
Cleared hypotheses: J₁, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J₂ : GrothendieckTopology.{v, u} C
sieves : (X : C) → Set (Sieve.{v, u} X)
top_mem' : ∀ (X : C), ⊤ ∈ sieves X
pullback_stable' : ∀ ⦃X Y : C⦄ ⦃S : Sieve.{v, u} X⦄ (f : Y ⟶ X), S ∈ sieves X → Sieve.pullback f S ∈ sieves Y
transitive' :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
    S ∈ sieves X →
      ∀ (R : Sieve.{v, u} X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X
h :
  Eq (α := (a : C) → Set (Sieve.{v, u} a))
    ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
      { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' })
    ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X) J₂)
⊢ { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' :
      GrothendieckTopology.{v, u} C } =
    J₂
have mk : ∀ (sieves_1 : (X : C) → Set (Sieve.{v, u} X)) (top_mem'_1 : ∀ (X : C), ⊤ ∈ sieves_1 X)
  (pullback_stable'_1 : ∀ ⦃X Y : C⦄ ⦃S : Sieve.{v, u} X⦄ (f : Y ⟶ X), S ∈ sieves_1 X → Sieve.pullback f S ∈ sieves_1 Y)
  (transitive'_1 :
    ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
      S ∈ sieves_1 X →
        ∀ (R : Sieve.{v, u} X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves_1 Y) → R ∈ sieves_1 X)
  (h :
    Eq (α := (a : C) → Set (Sieve.{v, u} a))
      ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
        { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' })
      ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
        { sieves := sieves_1, top_mem' := top_mem'_1, pullback_stable' := pullback_stable'_1,
          transitive' := transitive'_1 })),
  { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' :
      GrothendieckTopology.{v, u} C } =
    { sieves := sieves_1, top_mem' := top_mem'_1, pullback_stable' := pullback_stable'_1, transitive' := transitive'_1 }
Tactic: cases J₂
Cleared hypotheses: J₂, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
⊢ Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X ↔ S ∈ (J : (a : C) → Set (Sieve a)) Y
have refine : ∀ (H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X), S ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: refine ⟨fun H ↦ ?_, J.pullback_stable i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) Y
have h : S = Sieve.pullback (inv i) (Sieve.pullback i S)
Tactic: convert! J.pullback_stable (inv i) H
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S = Sieve.pullback (inv i) (Sieve.pullback i S)
have h : S = Sieve.pullback (inv i ≫ i) S
Tactic: rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X
h : S = Sieve.pullback (inv i ≫ i) S
⊢ S = Sieve.pullback (inv i) (Sieve.pullback i S)
have h₁ : S = Sieve.pullback (𝟙 Y) S
Tactic: rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X
h : S = Sieve.pullback (inv i ≫ i) S
h₁ : S = Sieve.pullback (𝟙 Y) S
⊢ S = Sieve.pullback (inv i) (Sieve.pullback i S)
have h₂ : S = S
Tactic: rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
Hss : S ≤ R
sjx : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ R ∈ (J : (a : C) → Set (Sieve a)) X
have apply : ∀ (Y : C) (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f R ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: apply J.transitive sjx R fun Y f hf => _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
Hss : S ≤ R
sjx : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R ∈ (J : (a : C) → Set (Sieve a)) Y
have a : Sieve.pullback f R = ⊤
Tactic: apply covering_of_eq_top
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
Hss : S ≤ R
sjx : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R = ⊤
have a : Sieve.pullback f S ≤ Sieve.pullback f R
Tactic: rw [← top_le_iff, ← S.pullback_eq_top_of_mem hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
rj : R ∈ (J : (a : C) → Set (Sieve a)) X
sj : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ R ⊓ S ∈ (J : (a : C) → Set (Sieve a)) X
have apply : ∀ (Y : C) (f : Y ⟶ X) (Hf : R.arrows f), Sieve.pullback f (R ⊓ S) ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: apply J.transitive rj _ fun Y f Hf => _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
rj : R ∈ (J : (a : C) → Set (Sieve a)) X
sj : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ (J : (a : C) → Set (Sieve a)) Y
have rw : ⊤ ⊓ Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: rw [Sieve.pullback_inter, R.pullback_eq_top_of_mem hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v, u} (Z i)
h : Sieve.ofArrows Z f ∈ (J : (a : C) → Set (Sieve a)) X
hR :
  ∀ (i : ι), Membership.mem (γ := Set (Sieve.{v, u} (Z i))) ((J : (a : C) → Set (Sieve a)) (Z i)) (Sieve.generate (R i))
⊢ Sieve.generate (Presieve.bindOfArrows Z f R) ∈ (J : (a : C) → Set (Sieve a)) X
have refine : (Sieve.bind (Sieve.ofArrows Z f).arrows fun (x : C) (x_1 : x ⟶ X) (hg : (Sieve.ofArrows Z f).arrows x_1) ↦
    Sieve.pullback (Sieve.ofArrows.h hg) (Sieve.generate (R (Sieve.ofArrows.i hg)))) ∈
  (J : (a : C) → Set (Sieve a)) X
Tactic: refine J.superset_covering (Presieve.bind_ofArrows_le_bindOfArrows _ _ _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S : Sieve.{v, u} X
hf : S.arrows f
⊢ J.Covers S f
have rw : ⊤ ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: rw [Covers, (Sieve.mem_iff_pullback_eq_top f).1 hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S : Sieve.{v, u} X
h : J.Covers S f
Z : C
g : Z ⟶ Y
⊢ J.Covers S (g ≫ f)
have rw : ∀ (h : Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y) {Z : C} (g : Z ⟶ Y),
  Sieve.pullback (g ≫ f) S ∈ (J : (a : C) → Set (Sieve a)) Z
Tactic: rw [covers_iff] at h ⊢
Cleared hypotheses: h, Z, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S R : Sieve.{v, u} X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
⊢ J.Covers R f
have h₁ : ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
  (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ (J : (a : C) → Set (Sieve a)) Y_1
Tactic: apply J.transitive h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S R : Sieve.{v, u} X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ (J : (a : C) → Set (Sieve a)) Z
have h₁ : Sieve.pullback (g ≫ f) R ∈ (J : (a : C) → Set (Sieve a)) Z
Tactic: rw [← Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
hf : Membership.mem (γ := Set (Sieve.{v, u} X)) {⊤} S
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y)) {⊤} (Sieve.pullback f S)
have hf₁ : S = ⊤
Tactic: rw [Set.mem_singleton_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : Membership.mem (γ := Set (Sieve.{v, u} X)) {⊤} S
R : Sieve.{v, u} X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Membership.mem (γ := Set (Sieve.{v, u} Y)) {⊤} (Sieve.pullback f R)
⊢ Membership.mem (γ := Set (Sieve.{v, u} X)) {⊤} R
have rw : ∀ (hS : S.arrows (𝟙 X)) (R : Sieve.{v, u} X)
  (hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Membership.mem (γ := Set (Sieve.{v, u} Y)) {⊤} (Sieve.pullback f R)),
  Membership.mem (γ := Set (Sieve.{v, u} X)) {⊤} R
Tactic: rw [Set.mem_singleton_iff, ← Sieve.id_mem_iff_eq_top] at hS
Cleared hypotheses: hS, R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
s : Set (GrothendieckTopology.{v, u} C)
⊢ IsGLB s (sInf s)
have refine_1 : ∀ {x y : GrothendieckTopology.{v, u} C}, x.sieves ≤ y.sieves ↔ x ≤ y
Tactic: refine @IsGLB.of_image _ _ _ _ sieves ?_ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
s : Set (GrothendieckTopology.{v, u} C)
refine_1 : ∀ {x y : GrothendieckTopology.{v, u} C}, x.sieves ≤ y.sieves ↔ x ≤ y
⊢ IsGLB s (sInf s)
have refine_2 : IsGLB (sieves '' s) (sInf s).sieves
Tactic: refine @IsGLB.of_image _ _ _ _ sieves ?_ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ Eq (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤
have a : LE.le (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
a : LE.le (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤
⊢ Eq (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤
have a₁ : LE.le (α := GrothendieckTopology.{v, u} C) ⊤ (discrete C)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ Eq (α := GrothendieckTopology.{v, u} C) (trivial C) ⊥
have a : LE.le (α := GrothendieckTopology.{v, u} C) (trivial C) ⊥
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
a : LE.le (α := GrothendieckTopology.{v, u} C) (trivial C) ⊥
⊢ Eq (α := GrothendieckTopology.{v, u} C) (trivial C) ⊥
have a₁ : LE.le (α := GrothendieckTopology.{v, u} C) ⊥ (trivial C)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (trivial C : (a : C) → Set (Sieve a)) X
⊢ S ∈ (⊥ : (a : C) → Set (Sieve a)) X
have hS₁ : S = ⊤
Tactic: rw [trivial_covering] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
⊢ Covers ⊥ S f ↔ S.arrows f
have rw : Sieve.pullback f S ∈ (⊥ : (a : C) → Set (Sieve a)) Y ↔ S.arrows f
Tactic: rw [covers_iff, bot_covering, ← Sieve.mem_iff_pullback_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
rw : Sieve.pullback f S ∈ (⊥ : (a : C) → Set (Sieve a)) Y ↔ S.arrows f
⊢ Covers ⊥ S f ↔ S.arrows f
have rw₁ : Sieve.pullback f S = ⊤ ↔ S.arrows f
Tactic: rw [covers_iff, bot_covering, ← Sieve.mem_iff_pullback_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
rw : Sieve.pullback f S ∈ (⊥ : (a : C) → Set (Sieve a)) Y ↔ S.arrows f
rw₁ : Sieve.pullback f S = ⊤ ↔ S.arrows f
⊢ Covers ⊥ S f ↔ S.arrows f
have rw₂ : S.arrows f ↔ S.arrows f
Tactic: rw [covers_iff, bot_covering, ← Sieve.mem_iff_pullback_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
⊢ J = ⊤ ↔ ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
have refine : ∀ (h : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X), J = ⊤
Tactic: refine ⟨fun h ↦ h ▸ by simp, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
h : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
⊢ J = ⊤
have rw : ⊤ ≤ J
Tactic: rw [_root_.eq_top_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsEmpty C
J : GrothendieckTopology.{v, u} C
⊢ J = ⊤
have rw : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := GrothendieckTopology.{v, u} C) ⊥ ⊤ ↔ IsEmpty C
have refine : ∀ (h : Eq (α := GrothendieckTopology.{v, u} C) ⊥ ⊤) (X : C), False
Tactic: refine ⟨fun h ↦ ⟨fun X ↦ ?_⟩, fun h ↦ eq_top_of_isEmpty _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Eq (α := GrothendieckTopology.{v, u} C) ⊥ ⊤
X : C
⊢ False
have apply : Eq (α := Sieve.{v, u} X) ⊥ ⊤
Tactic: apply bot_ne_top (α := Sieve X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ LT.lt (α := GrothendieckTopology.{v, u} C) ⊥ ⊤ ↔ Nonempty C
have contrapose! : ¬LT.lt (α := GrothendieckTopology.{v, u} C) ⊥ ⊤ ↔ IsEmpty C
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
H :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
Z : C
f : Z ⟶ Y
⊢ ∃ (Z_1 : C) (g : Z_1 ⟶ Z), (Sieve.pullback h S).arrows (g ≫ f)
have rcases : ∀ (W : C) (g : W ⟶ Z) (H' : S.arrows (g ≫ f ≫ h)), ∃ (Z_1 : C) (g : Z_1 ⟶ Z), (Sieve.pullback h S).arrows (g ≫ f)
Tactic: rcases H (f ≫ h) with ⟨W, g, H'⟩