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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
i : ι
⊢ (Sieve.ofArrows X' f').arrows (f i)
have rw : (Sieve.ofArrows X f).arrows (f i)
Tactic: rw [← 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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
i : ι
⊢ ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i
have obtain : ∀ ⦃Y : C⦄ (i' : ι') (w : X i ⟶ X' i') (fac : w ≫ f' i' = f i), ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i
Tactic: obtain ⟨_, _, _, ⟨i'⟩, fac⟩ : Sieve.ofArrows X' f' (f i) := by
      rw [← h]; apply Sieve.ofArrows_mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
⊢ ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
have h₂ : ∀ (i : ι), ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i
Tactic: have h₂ (i : ι) : ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i := by
    obtain ⟨_, _, _, ⟨i'⟩, fac⟩ : Sieve.ofArrows X' f' (f i) := by
      rw [← h]; apply Sieve.ofArrows_mk
    exact ⟨i', _, fac⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
h₂ : ∀ (i : ι), ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i
⊢ ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
have choose : ∀ (α : (i' : ι') → ι) (p' : (i' : ι') → X' i' ⟶ X (α i')) (w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'),
  ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
Tactic: choose α p' w using h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₂ : ∀ (i : ι), ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i
α : (i' : ι') → ι
p' : (i' : ι') → X' i' ⟶ X (α i')
w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'
⊢ ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
have choose : ∀ (β : (i : ι) → ι') (q' : (i : ι) → X i ⟶ X' (β i)) (w' : ∀ (i : ι), q' i ≫ f' (β i) = f i),
  ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
Tactic: choose β q' w' using h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
⊢ Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful
have obtain : ∀ (e : F.DescentData f ≌ F.DescentData f') (iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'),
  Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful
Tactic: obtain ⟨e, ⟨iso⟩⟩ := DescentData.exists_equivalence_of_sieve_eq F f f' 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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence
have obtain : ∀ (e : F.DescentData f ≌ F.DescentData f') (iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'),
  (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence
Tactic: obtain ⟨e, ⟨iso⟩⟩ := DescentData.exists_equivalence_of_sieve_eq F f f' 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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
e : F.DescentData f ≌ F.DescentData f'
iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence
have rw : (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f ⋙ e.functor).IsEquivalence
Tactic: rw [← Functor.isEquivalence_iff_of_iso iso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
φ :
  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) ⋯)
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₁) ≫
      ((F.toDescentData f).obj N).hom q f₁ f₂ ⋯ ⋯ =
    ((F.toDescentData f).obj M).hom q f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₂)
have this : Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom M N).map (Quiver.Hom.op (Over.homMk f₁ sorry))) :
        (a : (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i₁)))) →
          (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
      ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₁) :
    (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom M N).map (Quiver.Hom.op (Over.homMk f₂ sorry))) :
        (a : (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i₂)))) →
          (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
      ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₂) :
    (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
Tactic: have := φ.property i₁ i₂ (Over.mk q) (Over.homMk f₁) (Over.homMk f₂) (by cat_disch)
-- 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')
φ : M ⟶ N
⊢ (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 : ∀ (i : ι),
  Hom.hom
      ((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)))) φ)))
      i =
    ((F.toDescentData f).map φ).hom i
Tactic: ext i
-- 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'
⊢ F.IsPrestackFor R ↔ F.IsPrestackFor R'
have simp : 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)) ↔
  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: simp only [isPrestackFor_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 R' : Presieve.{v, u} S
h : Sieve.generate R = Sieve.generate R'
⊢ 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)) ↔
    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))
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'),
  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
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'
⊢ 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))
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')),
  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: 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')
⊢ 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))
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.nonempty_fullyFaithful_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.IsPrestackFor (Presieve.ofArrows X f) ↔ Nonempty (F.toDescentData f).FullyFaithful
have 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
Tactic: simp only [isPrestackFor_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
⊢ 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
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.nonempty_fullyFaithful_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
⊢ (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
have h : Sieve.generate (Presieve.ofArrows X f) = Sieve.ofArrows X f
Tactic: rw [Sieve.ofArrows_category']
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve.{v, u} S
h : F.IsStackFor R
⊢ 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)
have 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)
Tactic: rw [isStackFor_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve.{v, u} S
h : F.IsStackFor R
⊢ 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)
have 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)
Tactic: have := h.isEquivalence
-- 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'
⊢ F.IsStackFor R ↔ F.IsStackFor R'
have 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)
Tactic: simp only [isStackFor_iff]