awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
h :
  LE.le (α := Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
    (Sieve.arrows
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R) :
      Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
    (Presieve.ofArrows (fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
        fun (i : R.arrows.category) ↦ Over.homMk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom ⋯ :
      Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
⊢ Eq (α := Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
    (Sieve.arrows
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R) :
      Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
    (Presieve.ofArrows (fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
        fun (i : R.arrows.category) ↦ Over.homMk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom ⋯ :
      Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
have h₁ : LE.le (α := Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
  (Presieve.ofArrows (fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
      fun (i : R.arrows.category) ↦ Over.homMk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom sorry :
    Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
  (Sieve.arrows
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R) :
    Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
f : X ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ Presieve.ofArrows (fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
    (fun (i : R.arrows.category) ↦ Over.homMk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom ⋯) f
have h : ∀ (X : C) (g : X ⟶ S) (f : Over.mk g ⟶ Over.mk (𝟙 S)) (hf : R.arrows (Over.Hom.left f)),
  Presieve.ofArrows (fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
    (fun (i : R.arrows.category) ↦ Over.homMk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom sorry) f
Tactic: obtain ⟨X, g, rfl⟩ := Over.mk_surjective X
Cleared hypotheses: X, f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ f = Over.homMk g ⋯
have h : Over.Hom.left f = Over.Hom.left (Over.homMk g sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ Presieve.ofArrows (fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
    (fun (i : R.arrows.category) ↦ Over.homMk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom ⋯) f
have h : ∀ (hf : R.arrows (Y := (Over.mk g).left) (Over.Hom.left (Over.homMk g sorry))),
  Presieve.ofArrows (C := Over.{v, u} S) (X := Over.mk (𝟙 S))
    (fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
    fun (i : R.arrows.category) ↦ Over.homMk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom sorry (Y :=
    Over.mk g) (Over.homMk g sorry)
Tactic: obtain rfl : f = Over.homMk g := by ext; simpa using Over.w f
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
⊢ F.IsPrestackFor R.arrows ↔
    ∀ ⦃S₀ : C⦄ (M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')) (a : S ⟶ S₀),
      Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
        (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))
have rw : (∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
    Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
      (Sieve.arrows
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
          R))) ↔
  ∀ ⦃S₀ : C⦄ (M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')) (a : S ⟶ S₀),
    Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
      (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))
Tactic: rw [isPrestackFor_iff_isSheafFor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
tauto tauto₁ tauto₂ tauto₃ tauto₄ :
  (∀ ⦃S₀ : C⦄ (M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')) (a : S ⟶ S₀),
      Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
        (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))) →
    ∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
      Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
⊢ (∀ ⦃S₀ : C⦄ (M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')) (a : S ⟶ S₀),
      Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
        (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))) →
    ∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
      Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
have tauto₅ : (∀ ⦃S₀ : C⦄ (M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')) (a : S ⟶ S₀),
    Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
      (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))) →
  ∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u'))
    (x :
      Presieve.FamilyOfElements (X := Over.mk (𝟙 S)) (F.presheafHom M N)
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R))),
    x.Compatible (R :=
        Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R)) →
      ∃! t : (F.presheafHom M N).obj (op (Over.mk (𝟙 S))),
        x.IsAmalgamation (R :=
          Sieve.arrows
            ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
              R))
          t
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
⊢ (∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
      Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R))) ↔
    ∀ ⦃S₀ : C⦄ (M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')) (a : S ⟶ S₀),
      Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
        (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))
have refine : ∀
  (h :
    ∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
      Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R)))
  (S₀ : C) (M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')) (a : S ⟶ S₀),
  Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
    (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))
Tactic: refine ⟨fun h S₀ M N a ↦ ?_, by tauto⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
h :
  ∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
    Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
      (Sieve.arrows
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
a : S ⟶ S₀
⊢ Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
    (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))
have h₁ : Presieve.IsSheafFor (C := Over.{v, u} S) (X := Over.mk (𝟙 S))
  (F.presheafHom (Functor.obj (Cat.Hom.toFunctor (F.map a.op.toLoc)) M)
    (Functor.obj (Cat.Hom.toFunctor (F.map a.op.toLoc)) N))
  (Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
Tactic: replace h := h ((F.map a.op.toLoc).toFunctor.obj M) ((F.map a.op.toLoc).toFunctor.obj N)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (C := Over.{v, u} S) (X := Over.mk (𝟙 S))
    (F.presheafHom (Functor.obj (Cat.Hom.toFunctor (F.map a.op.toLoc)) M)
      (Functor.obj (Cat.Hom.toFunctor (F.map a.op.toLoc)) N))
    (Sieve.arrows
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
⊢ Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
    (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))
have h₁ : Presieve.IsSheafFor (F.presheafHom M N)
  (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) sorry).inv
      (Sieve.functorPushforward (Over.map a)
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
          R))).arrows
Tactic: rw [← Presieve.isSheafFor_iff_of_iso (F.overMapCompPresheafHomIso M N a),
    Presieve.isSheafFor_over_map_op_comp_iff (X' := Over.mk a)
      (e := Over.isoMk (Iso.refl _))] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a)
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R))).arrows
⊢ Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
    (Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R))
have h₁ : ((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R =
  Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) sorry).inv
    (Sieve.functorPushforward (Over.map a)
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
Tactic: convert! h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a)
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R))).arrows
⊢ ((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R =
    Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
      (Sieve.functorPushforward (Over.map a)
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
have h₁ : ((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R ≤
  Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) sorry).inv
    (Sieve.functorPushforward (Over.map a)
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a)
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R))).arrows
h₁ :
  ((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R ≤
    Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
      (Sieve.functorPushforward (Over.map a)
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
⊢ ((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R =
    Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
      (Sieve.functorPushforward (Over.map a)
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R))
have h₂ : Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) sorry).inv
    (Sieve.functorPushforward (Over.map a)
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R)) ≤
  ((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
a : S ⟶ S₀
h_1 :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a)
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R))).arrows
X : Over.{v, u} S₀
b : X ⟶ Over.mk a
Y : Over.{v, u} S
c : Y ⟶ Over.mk (𝟙 S)
d : X ⟶ (Over.map a).obj Y
h :
  Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R) c
fac : b ≫ (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv = d ≫ (Over.map a).map c
⊢ Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R) b
have fac₁ : Eq (α := Functor.obj (Over.forget S₀) X ⟶ Functor.obj (Over.forget S₀) ((Over.map a).obj (Over.mk (𝟙 S))))
  (Functor.map (Over.forget S₀) (b ≫ (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) sorry).inv))
  (Functor.map (Over.forget S₀) (d ≫ (Over.map a).map c))
Tactic: replace fac := (Over.forget _).congr_map fac
Cleared hypotheses: fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
a : S ⟶ S₀
h_1 :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a)
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R))).arrows
X : Over.{v, u} S₀
b : X ⟶ Over.mk a
Y : Over.{v, u} S
c : Y ⟶ Over.mk (𝟙 S)
d : X ⟶ (Over.map a).obj Y
h :
  Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R) c
fac : Over.Hom.left b ≫ 𝟙 S = Over.Hom.left d ≫ Over.Hom.left c
⊢ Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R) b
have fac₁ : Over.Hom.left b = Over.Hom.left d ≫ Over.Hom.left c
Tactic: rw [Category.comp_id] at fac
Cleared hypotheses: fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
a : S ⟶ S₀
h_1 :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a)
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            R))).arrows
X : Over.{v, u} S₀
b : X ⟶ Over.mk a
Y : Over.{v, u} S
c : Y ⟶ Over.mk (𝟙 S)
d : X ⟶ (Over.map a).obj Y
h :
  Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R) c
fac : Over.Hom.left b = Over.Hom.left d ≫ Over.Hom.left c
⊢ Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R) b
have h₁ : R.arrows (Over.Hom.left b)
Tactic: change R.arrows b.left
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S₀ : C
S : Over.{v, u} S₀
R : Sieve S
hF : F.IsPrestackFor (S := S.left) (Sieve.arrows ((Sieve.overEquiv S : (a : Sieve S) → Sieve S.left) R))
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows
have rw : ∀
  (hF :
    ∀ ⦃S₀_1 : C⦄ (M N : (↑(F.obj { as := op S₀_1 : LocallyDiscrete Cᵒᵖ }) : Type u')) (a : S.left ⟶ S₀_1),
      Presieve.IsSheafFor (X := Over.mk a) (F.presheafHom M N)
        (Sieve.arrows
          (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a))
            ((Sieve.overEquiv S : (a : Sieve S) → Sieve S.left) R))))
  (M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')), Presieve.IsSheafFor (F.presheafHom M N) R.arrows
Tactic: rw [isPrestackFor_iff_isSheafFor'] at hF
Cleared hypotheses: hF, M, N
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
⊢ Nonempty (F.toDescentData f).FullyFaithful
have rw : ∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
  Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
    (Sieve.arrows
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
        (Sieve.generate (Presieve.ofArrows X f))))
Tactic: rw [← isPrestackFor_ofArrows_iff, ← IsPrestackFor_generate_iff,
      isPrestackFor_iff_isSheafFor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
    (Sieve.arrows
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
        (Sieve.generate (Presieve.ofArrows X f))))
have refine : Membership.mem (α := Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S))) (γ := Set (Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S))))
  ((J.over S : (a : Over S) → Set (Sieve a)) (Over.mk (𝟙 S)))
  (Sieve.generate
      (Sieve.arrows
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
          (Sieve.generate (Presieve.ofArrows X f)))) :
    Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
Tactic: refine ((isSheaf_iff_isSheaf_of_type _ _).1
      (IsPrestack.isSheaf J M N)).isSheafFor _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ Membership.mem (α := Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S))) (γ :=
    Set (Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))) ((J.over S : (a : Over S) → Set (Sieve a)) (Over.mk (𝟙 S)))
    (Sieve.generate
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            (Sieve.generate (Presieve.ofArrows X f)))) :
      Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
have rwa : Membership.mem (α := Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))) (γ :=
  Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
  ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S))))
  ((Sieve.overEquiv (Over.mk (𝟙 S)) : (a : Sieve (Over.mk (𝟙 S))) → Sieve (Over.mk (𝟙 S)).left)
      (Sieve.generate
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            (Sieve.generate (Presieve.ofArrows X f))))) :
    Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S))))
Tactic: rwa [GrothendieckTopology.mem_over_iff, Sieve.generate_sieve, Equiv.apply_symm_apply]