awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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')
Y obj : Over.{v, u} S
h : R.arrows obj.hom
⊢ Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R :
      Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
    (Y :=
    Over.mk
      (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom)
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom) obj h)).hom)
    (Over.homMk
        (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom)
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom) obj h)).hom
        ⋯ :
      Quiver.Hom (V := Over.{v, u} S)
        ((fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom) obj h))
        (Over.mk (𝟙 S)))

Tactic:
h

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.Presieve.functorPullback
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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')
Y obj : Over.{v, u} S
h : R.arrows obj.hom
⊢ Sieve.arrows
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S))) R :
      Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
    (Y :=
    Over.mk
      (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom)
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom) obj h)).hom)
    (Over.homMk
        (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom)
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom) obj h)).hom
        ⋯ :
      Quiver.Hom (V := Over.{v, u} S)
        ((fun (i : R.arrows.category) ↦ Over.mk i.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom) obj h))
        (Over.mk (𝟙 S)))

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
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))
⊢ 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))

Tactic:
rw [isPrestackFor_iff_isSheafFor]

Premises used: CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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))
tauto₅ tauto₆ tauto₇ tauto₈ 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'))
      (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
⊢ (∀ ⦃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))

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve.{v, u} S
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))
⊢ (∀ (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⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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 (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)
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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 (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

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

Premises used: CategoryTheory.Over.isoMk, CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff, CategoryTheory.Presieve.isSheafFor_iff_of_iso, CategoryTheory.Pseudofunctor.overMapCompPresheafHomIso
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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 (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

Tactic:
h
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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))
⊢ 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:
convert! h
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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))
h₂ :
  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.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))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
Y : Over.{v, u} S₀
f : Y ⟶ Over.mk a
hf : Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R) f
⊢ 𝟙 Y.left ≫ ((Over.map a).obj (Over.mk (Over.Hom.left f))).hom = Y.hom

Tactic:
simpa using Over.w f

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
Y : Over.{v, u} S₀
f : Y ⟶ Over.mk a
hf : Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R) f
⊢ (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
    f

Tactic:
exact ⟨Over.mk f.left, Over.homMk f.left, Over.homMk (𝟙 _) (by simpa using Over.w f),
      hf, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
⊢ 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) ⋯).inv))
    (Functor.map (Over.forget S₀) (d ≫ (Over.map a).map c))

Tactic:
replace fac := (Over.forget _).congr_map fac
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
⊢ Over.Hom.left b = Over.Hom.left d ≫ Over.Hom.left c

Tactic:
rw [Category.comp_id] at fac

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
h₁ : R.arrows (Over.Hom.left b)
⊢ Sieve.arrows (((Sieve.overEquiv (Over.mk a)).symm : (a_1 : Sieve (Over.mk a).left) → Sieve (Over.mk a)) R) b

Tactic:
change R.arrows b.left

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.Sieve.arrows
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
⊢ R.arrows (Over.Hom.left b)

Tactic:
simpa [fac] using R.downward_closed h d.left

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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')
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
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows

Tactic:
rw [isPrestackFor_iff_isSheafFor'] at hF

Premises used: CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor'
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S₀ : C
M N : (↑(F.obj { as := op S₀ : LocallyDiscrete Cᵒᵖ }) : Type u')
S : C
a : S ⟶ S₀
R : Sieve (Over.mk a)
hF :
  ∀ ⦃S₀_1 : C⦄ (M N : (↑(F.obj { as := op S₀_1 : LocallyDiscrete Cᵒᵖ }) : Type u')) (a_1 : (Over.mk a).left ⟶ S₀_1),
    Presieve.IsSheafFor (X := Over.mk a_1) (F.presheafHom M N)
      (Sieve.arrows
        (((Sieve.overEquiv (Over.mk a_1)).symm : (a_2 : Sieve (Over.mk a_1).left) → Sieve (Over.mk a_1))
          ((Sieve.overEquiv (Over.mk a) : (a_2 : Sieve (Over.mk a)) → Sieve (Over.mk a).left) R)))
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows

Tactic:
simpa using hF M N a
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
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))))
⊢ Nonempty (F.toDescentData f).FullyFaithful

Tactic:
rw [← isPrestackFor_ofArrows_iff, ← IsPrestackFor_generate_iff,
      isPrestackFor_iff_isSheafFor]

Premises used: CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor, CategoryTheory.Pseudofunctor.IsPrestackFor_generate_iff