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' : 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'
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')),
    Nonempty
        (Functor.FullyFaithful (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)) ↔
      Nonempty
        (Functor.FullyFaithful (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))
⊢ Nonempty
      (Functor.FullyFaithful (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)) ↔
    Nonempty
      (Functor.FullyFaithful (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'

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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')
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)
⊢ Nonempty
      (Functor.FullyFaithful (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)) ↔
    Nonempty
      (Functor.FullyFaithful (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:
apply DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq

Premises used: CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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')
⊢ 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:
simpa only [Sieve.ofArrows_category']

Premises used: CategoryTheory.Sieve.ofArrows_category'
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve.{v, u} S
⊢ Sieve.generate (Sieve.generate R).arrows = Sieve.generate R

Tactic:
simp
-- 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
simp :
  Nonempty
      (Functor.FullyFaithful (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)) ↔
    Nonempty (F.toDescentData f).FullyFaithful
⊢ F.IsPrestackFor (Presieve.ofArrows X f) ↔ Nonempty (F.toDescentData f).FullyFaithful

Tactic:
simp only [isPrestackFor_iff]

Premises used: CategoryTheory.Pseudofunctor.isPrestackFor_iff
-- 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
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
⊢ Nonempty
      (Functor.FullyFaithful (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)) ↔
    Nonempty (F.toDescentData f).FullyFaithful

Tactic:
apply DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq

Premises used: CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq
-- 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
h h₁ : Sieve.generate (Presieve.ofArrows X f) = Sieve.ofArrows X f
⊢ (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:
rw [Sieve.ofArrows_category']

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

Tactic:
rw [isStackFor_iff] at h

Premises used: CategoryTheory.Pseudofunctor.isStackFor_iff
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve.{v, u} S
h :
  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.FullyFaithful (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:
exact .ofFullyFaithful _
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve.{v, u} S
h : F.IsStackFor 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)

Tactic:
have := h.isEquivalence
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve.{v, u} S
h : F.IsStackFor R
this :
  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.EssSurj (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:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
simp :
  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)
⊢ F.IsStackFor R ↔ F.IsStackFor R'

Tactic:
simp only [isStackFor_iff]

Premises used: CategoryTheory.Pseudofunctor.isStackFor_iff
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
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)
⊢ 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)

Tactic:
obtain ⟨_, _, f, rfl⟩ := Presieve.exists_eq_ofArrows R

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
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)
⊢ 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'

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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')
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)
⊢ 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:
apply DescentData.isEquivalence_toDescentData_iff_of_sieve_eq

Premises used: CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq
-- 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
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
⊢ F.IsStackFor (Presieve.ofArrows X f) ↔ (F.toDescentData f).IsEquivalence

Tactic:
simp only [isStackFor_iff]

Premises used: CategoryTheory.Pseudofunctor.isStackFor_iff
-- 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
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
⊢ 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:
apply DescentData.isEquivalence_toDescentData_iff_of_sieve_eq

Premises used: CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq