awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : 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
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₂ : Z ⟶ Y₂
h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom ⋯)
h₂ : (sieve f f' i).arrows (Y := Y₂) (Over.homMk Y₂.hom ⋯)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯) (g₂ ≫ Over.homMk Y₂.hom ⋯)
obtain :
  ∀ (g₂ : Z.left ⟶ Y₂.left) (hg₂ : g₂ ≫ Y₂.hom = Z.hom)
    (fac :
      Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯) (Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯)),
    Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₁ ⋯).op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) h₁) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₂ ⋯).op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) h₂) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₁ ⋯).op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) h₁) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((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 Y₂))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))

Tactic:
obtain ⟨g₂, hg₂, rfl⟩ := Over.homMk_surjective g₂

Premises used: CategoryTheory.Over.homMk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : 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
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
h₂ : (sieve f f' i).arrows (Y := Y₂) (Over.homMk Y₂.hom ⋯)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯) (Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯)
Y : C
j₁ : ι'
a₁ : Functor.obj (Over.forget (X i)) Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = Functor.map (Over.forget (X i)) (Over.homMk Y₁.hom ⋯) ≫ f i
obtain :
  ∀ ⦃Y : C⦄ (j₂ : ι') (a₂ : Functor.obj (Over.forget (X i)) Y₂ ⟶ X' j₂)
    (fac₂ : a₂ ≫ f' j₂ = Functor.map (Over.forget (X i)) (Over.homMk Y₂.hom ⋯) ≫ f i),
    Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₁ ⋯).op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) ⋯) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₂ ⋯).op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) ⋯) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₁ ⋯).op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) ⋯) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₂ ⋯).op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))

Tactic:
obtain ⟨_, a₂, _, ⟨j₂⟩, fac₂⟩ := h₂
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : 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
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯) (Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯)
Y_1 : C
j₁ : ι'
a₁ : Functor.obj (Over.forget (X i)) Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = Functor.map (Over.forget (X i)) (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : Functor.obj (Over.forget (X i)) Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = Functor.map (Over.forget (X i)) (Over.homMk Y₂.hom ⋯) ≫ f i
dsimp :
  pullHom (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) ⋯) g₁ Z.hom Z.hom ⋯ ⋯ =
    pullHom (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) ⋯) g₂ Z.hom Z.hom ⋯ ⋯
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₁ ⋯).op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) ⋯) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₂ ⋯).op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) ⋯) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))

Tactic:
dsimp at *
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : 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
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯) (Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯)
Y_1 : C
j₁ : ι'
a₁ : Functor.obj (Over.forget (X i)) Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = Functor.map (Over.forget (X i)) (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : Functor.obj (Over.forget (X i)) Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = Functor.map (Over.forget (X i)) (Over.homMk Y₂.hom ⋯) ≫ f i
rw : mor w φ Z.hom (g₁ ≫ a₁) ⋯ = mor w φ Z.hom (g₂ ≫ a₂) ⋯
⊢ pullHom (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) ⋯) g₁ Z.hom Z.hom ⋯ ⋯ =
    pullHom (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) ⋯) g₂ Z.hom Z.hom ⋯ ⋯

Tactic:
rw [familyOfElements_eq _ _ _ _ fac₁, familyOfElements_eq _ _ _ _ fac₂,
    ← dsimp% mor_precomp w φ Y₁.hom a₁ fac₁ _ _ _ hg₁ rfl,
    ← dsimp% mor_precomp w φ Y₂.hom a₂ fac₂ _ _ _ hg₂ rfl]

Premises used: _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_precomp, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements_eq, CategoryTheory.Over.hom, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : 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
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯) (Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯)
Y_1 : C
j₁ : ι'
a₁ : Functor.obj (Over.forget (X i)) Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = Functor.map (Over.forget (X i)) (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : Functor.obj (Over.forget (X i)) Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = Functor.map (Over.forget (X i)) (Over.homMk Y₂.hom ⋯) ≫ f i
⊢ mor w φ Z.hom (g₁ ≫ a₁) ⋯ = mor w φ Z.hom (g₂ ≫ a₂) ⋯

Tactic:
apply mor_unique

Premises used: _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_unique
-- 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
⊢ Membership.mem (γ := 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)))) (Sieve.generate (sieve f f' i).arrows)

Tactic:
simpa using sieve_mem _ hf' i

Premises used: _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve_mem
-- 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y : C
q : Y ⟶ X i
j : ι'
a : Y ⟶ X' j
fac : a ≫ f' j = q ≫ f i
⊢ Membership.mem (γ := 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)))) (Sieve.generate (sieve f f' i).arrows)

Tactic:
simpa using sieve_mem _ hf' i

Premises used: _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve_mem
-- 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y : C
q : Y ⟶ X i
j : ι'
a : Y ⟶ X' j
fac : a ≫ f' j = q ≫ f i
s : (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))) :=
  ⋯.amalgamate (R := (sieve f f' i).arrows) (familyOfElements w φ i) ⋯
⊢ Membership.mem (γ := 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)))) (Sieve.generate (sieve f f' i).arrows)

Tactic:
simpa using sieve_mem _ hf' i

Premises used: _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve_mem
-- 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y : C
q : Y ⟶ X i
j : ι'
a : Y ⟶ X' j
fac : a ≫ f' j = q ≫ f i
s : (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))) :=
  ⋯.amalgamate (R := (sieve f f' i).arrows) (familyOfElements w φ i) ⋯
⊢ (familyOfElements w φ i).IsAmalgamation (R := (sieve f f' i).arrows) s

Tactic:
have hs : (familyOfElements w φ i).IsAmalgamation s :=
    Presieve.IsSheafFor.isAmalgamation
      (((isSheaf_iff_isSheaf_of_type _ _).1 (IsPrestack.isSheaf J _ _)).isSheafFor _
        (by simpa using sieve_mem _ hf' i)) (compatible_familyOfElements w φ 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y : C
q : Y ⟶ X i
j : ι'
a : Y ⟶ X' j
fac : a ≫ f' j = q ≫ f i
s : (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))) :=
  ⋯.amalgamate (R := (sieve f f' i).arrows) (familyOfElements w φ i) ⋯
hs : (familyOfElements w φ i).IsAmalgamation (R := (sieve f f' i).arrows) s
⊢ Functor.map (Cat.Hom.toFunctor (F.map q.op.toLoc)) (hom w hf' φ i) = mor w φ q a fac

Tactic:
simpa [hom, familyOfElements_eq w φ (Z := Over.mk q) _ a fac,
    presheafHomObjHomEquiv, pullHom, mapComp'_id_comp_hom_app,
    mapComp'_id_comp_inv_app] using hs _ (mem_sieve _ _ fac)

Premises used: _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mem_sieve, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements_eq, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
rw :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (hom w hf' φ i₁) =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (hom w hf' φ i₁) ≫ D₂.hom q f₁ f₂ ⋯ ⋯ =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (hom w hf' φ i₂)

Tactic:
rw [← cancel_mono (D₂.hom q f₂ f₁), Category.assoc,
    Category.assoc, DescentData.hom_comp, D₂.hom_self _ _ hf₁, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Pseudofunctor.DescentData.hom, CategoryTheory.Pseudofunctor.DescentData.hom_self, CategoryTheory.Pseudofunctor.DescentData.hom_comp
-- 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
rw :
  Membership.mem (γ := Set (Sieve.{v, u} (Over.mk f₁).left)) ((J : (a : C) → Set (Sieve a)) (Over.mk f₁).left)
    (Sieve.pullback q (Sieve.ofArrows X' f'))
⊢ Membership.mem (α := Sieve (Over.mk f₁)) (γ := Set (Sieve (Over.mk f₁)))
    ((J.over (X i₁) : (a : Over (X i₁)) → Set (Sieve a)) (Over.mk f₁))
    (((Sieve.overEquiv (Over.mk f₁)).symm : (a : Sieve (Over.mk f₁).left) → Sieve (Over.mk f₁))
        (Sieve.pullback q (Sieve.ofArrows X' f')) :
      Sieve (Over.mk f₁))

Tactic:
rw [J.mem_over_iff, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.mem_over_iff
-- 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Membership.mem (γ := Set (Sieve.{v, u} (Over.mk f₁).left)) ((J : (a : C) → Set (Sieve a)) (Over.mk f₁).left)
    (Sieve.pullback q (Sieve.ofArrows X' f'))

Tactic:
J.pullback_stable _ hf'

Premises used: 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Membership.mem (γ := Set (Sieve.{v, u} (Over.mk f₁).left)) ((J : (a : C) → Set (Sieve a)) (Over.mk f₁).left)
    (Sieve.pullback q (Sieve.ofArrows X' f'))

Tactic:
exact J.pullback_stable _ hf'

Premises used: 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Membership.mem (α := Sieve (Over.mk f₁)) (γ := Set (Sieve (Over.mk f₁)))
    ((J.over (X i₁) : (a : Over (X i₁)) → Set (Sieve a)) (Over.mk f₁))
    (((Sieve.overEquiv (Over.mk f₁)).symm : (a : Sieve (Over.mk f₁).left) → Sieve (Over.mk f₁))
        (Sieve.pullback q (Sieve.ofArrows X' f')) :
      Sieve (Over.mk f₁))

Tactic:
have H : (Sieve.overEquiv (Over.mk f₁)).symm
      (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ J.over _ _ := by
    rw [J.mem_over_iff, Equiv.apply_symm_apply]
    exact J.pullback_stable _ hf'