awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
hf₄ : (sq i₂ i₃).p₂ ≫ f i₃ = (sq i₂ i₃).p
hgf₃ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₂
hgf₄ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₂ : (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p = (sq₃ i₁ i₂ i₃).p
hf₅ : (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p
hf₆ : (sq i₁ i₂).p₂ ≫ f i₂ = (sq i₁ i₂).p
hgf₅ : (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p₁ = (sq₃ i₁ i₂ i₃).p₁
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hgf₆ : (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p₂ = (sq₃ i₁ i₂ i₃).p₂
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ pullHom' (ofDescentData sq sq₃ D).hom q f₁ f₂ hf₁ hf₂ = D.hom q f₁ f₂ hf₁ hf₂
have obtain : ∀ (p : Y ⟶ (sq i₁ i₂).pullback) (h₁ : p ≫ (sq i₁ i₂).p₁ = f₁) (h₂ : p ≫ (sq i₁ i₂).p₂ = f₂),
  pullHom' (ofDescentData sq sq₃ D).hom q f₁ f₂ hf₁ hf₂ = D.hom q f₁ f₂ hf₁ hf₂
Tactic: obtain ⟨p, h₁, h₂⟩ := (sq i₁ i₂).isPullback.exists_lift f₁ f₂ (by cat_disch)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ pullHom' (ofDescentData sq sq₃ D).hom q f₁ f₂ hf₁ hf₂ = D.hom q f₁ f₂ hf₁ hf₂
have rw : pullHom ((ofDescentData sq sq₃ D).hom i₁ i₂) p f₁ f₂ sorry sorry = D.hom q f₁ f₂ hf₁ hf₂
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ pullHom ((ofDescentData sq sq₃ D).hom i₁ i₂) p f₁ f₂ ⋯ ⋯ = D.hom q f₁ f₂ hf₁ hf₂
have dsimp : pullHom (D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ sorry sorry) p f₁ f₂ sorry sorry = D.hom q f₁ f₂ hf₁ hf₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ p ≫ (sq i₁ i₂).p = q
have rw : p ≫ (sq i₁ i₂).p₁ ≫ f i₁ = q
Tactic: rw [← (sq i₁ i₂).hp₁, reassoc_of% h₁, hf₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
rw : p ≫ (sq i₁ i₂).p₁ ≫ f i₁ = q
rw₁ : f₁ ≫ f i₁ = q
⊢ p ≫ (sq i₁ i₂).p = q
have rw₂ : q = q
Tactic: rw [← (sq i₁ i₂).hp₁, reassoc_of% h₁, hf₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ pullHom (D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) p f₁ f₂ ⋯ ⋯ = D.hom q f₁ f₂ hf₁ hf₂
have rw : D.hom q f₁ f₂ sorry sorry = D.hom q f₁ f₂ hf₁ hf₂
Tactic: rw [D.pullHom_hom _ _ _ (by rw [← (sq i₁ i₂).hp₁, reassoc_of% h₁, hf₁]) _ _
    (by simp) (by simp) _ _ h₁ h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsPrestack (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : (↑(F.obj { as := op X₁ : LocallyDiscrete Cᵒᵖ }) : Type u')
M₂ : (↑(F.obj { as := op X₂ : LocallyDiscrete Cᵒᵖ }) : Type u')
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ :
  Quiver.Hom (V := (↑(F.obj { as := op Y : LocallyDiscrete Cᵒᵖ }) : Type u'))
    (Functor.obj (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) M₁) (Functor.obj (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) M₂)
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ pullHom (pullHom φ g gf₁ gf₂ hgf₁ hgf₂) g' g'f₁ g'f₂ hg'f₁ hg'f₂ = pullHom φ (g' ≫ g) g'f₁ g'f₂ ⋯ ⋯
have dsimp : (F.mapComp' gf₁.op.toLoc g'.op.toLoc g'f₁.op.toLoc sorry).hom.toNatTrans.app M₁ ≫
    Functor.map (Cat.Hom.toFunctor (F.map g'.op.toLoc))
        ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc sorry).hom.toNatTrans.app M₁ ≫
          Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc)) φ ≫
            (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc sorry).inv.toNatTrans.app M₂) ≫
      (F.mapComp' gf₂.op.toLoc g'.op.toLoc g'f₂.op.toLoc sorry).inv.toNatTrans.app M₂ =
  (F.mapComp' f₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y' : LocallyDiscrete Cᵒᵖ }) g.op.toLoc g'.op.toLoc)
              g'f₁.op.toLoc sorry).hom.toNatTrans.app
      M₁ ≫
    Functor.map (Cat.Hom.toFunctor (F.map (CategoryStruct.comp (Y := { as := op Y' }) g.op.toLoc g'.op.toLoc))) φ ≫
      (F.mapComp' f₂.op.toLoc (CategoryStruct.comp (Y := { as := op Y' : LocallyDiscrete Cᵒᵖ }) g.op.toLoc g'.op.toLoc)
                g'f₂.op.toLoc sorry).inv.toNatTrans.app
        M₂
Tactic: dsimp [pullHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsStack (goal)
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
⊢ F.IsStackFor R.arrows
have rw : 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: rw [isStackFor_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsStack (goal)
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
⊢ 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)
have have : ∀
  (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)),
  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 hF := (F.isPrestackFor' _ hR).fullyFaithful
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsStack (hypothesis)
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)
⊢ 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)
have this : 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)
Tactic: have := hF.full
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsStack (hypothesis)
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 :
  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)
⊢ 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)
have 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)
Tactic: have := hF.faithful
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsStack (hypothesis)
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.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)
have 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)
Tactic: have := IsStack.essSurj_of_sieve F _ hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsStack (goal)
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.toDescentData f).IsEquivalence
have rw : F.IsStackFor (Sieve.generate (Presieve.ofArrows X f)).arrows
Tactic: rw [← isStackFor_ofArrows_iff, ← IsStackFor_generate_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.IsStack (hypothesis)
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.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)
have 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)
Tactic: have := (isStackFor_iff _ _).1 (hF _ _ hR)
-- 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 φ'
⊢ φ = φ'
have h : ∀ (i : ι), φ.hom i = φ'.hom i
Tactic: ext 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
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
⊢ φ.hom i = φ'.hom i
have _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: refine F.presheafHomObjHomEquiv.injective ?_i
-- 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 : ι
⊢ 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)))))
have 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))))
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'