awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
φ φ' : 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
⊢ 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 (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))))) :
      (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 (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))))) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
have this₁ : Over.Hom.left g = Z.hom
Tactic: have : g.left = Z.hom := by simpa using Over.w g
-- 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
φ φ' : 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₂
⊢ (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 ⋯ ⋯
have obtain : ∀ (hp : p ≫ f' j = Over.Hom.left (Over.homMk Z.hom sorry) ≫ f i) (this : Over.Hom.left (Over.homMk Z.hom sorry) = Z.hom),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Quiver.Hom.op (Over.homMk Z.hom sorry))) :
        (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) sorry sorry ≫
      pullHom (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (ψ.hom (α j))) p (p ≫ p' j) (p ≫ p' j) sorry sorry ≫
        D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom sorry sorry
Tactic: obtain rfl : g = Over.homMk Z.hom := by cat_disch
Cleared hypotheses: g, hp, this
-- 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
φ φ' : 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
⊢ (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 ⋯ ⋯
have this₁ : Functor.map (Cat.Hom.toFunctor (F.map Z.hom.op.toLoc)) (ψ.hom i) ≫ D₂.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) sorry sorry =
  D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) sorry sorry ≫ Functor.map (Cat.Hom.toFunctor (F.map (p ≫ p' j).op.toLoc)) (ψ.hom (α j))
Tactic: have := ψ.comm _ Z.hom (p ≫ p' j) rfl (by grind)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
i : ι
Z : C
q : Z ⟶ X i
hq : (sieve f f' i).arrows (Y := Over.mk q) (Over.homMk q ⋯)
⊢ ∃ (j : ι') (a : Z ⟶ X' j), a ≫ f' j = q ≫ f i
have obtain : ∀ ⦃Y : C⦄ (j : ι') (q_1 : Functor.obj (Over.forget (X i)) (Over.mk q) ⟶ X' j)
  (fac : q_1 ≫ f' j = Functor.map (Over.forget (X i)) (Over.homMk q sorry) ≫ f i),
  ∃ (j : ι') (a : Z ⟶ X' j), a ≫ f' j = q ≫ f i
Tactic: obtain ⟨_, q, _, ⟨j⟩, fac⟩ := hq
Cleared hypotheses: hq
-- 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 : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
q' : Z ⟶ S
a' : Z ⟶ X (α j)
hq' : q ≫ f i = q'
ha' : a ≫ p' j = a'
⊢ mor w φ q a fac = D₁.hom q' q a' ⋯ ⋯ ≫ pullHom (φ.hom j) a a' a' ⋯ ⋯ ≫ D₂.hom q' a' q ⋯ ⋯
have subst : mor w φ q a fac =
  D₁.hom (q ≫ f i) q (a ≫ p' j) sorry sorry ≫ pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) sorry sorry ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q sorry sorry
Tactic: subst hq' ha'
Cleared hypotheses: q', a', hq', ha'
-- 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 : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
⊢ mor w φ r' a' ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Quiver.Hom.op (Over.homMk r ⋯))) :
        (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk q)))) →
          (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk r'))))
      (mor w φ q a fac)
have dsimp : mor w φ r' a' sorry = pullHom (mor w φ q a fac) r r' r' sorry sorry
Tactic: dsimp
-- 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 : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
⊢ mor w φ r' a' ⋯ = pullHom (mor w φ q a fac) r r' r' ⋯ ⋯
have rw : pullHom (D₁.hom (q ≫ f i) q (a ≫ p' j) sorry sorry) r r' (r ≫ a ≫ p' j) sorry sorry ≫
    pullHom (φ.hom j) a' (r ≫ a ≫ p' j) (r ≫ a ≫ p' j) sorry sorry ≫
      pullHom (D₂.hom (q ≫ f i) (a ≫ p' j) q sorry sorry) r (r ≫ a ≫ p' j) r' sorry sorry =
  pullHom
    (D₁.hom (q ≫ f i) q (a ≫ p' j) sorry sorry ≫
      pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) sorry sorry ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q sorry sorry)
    r r' r' sorry sorry
Tactic: rw [mor_eq _ _ _ _ _ (r ≫ q ≫ f i) (r ≫ a ≫ p' j),
    mor_eq _ _ _ _ _ _ _ rfl rfl,
    ← D₁.pullHom_hom r (q ≫ f i) _ rfl q (a ≫ p' j) rfl (by cat_disch) r' _ hr' rfl,
    ← D₂.pullHom_hom r (q ≫ f i) _ rfl (a ≫ p' j) q (by cat_disch) rfl _ r' rfl hr']
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
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 : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂
have this : Functor.map (Cat.Hom.toFunctor (F.map a₁.op.toLoc)) (φ.hom j₁) ≫
    hom (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₂) (q ≫ f i) a₁ a₂ sorry sorry =
  hom (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') sorry) D₁) (q ≫ f i) a₁ a₂ sorry sorry ≫
    Functor.map (Cat.Hom.toFunctor (F.map a₂.op.toLoc)) (φ.hom j₂)
Tactic: have := φ.comm (q ≫ f i) a₁ a₂ fac₁ fac₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
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 : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  Functor.map (Cat.Hom.toFunctor (F.map a₁.op.toLoc)) (φ.hom j₁) ≫
      pullFunctorObjHom (p := 𝟙 S) ⋯ D₂ (a₁ ≫ f' j₁) a₁ a₂ ⋯ ⋯ =
    pullFunctorObjHom (p := 𝟙 S) ⋯ D₁ (a₁ ≫ f' j₁) a₁ a₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map a₂.op.toLoc)) (φ.hom j₂)
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂
have this₁ : ((F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc sorry).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) sorry sorry ≫
        (F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc sorry).hom.toNatTrans.app (D₂.obj (α j₁))) ≫
    (F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc sorry).inv.toNatTrans.app (D₂.obj (α j₁)) ≫
      D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) sorry sorry ≫
        (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc sorry).hom.toNatTrans.app (D₂.obj (α j₂)) =
  ((F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc sorry).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) sorry sorry ≫
        (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc sorry).hom.toNatTrans.app (D₁.obj (α j₂))) ≫
    (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc sorry).inv.toNatTrans.app (D₁.obj (α j₂)) ≫
      pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) sorry sorry ≫
        (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc sorry).hom.toNatTrans.app (D₂.obj (α j₂))
Tactic: rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) rfl,
    pullFunctorObjHom_eq _ _ _ _ _ (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) rfl,
    map_eq_pullHom _ _ _ _ (by exact rfl) rfl, map_eq_pullHom _ _ _ _ rfl rfl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
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 : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc a₂.op.toLoc)
                  ⋯).hom.toNatTrans.app
          (D₂.obj (α j₂)) =
    D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
      pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op (X' j₂) }) (p' j₂).op.toLoc a₂.op.toLoc) ⋯).hom.toNatTrans.app
          (D₂.obj (α j₂))
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂
have this₁ : pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) sorry sorry ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) sorry sorry =
  D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) sorry sorry ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) sorry sorry
Tactic: simp only [← Category.assoc, cancel_mono] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
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 : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂
have this₁ : pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) sorry sorry ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q sorry sorry =
  (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) sorry sorry ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) sorry sorry) ≫
    D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q sorry sorry
Tactic: rw [← cancel_mono (D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q), Category.assoc,
    D₂.hom_comp] at this
Cleared hypotheses: this
-- 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 : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂
have rw : D₁.hom (q ≫ f i) q (a₁ ≫ p' j₁) sorry sorry ≫
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) sorry sorry ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) sorry sorry) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q sorry sorry =
  D₁.hom (q ≫ f i) q (a₂ ≫ p' j₂) sorry sorry ≫
    pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) sorry sorry ≫ D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q sorry sorry
Tactic: rw [mor_eq _ _ _ _ _ _ _ rfl rfl, mor_eq _ _ _ _ _ _ _ rfl rfl, this]
-- 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₂)
i : ι
Z : Over.{v, u} (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
⊢ (sieve f f' i).arrows (Y := Over.mk Z.hom) (Over.homMk Z.hom ⋯)
have h : Over.mk Z.hom = Z → Over.homMk Z.hom sorry = q
Tactic: convert! hq
-- 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₂)
i : ι
Z : Over.{v, u} (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
e_5 : Over.mk Z.hom = Z
⊢ Over.homMk Z.hom ⋯ = q
have h : Over.Hom.left (Over.homMk Z.hom sorry) = Over.Hom.left q
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
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 : ι
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
⊢ g = Over.homMk Z.hom ⋯
have h : Over.Hom.left g = Over.Hom.left (Over.homMk Z.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
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 : ι
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
⊢ (sieve f f' i).arrows g
have rw : (sieve f f' i).arrows (Y := Z) (Over.homMk Z.hom sorry)
Tactic: rw [show g = Over.homMk Z.hom by ext; simpa using Over.w g]