awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsStack J
S : C
R : Sieve.{v, u} S
hR : R ∈ (J : (a : C) → Set (Sieve a)) S
hF :
  Functor.FullyFaithful (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
this_1 :
  Functor.Full (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
this :
  Functor.Faithful (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
⊢ Functor.EssSurj (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)

Tactic:
have := IsStack.essSurj_of_sieve F _ hR
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsStack J
S : C
R : Sieve.{v, u} S
hR : R ∈ (J : (a : C) → Set (Sieve a)) S
hF :
  Functor.FullyFaithful (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
this_1 :
  Functor.Full (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
this_2 :
  Functor.Faithful (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
this :
  Functor.EssSurj (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)

Tactic:

Premises used: CategoryTheory.Functor.IsEquivalence.mk
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsStack J
S : C
R : Sieve.{v, u} S
hR : R ∈ (J : (a : C) → Set (Sieve a)) S
hF :
  Functor.FullyFaithful (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
this_1 :
  Functor.Full (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
this_2 :
  Functor.Faithful (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
this :
  Functor.EssSurj (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)

Tactic:
exact { }
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsStack J
S : C
R : Presieve.{v, u} S
hR : Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) S
⊢ F.IsStackFor R

Tactic:
simpa using F.isStackFor' _ hR

Premises used: CategoryTheory.Pseudofunctor.isStackFor'
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsStack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
rw : F.IsStackFor (Sieve.generate (Presieve.ofArrows X f)).arrows
⊢ (F.toDescentData f).IsEquivalence

Tactic:
rw [← isStackFor_ofArrows_iff, ← IsStackFor_generate_iff]

Premises used: CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, CategoryTheory.Pseudofunctor.IsStackFor_generate_iff
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsStack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
⊢ Sieve.generate (Sieve.generate (Presieve.ofArrows X f)).arrows ∈ (J : (a : C) → Set (Sieve a)) S

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsStack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
⊢ F.IsStackFor (Sieve.generate (Presieve.ofArrows X f)).arrows

Tactic:
exact F.isStackFor _ (by simpa)

Premises used: CategoryTheory.Pseudofunctor.isStackFor
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
hF : ∀ (S : C), ∀ R ∈ (J : (a : C) → Set (Sieve a)) S, F.IsStackFor R.arrows
S : C
R : Sieve.{v, u} S
hR : R ∈ (J : (a : C) → Set (Sieve a)) S
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)

Tactic:
have := (isStackFor_iff _ _).1 (hF _ _ hR)
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
hF : ∀ (S : C), ∀ R ∈ (J : (a : C) → Set (Sieve a)) S, F.IsStackFor R.arrows
S : C
R : Sieve.{v, u} S
hR : R ∈ (J : (a : C) → Set (Sieve a)) S
this :
  Functor.IsEquivalence (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)
⊢ Functor.EssSurj (C := (↑(F.obj { as := Opposite.op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    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)
    (F.toDescentData fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R.arrows f.hom).hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
h : ∀ (i : ι), φ.hom i = φ'.hom i
⊢ φ = φ'

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
⊢ φ.hom i = φ'.hom i

Tactic:
F.presheafHomObjHomEquiv.injective ?_i

Premises used: Equiv.injective, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
_i :
  Eq (α := (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
    ((F.presheafHomObjHomEquiv :
          (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
        (φ.hom i) :
      (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
    ((F.presheafHomObjHomEquiv :
          (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
        (φ'.hom i) :
      (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
⊢ φ.hom i = φ'.hom i

Tactic:
refine F.presheafHomObjHomEquiv.injective ?_i
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
⊢ Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))

Tactic:
simpa only [J.mem_over_iff, Equiv.apply_symm_apply] using J.pullback_stable (f i) hf'

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
⊢ Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))

Tactic:
have : (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm
      (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈ J.over (X i) _ := by
      simpa only [J.mem_over_iff, Equiv.apply_symm_apply] using J.pullback_stable (f i) hf'
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
⊢ Eq (α := (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
    ((F.presheafHomObjHomEquiv :
          (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
        (φ.hom i) :
      (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
    ((F.presheafHomObjHomEquiv :
          (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
        (φ'.hom i) :
      (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))

Tactic:
(((isSheaf_iff_isSheaf_of_type _ _).1
      (IsPrestack.isSheaf _ _ _)).isSeparated _ this).ext ?_

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Pseudofunctor.IsPrestack.isSheaf, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
Y : C
j : ι'
p : Z.left ⟶ X' j
hp : p ≫ f' j = Over.Hom.left g ≫ f i
⊢ Over.Hom.left g = Z.hom

Tactic:
simpa using Over.w g

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
Y : C
j : ι'
p : Z.left ⟶ X' j
hp : p ≫ f' j = Over.Hom.left g ≫ f i
⊢ Over.Hom.left g = Z.hom

Tactic:
have : g.left = Z.hom := by simpa using Over.w g
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this_1 :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
Y : C
j : ι'
p : Z.left ⟶ X' j
hp : p ≫ f' j = Over.Hom.left g ≫ f i
this : Over.Hom.left g = Z.hom
ψ : D₁ ⟶ D₂
obtain :
  ∀ (hp : p ≫ f' j = Over.Hom.left (Over.homMk Z.hom ⋯) ≫ f i) (this : Over.Hom.left (Over.homMk Z.hom ⋯) = Z.hom),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Quiver.Hom.op (Over.homMk Z.hom ⋯))) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        ((F.presheafHomObjHomEquiv :
              (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
            (ψ.hom i) :
          (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i))))) =
      D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
        pullHom (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (ψ.hom (α j))) p (p ≫ p' j) (p ≫ p' j) ⋯ ⋯ ≫
          D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op) :
        (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))) →
          (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((F.presheafHomObjHomEquiv :
            (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
          (ψ.hom i) :
        (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i))))) =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
      pullHom (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (ψ.hom (α j))) p (p ≫ p' j) (p ≫ p' j) ⋯ ⋯ ≫
        D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯

Tactic:
obtain rfl : g = Over.homMk Z.hom := by cat_disch

Premises used: CategoryTheory.Over.homMk, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this_1 :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
Z : Over.{v, u} (X i)
Y : C
j : ι'
p : Z.left ⟶ X' j
ψ : D₁ ⟶ D₂
hp : p ≫ f' j = Over.Hom.left (Over.homMk Z.hom ⋯) ≫ f i
this : Over.Hom.left (Over.homMk Z.hom ⋯) = Z.hom
⊢ (p ≫ p' j) ≫ f (α j) = Z.hom ≫ f i

Tactic:
grind