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'
j : ι'
g : Y ⟶ X' j
hg : g ≫ f' j = q
rw :
  Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op Y : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map g.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j))))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map g.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j)))))
    ((F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j)) ≫
      𝟙
          (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (g ≫ p' j).op.toLoc)) (D.obj (α j))) ≫
        (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j)))
    (𝟙
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map g.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j)))))
⊢ pullFunctorObjHom w D (g ≫ f' j) g g ⋯ ⋯ =
    𝟙
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map g.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j))))

Tactic:
rw [pullFunctorObjHom_eq _ _ _ _ _ _ _ _ rfl rfl rfl rfl rfl,
      D.hom_self _ _ (by cat_disch)]

Premises used: CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, 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
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'
j : ι'
g : Y ⟶ X' j
hg : g ≫ f' j = q
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op Y : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map g.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j))))
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map g.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α j)))))
    ((F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j)) ≫
      𝟙
          (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
            (Cat.Hom.toFunctor (F.map (g ≫ p' j).op.toLoc)) (D.obj (α j))) ≫
        (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j)))
    (𝟙
      (Functor.obj (C := (↑(F.obj { as := op (X' j) : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map g.op.toLoc))
        (Functor.obj (C := (↑(F.obj { as := op (X (α j)) : LocallyDiscrete Cᵒᵖ }) : Type u'))
          (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (D.obj (α 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
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'
j₁ j₂ j₃ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
f₃ : Y ⟶ X' j₃
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
hf₃ : f₃ ≫ f' j₃ = q
rw :
  ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
        D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))) ≫
      (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₂)) ≫
        D.hom (q ≫ p) (f₂ ≫ p' j₂) (f₃ ≫ p' j₃) ⋯ ⋯ ≫
          (F.mapComp' (p' j₃).op.toLoc f₃.op.toLoc (f₃ ≫ p' j₃).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₃)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₃ ≫ p' j₃) ⋯ ⋯ ≫
        (F.mapComp' (p' j₃).op.toLoc f₃.op.toLoc (f₃ ≫ p' j₃).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₃))
⊢ pullFunctorObjHom w D (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ ≫ pullFunctorObjHom w D (f₂ ≫ f' j₂) f₂ f₃ ⋯ ⋯ =
    pullFunctorObjHom w D (f₁ ≫ f' j₁) f₁ f₃ ⋯ ⋯

Tactic:
rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₂ ≫ p' j₂) (f₃ ≫ p' j₃),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₃ ≫ p' j₃)]

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq
-- 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'
j₁ j₂ j₃ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
f₃ : Y ⟶ X' j₃
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
hf₃ : f₃ ≫ f' j₃ = q
⊢ ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
        D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))) ≫
      (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₂)) ≫
        D.hom (q ≫ p) (f₂ ≫ p' j₂) (f₃ ≫ p' j₃) ⋯ ⋯ ≫
          (F.mapComp' (p' j₃).op.toLoc f₃.op.toLoc (f₃ ≫ p' j₃).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₃)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₃ ≫ p' j₃) ⋯ ⋯ ≫
        (F.mapComp' (p' j₃).op.toLoc f₃.op.toLoc (f₃ ≫ p' j₃).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α 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
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₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
rw : f₁ ≫ p' j₁ ≫ f (α j₁) = q ≫ p
rw₁ : f₁ ≫ f' j₁ ≫ p = q ≫ p
rw₂ rw₃ : q ≫ p = q ≫ p
⊢ (f₁ ≫ p' j₁) ≫ f (α j₁) = q ≫ p

Tactic:
rw [Category.assoc, w, reassoc_of% hf₁]

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
D₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
rw : f₂ ≫ p' j₂ ≫ f (α j₂) = q ≫ p
rw₁ : f₂ ≫ f' j₂ ≫ p = q ≫ p
rw₂ rw₃ : q ≫ p = q ≫ p
⊢ (f₂ ≫ p' j₂) ≫ f (α j₂) = q ≫ p

Tactic:
rw [Category.assoc, w, reassoc_of% hf₂]

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
D₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ Functor.map (Cat.Hom.toFunctor (F.map (f₁ ≫ p' j₁).op.toLoc)) (φ.hom (α j₁)) ≫
      D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map (f₂ ≫ p' j₂).op.toLoc)) (φ.hom (α j₂))

Tactic:
have := φ.comm (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)
          (by rw [Category.assoc, w, reassoc_of% hf₁])
          (by rw [Category.assoc, w, 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
D₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  Functor.map (Cat.Hom.toFunctor (F.map (f₁ ≫ p' j₁).op.toLoc)) (φ.hom (α j₁)) ≫
      D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map (f₂ ≫ p' j₂).op.toLoc)) (φ.hom (α j₂))
dsimp :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₁).op.toLoc)) (φ.hom (α j₁))) ≫
      pullFunctorObjHom w D₂ (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom w D₁ (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₂).op.toLoc)) (φ.hom (α j₂)))
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₁).op.toLoc)) (φ.hom (α j₁))) ≫
      (pullFunctorObj w D₂).hom q f₁ f₂ ⋯ ⋯ =
    (pullFunctorObj w D₁).hom q f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₂).op.toLoc)) (φ.hom (α j₂)))

Tactic:
dsimp at this ⊢
-- 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₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  Functor.map
        (Cat.Hom.toFunctor
          (F.map (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc f₁.op.toLoc)))
        (φ.hom (α j₁)) ≫
      D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
      Functor.map
        (Cat.Hom.toFunctor (F.map (CategoryStruct.comp (Y := { as := op (X' j₂) }) (p' j₂).op.toLoc f₂.op.toLoc)))
        (φ.hom (α j₂))
rw :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₁).op.toLoc)) (φ.hom (α j₁))) ≫
      (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj (α j₁)) ≫
        D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj (α j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj (α j₂)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map (p' j₂).op.toLoc)) (φ.hom (α j₂)))
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₁).op.toLoc)) (φ.hom (α j₁))) ≫
      pullFunctorObjHom w D₂ (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom w D₁ (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₂).op.toLoc)) (φ.hom (α j₂)))

Tactic:
rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂),
          pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)]

Premises used: CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq
-- 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₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  Functor.map
        (Cat.Hom.toFunctor
          (F.map (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc f₁.op.toLoc)))
        (φ.hom (α j₁)) ≫
      D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
      Functor.map
        (Cat.Hom.toFunctor (F.map (CategoryStruct.comp (Y := { as := op (X' j₂) }) (p' j₂).op.toLoc f₂.op.toLoc)))
        (φ.hom (α j₂))
dsimp :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₁).op.toLoc)) (φ.hom (α j₁))) ≫
      (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc
                  (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc f₁.op.toLoc)
                  ⋯).inv.toNatTrans.app
          (D₂.obj (α j₁)) ≫
        D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc
                    (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc f₂.op.toLoc)
                    ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc
                (CategoryStruct.comp (Y := { as := op (X' j₁) : LocallyDiscrete Cᵒᵖ }) (p' j₁).op.toLoc f₁.op.toLoc)
                ⋯).inv.toNatTrans.app
        (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc
                    (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc f₂.op.toLoc)
                    ⋯).hom.toNatTrans.app
            (D₁.obj (α j₂)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map (p' j₂).op.toLoc)) (φ.hom (α j₂)))
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (p' j₁).op.toLoc)) (φ.hom (α j₁))) ≫
      (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj (α j₁)) ≫
        D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj (α j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj (α j₂)) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map (p' j₂).op.toLoc)) (φ.hom (α j₂)))

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
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
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)) ((F.isoMapOfCommSq ⋯).inv.toNatTrans.app M) ≫
      (F.mapComp' (f' i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app
          (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M) ≫
        (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app
          (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc)) M) =
    pullFunctorObjHom w (ofObj M) (f₁ ≫ f' i₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) ((F.isoMapOfCommSq ⋯).inv.toNatTrans.app M)
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Iso.hom ((fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) i₁)) ≫
      (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M).hom q f₁ f₂ ⋯ ⋯ =
    ((F.toDescentData f ⋙ pullFunctor F w).obj M).hom q f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Iso.hom ((fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) 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
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
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
⊢ Eq.{v + 1} (α := { as := op S' : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (X' i₁) }) (f' i₁).op.toLoc f₁.op.toLoc) q.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
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
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
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (X' i₁) })
      (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc (f' i₁).op.toLoc) f₁.op.toLoc)
    (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc q.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
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
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
⊢ Eq.{v + 1} (α := { as := op S' : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (X' i₂) }) (f' i₂).op.toLoc f₂.op.toLoc) q.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
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
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
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (X' i₂) })
      (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc (f' i₂).op.toLoc) f₂.op.toLoc)
    (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc q.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
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
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
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op (X' i₁) })
    (CategoryStruct.comp (Y := { as := op (X (α i₁)) }) (Quiver.Hom.toLoc (Quiver.Hom.op (f (α i₁)))) (p' i₁).op.toLoc)
    (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc (f' i₁).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
M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
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
⊢ Eq.{v + 1} (α := { as := op S : LocallyDiscrete Cᵒᵖ } ⟶ { as := op (X' i₂) })
    (CategoryStruct.comp (Y := { as := op (X (α i₂)) }) (Quiver.Hom.toLoc (Quiver.Hom.op (f (α i₂)))) (p' i₂).op.toLoc)
    (CategoryStruct.comp (Y := { as := op S' }) p.op.toLoc (f' i₂).op.toLoc)

Tactic:
grind