awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
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
dsimp :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₁) : LocallyDiscrete Cᵒᵖ }))) (D.obj i₁)) ≫
      D.hom q f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom ⋯ D (f₁ ≫ f i₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₂) }))) (D.obj i₂))
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Iso.hom
          ((fun (i : ι) ↦
              (Iso.app (Cat.Hom.toNatIso (F.mapId { as := op (X ((fun (x : ι) ↦ x) i)) }))
                  (D.obj ((fun (x : ι) ↦ x) i)) :
                (F.map (𝟙 { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ })).toFunctor.obj
                    (D.obj ((fun (x : ι) ↦ x) i)) ≅
                  (Cat.Hom.toFunctor (𝟙 (F.obj { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ }))).obj
                    (D.obj ((fun (x : ι) ↦ x) i))))
            i₁)) ≫
      (Functor.obj (𝟭 (F.DescentData f)) D).hom q f₁ f₂ ⋯ ⋯ =
    (Functor.obj (pullFunctor F ⋯) D).hom q f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Iso.hom
          ((fun (i : ι) ↦
              (Iso.app (Cat.Hom.toNatIso (F.mapId { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ }))
                  (D.obj ((fun (x : ι) ↦ x) i)) :
                (F.map (𝟙 { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ })).toFunctor.obj
                    (D.obj ((fun (x : ι) ↦ x) i)) ≅
                  (Cat.Hom.toFunctor (𝟙 (F.obj { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ }))).obj
                    (D.obj ((fun (x : ι) ↦ x) i))))
            i₂))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
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
rw :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₁) : LocallyDiscrete Cᵒᵖ }))) (D.obj i₁)) ≫
      D.hom q f₁ f₂ ⋯ ⋯ =
    NatTrans.app
        (Cat.Hom₂.toNatTrans
          (Iso.inv (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i₁)))) f₁.op.toLoc f₁.op.toLoc ⋯)))
        (D.obj i₁) ≫
      D.hom q f₁ f₂ ⋯ ⋯ ≫
        NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.hom (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i₂)))) f₂.op.toLoc f₂.op.toLoc ⋯)))
            (D.obj i₂) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
            (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₂) : LocallyDiscrete Cᵒᵖ })))
              (D.obj i₂))
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₁) : LocallyDiscrete Cᵒᵖ }))) (D.obj i₁)) ≫
      D.hom q f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom ⋯ D (f₁ ≫ f i₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₂) }))) (D.obj i₂))

Tactic:
rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ q f₁ f₂ rfl]

Premises used: CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
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
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₁) : LocallyDiscrete Cᵒᵖ }))) (D.obj i₁)) ≫
      D.hom q f₁ f₂ ⋯ ⋯ =
    NatTrans.app
        (Cat.Hom₂.toNatTrans
          (Iso.inv (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i₁)))) f₁.op.toLoc f₁.op.toLoc ⋯)))
        (D.obj i₁) ≫
      D.hom q f₁ f₂ ⋯ ⋯ ≫
        NatTrans.app
            (Cat.Hom₂.toNatTrans
              (Iso.hom (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i₂)))) f₂.op.toLoc f₂.op.toLoc ⋯)))
            (D.obj i₂) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
            (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₂) : LocallyDiscrete Cᵒᵖ })))
              (D.obj i₂))

Tactic:
simp [mapComp'_id_comp_inv_app_assoc, mapComp'_id_comp_hom_app, ← Functor.map_comp]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_2
k : ι''
dsimp : r' k ≫ f (α (β k)) = f'' k ≫ r
⊢ r' k ≫ f ((α ∘ β) k) = f'' k ≫ r

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_2
k : ι''
rw : (q' k ≫ p' (β k)) ≫ f (α (β k)) = f'' k ≫ r
rw₁ : q' k ≫ p' (β k) ≫ f (α (β k)) = f'' k ≫ r
rw₂ : q' k ≫ f' (β k) ≫ p = f'' k ≫ r
rw₃ : f'' k ≫ q ≫ p = f'' k ≫ r
rw₄ rw₅ : f'' k ≫ r = f'' k ≫ r
⊢ r' k ≫ f (α (β k)) = f'' k ≫ r

Tactic:
rw [← hr', Category.assoc, w, reassoc_of% w', hr]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
x : ι''
⊢ Eq.{v + 1} (α := { as := op (X (α (β x))) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op (X'' x) })
    (CategoryStruct.comp (Y := { as := op (X' (β x)) }) (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β x)))) (q' x).op.toLoc)
    (r' x).op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
rw :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₁)))) (q' k₁).op.toLoc (r' k₁).op.toLoc
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁)))) ≫
      (F.mapComp' (r' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj ((α ∘ β) k₁)) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (r' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ r' k₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj ((α ∘ β) k₂)) =
    ((F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ q' k₁).op.toLoc ⋯).inv.toNatTrans.app
          ((pullFunctorObj w D).obj (β k₁)) ≫
        (pullFunctorObj w D).hom (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂) ⋯ ⋯ ≫
          (F.mapComp' (q' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ q' k₂).op.toLoc ⋯).hom.toNatTrans.app
            ((pullFunctorObj w D).obj (β k₂))) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₂)))) (q' k₂).op.toLoc (r' k₂).op.toLoc
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₂))))
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₁)))) (q' k₁).op.toLoc (r' k₁).op.toLoc
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁)))) ≫
      pullFunctorObjHom (p := r) ⋯ D (f₁ ≫ f'' k₁) f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom w' (pullFunctorObj w D) (f₁ ≫ f'' k₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₂)))) (q' k₂).op.toLoc (r' k₂).op.toLoc
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₂))))

Tactic:
rw [pullFunctorObjHom_eq _ _ _ _ _ (s ≫ r) _ _ rfl,
        pullFunctorObjHom_eq _ _ _ _ _ (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂)]

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (f₂ ≫ q' k₂) ≫ f' (β k₂) = (f₁ ≫ q' k₁) ≫ f' (β k₁)

Tactic:
simp [w', reassoc_of% hf₁, reassoc_of% hf₂]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ ((f₁ ≫ q' k₁) ≫ f' (β k₁)) ≫ p = s ≫ r

Tactic:
simp [reassoc_of% w', reassoc_of% hf₁, hr]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ Eq.{v + 1} (α := { as := op (X (α (β k₁))) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op (X'' k₁) })
    (CategoryStruct.comp (Y := { as := op (X' (β k₁)) }) (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₁))))
      (q' k₁).op.toLoc)
    (r' k₁).op.toLoc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ (p' j ≫ q' (α j)) ≫ f' (β (α j)) = p' j ≫ q' (α j) ≫ f' (β (α j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ 𝟙 (X' j) ≫ f' j = p' j ≫ q' (α j) ≫ f' (β (α j))

Tactic:
simp [w', reassoc_of% w]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ 𝟙 (X (α j)) = p' j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ q' (α j) ≫ p' (β (α j)) = p' j ≫ q' (α j) ≫ p' (β (α j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ f (α j) = p' j ≫ f (α j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ 𝟙 (X (α j)) ≫ f (α j) = f (α j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ Eq.{v + 1} (α := X (α j) ⟶ S) ((q' (α j) ≫ p' (β (α j))) ≫ f (α (β (α j)))) (f (α j))

Tactic:
simp [w, reassoc_of% w']
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ Eq.{v + 1} (α := { as := op (X (α (β (α j)))) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op (X' j) })
    (CategoryStruct.comp (Y := { as := op (X' (β (α j))) }) (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))
      (CategoryStruct.comp (Y := { as := op (X (α j)) }) (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))) (p' j).op.toLoc))
    (CategoryStruct.comp (Y := { as := op (X (α j)) })
      (CategoryStruct.comp (Y := { as := op (X' (β (α j))) }) (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β (α j)))))
        (Quiver.Hom.toLoc (Quiver.Hom.op (q' (α j)))))
      (p' j).op.toLoc)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc _ _ _ _ _ _ rfl rfl (by simp),
      mapComp'_comp_id_hom_app, mapComp'_id_comp_inv_app_assoc, ← Functor.map_comp_assoc,
      Cat.Hom.inv_hom_id_toNatTrans_app]

Premises used: CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [D.hom_self _ _ rfl]

Premises used: CategoryTheory.Pseudofunctor.DescentData.hom_self, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
rw : (Sieve.ofArrows X' f').arrows (f' i')
⊢ (Sieve.ofArrows X f).arrows (f' i')

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
⊢ (Sieve.ofArrows X' f').arrows (f' i')

Tactic:
apply Sieve.ofArrows_mk

Premises used: CategoryTheory.Sieve.ofArrows_mk
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
obtain : ∀ ⦃Y : C⦄ (i : ι) (w : X' i' ⟶ X i) (fac : w ≫ f i = f' i'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
⊢ ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'

Tactic:
obtain ⟨_, _, _, ⟨i⟩, fac⟩ : Sieve.ofArrows X f (f' i') := by
      rw [h]; apply Sieve.ofArrows_mk

Premises used: CategoryTheory.Sieve.ofArrows, CategoryTheory.Sieve.arrows
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
Y : C
i : ι
w : X' i' ⟶ X i
fac : w ≫ f i = f' i'
⊢ ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'

Tactic:
⟨i, _, fac⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
Y : C
i : ι
w : X' i' ⟶ X i
fac : w ≫ f i = f' i'
⊢ ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'

Tactic:
exact ⟨i, _, fac⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
⊢ ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'

Tactic:
have h₁ (i' : ι') : ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i' := by
    obtain ⟨_, _, _, ⟨i⟩, fac⟩ : Sieve.ofArrows X f (f' i') := by
      rw [h]; apply Sieve.ofArrows_mk
    exact ⟨i, _, fac⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
i : ι
rw : (Sieve.ofArrows X f).arrows (f i)
⊢ (Sieve.ofArrows X' f').arrows (f i)

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
i : ι
⊢ (Sieve.ofArrows X f).arrows (f i)

Tactic:
apply Sieve.ofArrows_mk

Premises used: CategoryTheory.Sieve.ofArrows_mk