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 R' : Presieve.{v, u} S
h : Sieve.generate R = Sieve.generate R'
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).left)
        fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).hom)
      (F.toDescentData fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).hom) ↔
    Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).left)
        fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
      (F.toDescentData fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
have obtain : ∀ (w : Type (max u v)) (w_1 : w → C) (f : (i : w) → w_1 i ⟶ S)
  (h : Sieve.generate (Presieve.ofArrows w_1 f) = Sieve.generate R'),
  Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).left)
        fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom)
      (F.toDescentData fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom) ↔
    Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).left)
        fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
      (F.toDescentData fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
Tactic: obtain ⟨_, _, f, rfl⟩ := Presieve.exists_eq_ofArrows R
Cleared hypotheses: R, 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' : Presieve.{v, u} S
w : Type (max u v)
w_1 : w → C
f : (i : w) → w_1 i ⟶ S
h : Sieve.generate (Presieve.ofArrows w_1 f) = Sieve.generate R'
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).left)
        fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom)
      (F.toDescentData fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom) ↔
    Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).left)
        fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
      (F.toDescentData fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
have obtain : ∀ (w_2 : Type (max u v)) (w_3 : w_2 → C) (f' : (i : w_2) → w_3 i ⟶ S)
  (h : Sieve.generate (Presieve.ofArrows w_1 f) = Sieve.generate (Presieve.ofArrows w_3 f')),
  Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).left)
        fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom)
      (F.toDescentData fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom) ↔
    Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f : (Presieve.ofArrows w_3 f').category) ↦
        f.obj (P := fun (f : Over.{v, u} S) ↦ Presieve.ofArrows w_3 f' f.hom).left)
        fun (f : (Presieve.ofArrows w_3 f').category) ↦
        f.obj (P := fun (f : Over.{v, u} S) ↦ Presieve.ofArrows w_3 f' f.hom).hom)
      (F.toDescentData fun (f : (Presieve.ofArrows w_3 f').category) ↦
        f.obj (P := fun (f : Over.{v, u} S) ↦ Presieve.ofArrows w_3 f' f.hom).hom)
Tactic: obtain ⟨_, _, f', rfl⟩ := Presieve.exists_eq_ofArrows R'
Cleared hypotheses: R', 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
w : Type (max u v)
w_1 : w → C
f : (i : w) → w_1 i ⟶ S
w_2 : Type (max u v)
w_3 : w_2 → C
f' : (i : w_2) → w_3 i ⟶ S
h : Sieve.generate (Presieve.ofArrows w_1 f) = Sieve.generate (Presieve.ofArrows w_3 f')
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).left)
        fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom)
      (F.toDescentData fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom) ↔
    Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f : (Presieve.ofArrows w_3 f').category) ↦
        f.obj (P := fun (f : Over.{v, u} S) ↦ Presieve.ofArrows w_3 f' f.hom).left)
        fun (f : (Presieve.ofArrows w_3 f').category) ↦
        f.obj (P := fun (f : Over.{v, u} S) ↦ Presieve.ofArrows w_3 f' f.hom).hom)
      (F.toDescentData fun (f : (Presieve.ofArrows w_3 f').category) ↦
        f.obj (P := fun (f : Over.{v, u} S) ↦ Presieve.ofArrows w_3 f' f.hom).hom)
have h₁ : Eq (α := Sieve.{v, u} S)
  (Sieve.ofArrows
    (fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
      f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).left)
    fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
    f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom)
  (Sieve.ofArrows
    (fun (f : (Presieve.ofArrows w_3 f').category) ↦
      f.obj (P := fun (f : Over.{v, u} S) ↦ Presieve.ofArrows w_3 f' f.hom).left)
    fun (f : (Presieve.ofArrows w_3 f').category) ↦
    f.obj (P := fun (f : Over.{v, u} S) ↦ Presieve.ofArrows w_3 f' f.hom).hom)
Tactic: apply DescentData.isEquivalence_toDescentData_iff_of_sieve_eq
-- 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
⊢ F.IsStackFor (Presieve.ofArrows X f) ↔ (F.toDescentData f).IsEquivalence
have simp : Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    F.DescentData (S := S) (X := fun (f_1 : (Presieve.ofArrows X f).category) ↦
      f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows X f f_2.hom).left)
      fun (f_1 : (Presieve.ofArrows X f).category) ↦
      f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows X f f_2.hom).hom)
    (F.toDescentData fun (f_1 : (Presieve.ofArrows X f).category) ↦
      f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows X f f_2.hom).hom) ↔
  (F.toDescentData f).IsEquivalence
Tactic: simp only [isStackFor_iff]
-- 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
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
      F.DescentData (S := S) (X := fun (f_1 : (Presieve.ofArrows X f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows X f f_2.hom).left)
        fun (f_1 : (Presieve.ofArrows X f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows X f f_2.hom).hom)
      (F.toDescentData fun (f_1 : (Presieve.ofArrows X f).category) ↦
        f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows X f f_2.hom).hom) ↔
    (F.toDescentData f).IsEquivalence
have h : (Sieve.ofArrows
    (fun (f_1 : (Presieve.ofArrows X f).category) ↦
      f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows X f f_2.hom).left)
    fun (f_1 : (Presieve.ofArrows X f).category) ↦
    f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows X f f_2.hom).hom) =
  Sieve.ofArrows X f
Tactic: apply DescentData.isEquivalence_toDescentData_iff_of_sieve_eq
-- 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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ 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) ⋯)
have 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) sorry))
        (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
          (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) sorry)) →
            (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
        (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) sorry))
      (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))))
Tactic: rw [Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← (DescentData.subtypeCompatibleHomEquiv F f).bijective.of_comp_iff',
    ← Function.Bijective.of_comp_iff _ (presheafHomObjHomEquiv F).bijective]
-- 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
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).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)))))
have 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) sorry))
      (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
        (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) sorry)) →
          (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
      (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) sorry))
    (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))))
  (F.toDescentData f).map
Tactic: convert! Iff.rfl
-- 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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ 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
have 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) sorry))
        (⇑(DescentData.subtypeCompatibleHomEquiv F f) :
          (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) sorry)) →
            (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
        (Presieve.Arrows.toCompatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) sorry))
      (⇑F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))) φ =
    (F.toDescentData f).map φ
Tactic: ext φ : 1
-- 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 ↔
    ∀ (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 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))
Tactic: rw [isPrestackFor_iff, Functor.FullyFaithful.nonempty_iff_map_bijective]
-- 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
⊢ (∀ (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))
have 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))
Tactic: refine forall_congr' (fun M ↦ forall_congr' (fun 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
S : C
R : Sieve.{v, u} S
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))
have 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 sorry) ↔
  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]
-- 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)
      (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))
have 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 sorry :
    Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
Tactic: convert! Iff.rfl
-- 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')
⊢ 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)))
  (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 sorry :
    Presieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
Tactic: refine le_antisymm ?_ ?_