awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
⊢ p ≫ (sq i i).p = f i

Tactic:
have : p ≫ (sq i i).p = f i := by rw [← (sq i i).hp₁, reassoc_of% h₁]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
rw : 𝟙 (X i) ≫ f i = f i
hq : p ≫ (sq i i).p = f i
hf₁ : (sq i i).p₁ ≫ f i = (sq i i).p
hf₂ : (sq i i).p₂ ≫ f i = (sq i i).p
hgf₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
hgf₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i))
      (𝟙 (X i)) ⋯ ⋯)
    (𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))

Tactic:
rw [pullHom'_eq_pullHom _ _ _ _ p, D.pullHom_hom _ _ (f i), D.hom_self (f i) (𝟙 _)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Pseudofunctor.DescentData.pullHom_hom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom, CategoryTheory.Pseudofunctor.DescentData.hom_self
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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₁
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₃ ⋯ ⋯)

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]

Premises used: CategoryTheory.Limits.ChosenPullback₃.p₁₃, CategoryTheory.Limits.ChosenPullback₃.p₁₂, CategoryTheory.Pseudofunctor.DescentData.pullHom_hom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom, CategoryTheory.Limits.ChosenPullback₃.p₂₃, CategoryTheory.Pseudofunctor.DescentData.hom_comp, CategoryTheory.Limits.ChosenPullback₃.p
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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
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₂
⊢ 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)

Premises used: CategoryTheory.Limits.ChosenPullback.isPullback, CategoryTheory.IsPullback.exists_lift
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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 : pullHom ((ofDescentData sq sq₃ D).hom i₁ i₂) p f₁ f₂ ⋯ ⋯ = D.hom q f₁ f₂ hf₁ hf₂
⊢ pullHom' (ofDescentData sq sq₃ D).hom q f₁ f₂ hf₁ hf₂ = D.hom q f₁ f₂ hf₁ hf₂

Tactic:
rw [pullHom'_eq_pullHom _ _ _ _ p]

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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₂
dsimp : 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₂
⊢ pullHom ((ofDescentData sq sq₃ D).hom i₁ i₂) p f₁ f₂ ⋯ ⋯ = D.hom q f₁ f₂ hf₁ hf₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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
rw₂ rw₃ : q = q
⊢ p ≫ (sq i₁ i₂).p = q

Tactic:
rw [← (sq i₁ i₂).hp₁, reassoc_of% h₁, hf₁]

Premises used: CategoryTheory.Limits.ChosenPullback.hp₁
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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₂
⊢ (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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₂
⊢ (sq i₁ i₂).p₂ ≫ f i₂ = (sq i₁ i₂).p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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 rw₁ : D.hom q f₁ f₂ ⋯ ⋯ = D.hom q f₁ f₂ hf₁ hf₂
⊢ 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₂

Tactic:
rw [D.pullHom_hom _ _ _ (by rw [← (sq i₁ i₂).hp₁, reassoc_of% h₁, hf₁]) _ _
    (by simp) (by simp) _ _ h₁ h₂]

Premises used: CategoryTheory.Pseudofunctor.DescentData.pullHom_hom
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
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₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Eq.{v + 1} (α := { as := op X₁ : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y' })
    (CategoryStruct.comp (Y := { as := op Y }) f₁.op.toLoc g.op.toLoc) gf₁.op.toLoc

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
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₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Eq.{v + 1} (α := { as := op X₂ : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y' })
    (CategoryStruct.comp (Y := { as := op Y }) f₂.op.toLoc g.op.toLoc) gf₂.op.toLoc

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
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₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc)) φ =
    (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).inv.toNatTrans.app M₁ ≫
      pullHom φ g gf₁ gf₂ hgf₁ hgf₂ ≫ (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).hom.toNatTrans.app M₂

Tactic:
simp [Cat.Hom.comp_toFunctor, pullHom, ← reassoc_of% Cat.Hom₂.comp_app, ← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
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₂)
⊢ pullHom φ (𝟙 Y) f₁ f₂ ⋯ ⋯ = φ

Tactic:
simp [pullHom, mapComp'_comp_id_hom_app, mapComp'_comp_id_inv_app,
    ← reassoc_of% Cat.Hom₂.comp_app, Iso.inv_hom_id]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
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₂
dsimp :
  (F.mapComp' gf₁.op.toLoc g'.op.toLoc g'f₁.op.toLoc ⋯).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 ⋯).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 ⋯).inv.toNatTrans.app M₂) ≫
        (F.mapComp' gf₂.op.toLoc g'.op.toLoc g'f₂.op.toLoc ⋯).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 ⋯).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 ⋯).inv.toNatTrans.app
          M₂
⊢ pullHom (pullHom φ g gf₁ gf₂ hgf₁ hgf₂) g' g'f₁ g'f₂ hg'f₁ hg'f₂ = pullHom φ (g' ≫ g) g'f₁ g'f₂ ⋯ ⋯

Tactic:
dsimp [pullHom]

Premises used: CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
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₂
⊢ Eq.{v + 1} (α := { as := op X₂ : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y'' })
    (CategoryStruct.comp (Y := { as := op Y' }) gf₂.op.toLoc g'.op.toLoc) g'f₂.op.toLoc

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
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₂
⊢ Eq.{v + 1} (α := { as := op X₁ : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y'' })
    (CategoryStruct.comp (Y := { as := op Y' }) gf₁.op.toLoc g'.op.toLoc) g'f₁.op.toLoc

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
S' : C
q : S' ⟶ S
T : (Over.{v, u} S')ᵒᵖ
e : Iso (C :=
  Functor.{v', v', u', u'} (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
    (↑(F.obj { as := op (unop T).left : LocallyDiscrete Cᵒᵖ }) : Type u'))
  (Cat.Hom.toFunctor (F.map ((Over.map q).obj (unop T)).hom.op.toLoc))
  (Cat.Hom.toFunctor
    (CategoryStruct.comp (Y := F.obj { as := op S' }) (F.map q.op.toLoc) (F.map (unop T).hom.op.toLoc))) :=
  Cat.Hom.toNatIso (F.mapComp' q.op.toLoc (unop T).hom.op.toLoc ((Over.map q).obj (unop T)).hom.op.toLoc ⋯)
⊢ ((Over.map q).op ⋙ F.presheafHom M N).obj T ≃
    Functor.obj
      (F.presheafHom (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) M)
        (Functor.obj (Cat.Hom.toFunctor (F.map q.op.toLoc)) N))
      T

Tactic:
exact (Iso.homFromEquiv (e.app M)).trans (Iso.homToEquiv (e.app N))

Premises used: CategoryTheory.Iso.homToEquiv, Equiv.trans, CategoryTheory.Iso.app, CategoryTheory.Iso.homFromEquiv
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
S' : C
q : S' ⟶ S
T₁ T₂ : Over.{v, u} S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op T₂.left })
    (CategoryStruct.comp (Y := { as := op T₁.left })
      (CategoryStruct.comp (Y := { as := op S' }) q.op.toLoc T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc)
    (CategoryStruct.comp (Y := { as := op S' }) q.op.toLoc T₂.hom.op.toLoc)

Tactic:
simp only [← Quiver.Hom.comp_toLoc, ← op_comp, Over.w_assoc]

Premises used: CategoryTheory.op_comp, Quiver.Hom.comp_toLoc, CategoryTheory.Over.w_assoc
-- Module: Mathlib.CategoryTheory.Sites.Descent.IsStack
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsStack J
S : C
R : Sieve.{v, u} S
hR : R ∈ (J : (a : C) → Set (Sieve a)) S
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)
⊢ F.IsStackFor R.arrows

Tactic:
rw [isStackFor_iff]

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