awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
h₂ : (sieve f f' i).arrows f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ f₁ = Over.homMk Y₁.hom ⋯
have h : Over.Hom.left f₁ = Over.Hom.left (Over.homMk Y₁.hom sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
h₂ : (sieve f f' i).arrows f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ 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 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 f₁ 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 f₂ h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
have obtain : ∀ (h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom sorry)) (fac : g₁ ≫ Over.homMk Y₁.hom sorry = g₂ ≫ f₂),
  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 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 sorry) 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 f₂ h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
Tactic: obtain rfl : f₁ = Over.homMk Y₁.hom := by ext; simpa using Over.w f₁
Cleared hypotheses: f₁, h₁, fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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₁
g₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₂ : (sieve f f' i).arrows f₂
h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom ⋯)
fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂
⊢ f₂ = Over.homMk Y₂.hom ⋯
have h : Over.Hom.left f₂ = Over.Hom.left (Over.homMk Y₂.hom sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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₁
g₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₂ : (sieve f f' i).arrows f₂
h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom ⋯)
fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂
⊢ 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 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 f₂ h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
have obtain : ∀ (h₂ : (sieve f f' i).arrows (Y := Y₂) (Over.homMk Y₂.hom sorry))
  (fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (g₁ ≫ Over.homMk Y₁.hom sorry) (g₂ ≫ Over.homMk Y₂.hom sorry)),
  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 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 sorry) 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 sorry) h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
Tactic: obtain rfl : f₂ = Over.homMk Y₂.hom := by ext; simpa using Over.w f₂
Cleared hypotheses: f₂, h₂, fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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₁
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 ⋯)
fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (g₁ ≫ Over.homMk Y₁.hom ⋯) (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 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)))
have obtain : ∀ (g₁ : Z.left ⟶ Y₁.left) (hg₁ : g₁ ≫ Y₁.hom = Z.hom)
  (fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ sorry ≫ Over.homMk Y₁.hom sorry) (g₂ ≫ Over.homMk Y₂.hom sorry)),
  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₁ sorry).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 sorry) 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 sorry) 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₁
Cleared hypotheses: g₁, fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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 ⋯)
⊢ 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)))
have obtain : ∀ (g₂ : Z.left ⟶ Y₂.left) (hg₂ : g₂ ≫ Y₂.hom = Z.hom)
  (fac :
    Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ sorry ≫ Over.homMk Y₁.hom sorry) (Over.homMk g₂ sorry ≫ Over.homMk Y₂.hom sorry)),
  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₁ sorry).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 sorry) 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₂ sorry).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 sorry) 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₂
Cleared hypotheses: g₂, fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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
⊢ 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)))
have 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 sorry) ≫ 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₁ sorry).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 sorry) sorry) :
      (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₂ sorry).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 sorry) sorry) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
Tactic: obtain ⟨_, a₂, _, ⟨j₂⟩, fac₂⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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
⊢ 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)))
have dsimp : pullHom (familyOfElements w φ i (Over.homMk Y₁.hom sorry) sorry) g₁ Z.hom Z.hom sorry sorry =
  pullHom (familyOfElements w φ i (Over.homMk Y₂.hom sorry) sorry) g₂ Z.hom Z.hom sorry sorry
Tactic: dsimp at *
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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
⊢ 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 ⋯ ⋯
have rw : mor w φ Z.hom (g₁ ≫ a₁) sorry = mor w φ Z.hom (g₂ ≫ a₂) sorry
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
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) ⋯
⊢ Functor.map (Cat.Hom.toFunctor (F.map q.op.toLoc)) (hom w hf' φ i) = mor w φ q a fac
have hs : (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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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
⊢ 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₂)
have rw : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (hom w hf' φ i₁) =
  D₁.hom q f₁ f₂ sorry sorry ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ sorry sorry
Tactic: rw [← cancel_mono (D₂.hom q f₂ f₁), Category.assoc,
    Category.assoc, DescentData.hom_comp, D₂.hom_self _ _ hf₁, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
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₁))
have 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'))
Tactic: rw [J.mem_over_iff, Equiv.apply_symm_apply]