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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
rw :
  Function.Bijective (α := M ⟶ N) (F.toDescentData f).map ↔
    Function.Bijective (α := M ⟶ N) (β := (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
      (Function.comp (β := (F.presheafHom M N).obj (op (Over.mk (𝟙 S))))
        (Function.comp (β :=
          Subtype (α := (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i)))
            (Presieve.Arrows.Compatible (F.presheafHom M N) (B := Over.mk (𝟙 S)) fun (i : ι) ↦ Over.homMk (f i) ⋯))
          (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
            (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
              (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
          (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯))
        (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))))
⊢ Function.Bijective (α := M ⟶ N) (F.toDescentData f).map ↔
    Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
      (Presieve.ofArrows (fun (i : ι) ↦ Over.mk (f i)) fun (i : ι) ↦ Over.homMk (f i) ⋯)

Tactic:
rw [Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← (DescentData.subtypeCompatibleHomEquiv F f).bijective.of_comp_iff',
    ← Function.Bijective.of_comp_iff _ (presheafHomObjHomEquiv F).bijective]

Premises used: Equiv.bijective, CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv, Function.Bijective.of_comp_iff, Function.Bijective.of_comp_iff', CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv
-- 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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ Function.Bijective (α := M ⟶ N) (F.toDescentData f).map ↔ Function.Bijective (α := M ⟶ N) (F.toDescentData f).map

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- 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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
h :
  Eq (α := (M ⟶ N) → ((F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N))
    (Function.comp (β := (F.presheafHom M N).obj (op (Over.mk (𝟙 S))))
      (Function.comp (β :=
        Subtype (α := (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i)))
          (Presieve.Arrows.Compatible (F.presheafHom M N) (B := Over.mk (𝟙 S)) fun (i : ι) ↦ Over.homMk (f i) ⋯))
        (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
          (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
            (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
        (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯))
      (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))))
    (F.toDescentData f).map
⊢ Function.Bijective (α := M ⟶ N) (F.toDescentData f).map ↔
    Function.Bijective (α := M ⟶ N) (β := (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
      (Function.comp (β := (F.presheafHom M N).obj (op (Over.mk (𝟙 S))))
        (Function.comp (β :=
          Subtype (α := (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i)))
            (Presieve.Arrows.Compatible (F.presheafHom M N) (B := Over.mk (𝟙 S)) fun (i : ι) ↦ Over.homMk (f i) ⋯))
          (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
            (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
              (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
          (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯))
        (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))))

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- 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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
h :
  ∀ (φ : M ⟶ N),
    Function.comp (β := (F.presheafHom M N).obj (op (Over.mk (𝟙 S))))
        (Function.comp (β :=
          Subtype (α := (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i)))
            (Presieve.Arrows.Compatible (F.presheafHom M N) (B := Over.mk (𝟙 S)) fun (i : ι) ↦ Over.homMk (f i) ⋯))
          (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
            (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
              (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
          (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯))
        (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))) φ =
      (F.toDescentData f).map φ
⊢ Eq (α := (M ⟶ N) → ((F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N))
    (Function.comp (β := (F.presheafHom M N).obj (op (Over.mk (𝟙 S))))
      (Function.comp (β :=
        Subtype (α := (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i)))
          (Presieve.Arrows.Compatible (F.presheafHom M N) (B := Over.mk (𝟙 S)) fun (i : ι) ↦ Over.homMk (f i) ⋯))
        (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
          (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
            (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
        (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯))
      (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))))
    (F.toDescentData f).map

Tactic:
ext φ : 1
-- 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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
φ : M ⟶ N
⊢ Function.comp (β := (F.presheafHom M N).obj (op (Over.mk (𝟙 S))))
      (Function.comp (β :=
        Subtype (α := (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i)))
          (Presieve.Arrows.Compatible (F.presheafHom M N) (B := Over.mk (𝟙 S)) fun (i : ι) ↦ Over.homMk (f i) ⋯))
        (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
          (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
            (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
        (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯))
      (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))) φ =
    (F.toDescentData f).map φ

Tactic:
apply DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv

Premises used: CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv
-- 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 :
  (∀ (X Y : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
      Function.Bijective (α := X ⟶ Y) (β :=
        Quiver.Hom (V :=
          F.DescentData (S := S) (X := fun (f : R.arrows.category) ↦
            f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).left) fun (f : R.arrows.category) ↦
            f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
          (Functor.obj
            (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom) X)
          (Functor.obj
            (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
            Y))
        (Functor.map
          (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom))) ↔
    ∀ (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))
⊢ F.IsPrestackFor R.arrows ↔
    ∀ (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:
rw [isPrestackFor_iff, Functor.FullyFaithful.nonempty_iff_map_bijective]

Premises used: CategoryTheory.Functor.FullyFaithful.nonempty_iff_map_bijective, CategoryTheory.Pseudofunctor.isPrestackFor_iff
-- 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
⊢ (∀ (X Y : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
      Function.Bijective (α := X ⟶ Y) (β :=
        Quiver.Hom (V :=
          F.DescentData (S := S) (X := fun (f : R.arrows.category) ↦
            f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).left) fun (f : R.arrows.category) ↦
            f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
          (Functor.obj
            (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom) X)
          (Functor.obj
            (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
            Y))
        (Functor.map
          (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom))) ↔
    ∀ (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:
forall_congr' (fun M ↦ forall_congr' (fun N ↦ ?_))

Premises used: forall_congr'
-- 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 :
  ∀ (M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
    Function.Bijective (α := M ⟶ N) (β :=
        Quiver.Hom (V :=
          F.DescentData (S := S) (X := fun (f : R.arrows.category) ↦
            f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).left) fun (f : R.arrows.category) ↦
            f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
          (Functor.obj
            (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom) M)
          (Functor.obj
            (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
            N))
        (Functor.map
          (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)) ↔
      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))
⊢ (∀ (X Y : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')),
      Function.Bijective (α := X ⟶ Y) (β :=
        Quiver.Hom (V :=
          F.DescentData (S := S) (X := fun (f : R.arrows.category) ↦
            f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).left) fun (f : R.arrows.category) ↦
            f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
          (Functor.obj
            (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom) X)
          (Functor.obj
            (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
            Y))
        (Functor.map
          (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom))) ↔
    ∀ (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:
refine forall_congr' (fun M ↦ forall_congr' (fun N ↦ ?_))

Premises used: forall_congr'
-- 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')
rw :
  Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
      (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.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))
⊢ Function.Bijective (α := M ⟶ N) (β :=
      Quiver.Hom (V :=
        F.DescentData (S := S) (X := fun (f : R.arrows.category) ↦
          f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).left) fun (f : R.arrows.category) ↦
          f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
        (Functor.obj
          (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom) M)
        (Functor.obj
          (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom) N))
      (Functor.map
        (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)) ↔
    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:
rw [bijective_toDescentData_map_iff]

Premises used: CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff
-- 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')
⊢ Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
      (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.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
      (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 ⋯)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- 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')
h :
  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)))
⊢ Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
      (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.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:
convert! Iff.rfl

Premises used: Iff.rfl
-- 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')
⊢ 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)))

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
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)))
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 ⋯ :
      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)))
⊢ 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)))

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
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)
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 ⋯) 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

Tactic:
obtain ⟨X, g, rfl⟩ := Over.mk_surjective X

Premises used: CategoryTheory.Over.mk_surjective, rfl
-- 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')
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
h : Over.Hom.left f = Over.Hom.left (Over.homMk g ⋯)
⊢ f = Over.homMk g ⋯

Tactic:
ext
-- 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')
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ Over.Hom.left f = Over.Hom.left (Over.homMk g ⋯)

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
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)
h :
  ∀ (hf : R.arrows (Y := (Over.mk g).left) (Over.Hom.left (Over.homMk g ⋯))),
    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 ⋯ (Y :=
      Over.mk g) (Over.homMk g ⋯)
⊢ 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

Tactic:
obtain rfl : f = Over.homMk g := by ext; simpa using Over.w f

Premises used: CategoryTheory.Over.homMk, rfl
-- 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')
X : C
g : X ⟶ S
hf : R.arrows (Y := (Over.mk g).left) (Over.Hom.left (Over.homMk g ⋯))
⊢ 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 ⋯ (Y :=
    Over.mk g) (Over.homMk g ⋯)

Tactic:
Presieve.ofArrows.mk (ι := R.arrows.category) ⟨Over.mk g, hf⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Over.mk
-- 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')
X : C
g : X ⟶ S
hf : R.arrows (Y := (Over.mk g).left) (Over.Hom.left (Over.homMk g ⋯))
⊢ 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 ⋯ (Y :=
    Over.mk g) (Over.homMk g ⋯)

Tactic:
exact Presieve.ofArrows.mk (ι := R.arrows.category) ⟨Over.mk g, hf⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Over.mk