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
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
simp : 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:
simp only [Category.assoc,
          ← F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app p.op.toLoc
            (f' i₂).op.toLoc f₂.op.toLoc _ q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) rfl
            (by grind) (by grind) M,
          ← F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc (f (α i₁)).op.toLoc
            (p' i₁).op.toLoc f₁.op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) _
            (p.op.toLoc ≫ q.op.toLoc) (by grind) rfl (by grind) M,
          F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc (f (α i₂)).op.toLoc
            (p' i₂).op.toLoc f₂.op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) _
            (p.op.toLoc ≫ q.op.toLoc) (by grind) rfl (by grind) M]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.op, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc, CategoryTheory.CategoryStruct.comp, Quiver.Hom.toLoc, 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
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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_1 : (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_1 (α j) = f' j ≫ p
X_1 Y : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
f : X_1 ⟶ Y
h :
  ∀ (i : ι'),
    Eq (α :=
      ((F.toDescentData f_1 ⋙ pullFunctor F w).obj X_1).obj i ⟶
        (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') Y).obj i)
      (Hom.hom
        ((F.toDescentData f_1 ⋙ pullFunctor F w).map f ≫
          Iso.hom
            ((fun (M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) ↦
                (isoMk (fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) ⋯ :
                  (F.toDescentData f_1 ⋙ pullFunctor F w).obj M ≅
                    Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M))
              Y))
        i)
      (Hom.hom
        (Iso.hom
            ((fun (M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) ↦
                (isoMk (fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) ⋯ :
                  (F.toDescentData f_1 ⋙ pullFunctor F w).obj M ≅
                    Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M))
              X_1) ≫
          Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') f)
        i)
⊢ Eq (α :=
    (F.toDescentData f_1 ⋙ pullFunctor F w).obj X_1 ⟶
      Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') Y)
    ((F.toDescentData f_1 ⋙ pullFunctor F w).map f ≫
      Iso.hom
        ((fun (M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) ↦
            (isoMk (fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) ⋯ :
              (F.toDescentData f_1 ⋙ pullFunctor F w).obj M ≅
                Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M))
          Y))
    (Iso.hom
        ((fun (M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) ↦
            (isoMk (fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) ⋯ :
              (F.toDescentData f_1 ⋙ pullFunctor F w).obj M ≅
                Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M))
          X_1) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') f)

Tactic:
ext i
-- 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_1 : (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_1 (α j) = f' j ≫ p
X_1 Y : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
f : X_1 ⟶ Y
i : ι'
⊢ Eq (α :=
    ((F.toDescentData f_1 ⋙ pullFunctor F w).obj X_1).obj i ⟶
      (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') Y).obj i)
    (Hom.hom
      ((F.toDescentData f_1 ⋙ pullFunctor F w).map f ≫
        Iso.hom
          ((fun (M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) ↦
              (isoMk (fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) ⋯ :
                (F.toDescentData f_1 ⋙ pullFunctor F w).obj M ≅
                  Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M))
            Y))
      i)
    (Hom.hom
      (Iso.hom
          ((fun (M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) ↦
              (isoMk (fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) ⋯ :
                (F.toDescentData f_1 ⋙ pullFunctor F w).obj M ≅
                  Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M))
            X_1) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') f)
      i)

Tactic:
(F.isoMapOfCommSq (CommSq.mk (w i)).op.toLoc).inv.toNatTrans.naturality f

Premises used: CategoryTheory.CommSq.toLoc, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Pseudofunctor.isoMapOfCommSq, CategoryTheory.Cat.Hom₂.toNatTrans, CategoryTheory.Iso.inv
-- 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_1 : (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_1 (α j) = f' j ≫ p
X_1 Y : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
f : X_1 ⟶ Y
i : ι'
⊢ Eq (α :=
    ((F.toDescentData f_1 ⋙ pullFunctor F w).obj X_1).obj i ⟶
      (Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') Y).obj i)
    (Hom.hom
      ((F.toDescentData f_1 ⋙ pullFunctor F w).map f ≫
        Iso.hom
          ((fun (M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) ↦
              (isoMk (fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) ⋯ :
                (F.toDescentData f_1 ⋙ pullFunctor F w).obj M ≅
                  Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M))
            Y))
      i)
    (Hom.hom
      (Iso.hom
          ((fun (M : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) ↦
              (isoMk (fun (i : ι') ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M) ⋯ :
                (F.toDescentData f_1 ⋙ pullFunctor F w).obj M ≅
                  Functor.obj (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') M))
            X_1) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc) ⋙ F.toDescentData f') f)
      i)

Tactic:
exact (F.isoMapOfCommSq (CommSq.mk (w i)).op.toLoc).inv.toNatTrans.naturality f

Premises used: CategoryTheory.CommSq.toLoc, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Pseudofunctor.isoMapOfCommSq, CategoryTheory.Cat.Hom₂.toNatTrans, CategoryTheory.Iso.inv
-- 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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
dsimp :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' 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)) (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯)
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Iso.hom ((fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) j₁)) ≫
      ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
    ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Iso.hom ((fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) 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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : f₁ ≫ p' j₁ = f₁ ≫ p' j₁
⊢ f₁ ≫ p' j₁ = f₁ ≫ p' j₁

Tactic:
cat_disch
-- 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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : f₁ ≫ p'' j₁ = f₁ ≫ p'' j₁
⊢ f₁ ≫ p'' j₁ = f₁ ≫ p'' j₁

Tactic:
cat_disch
-- 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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : f₂ ≫ p' j₂ = f₂ ≫ p' j₂
⊢ f₂ ≫ p' j₂ = f₂ ≫ p' j₂

Tactic:
cat_disch
-- 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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : f₂ ≫ p'' j₂ = f₂ ≫ p'' j₂
⊢ f₂ ≫ p'' j₂ = f₂ ≫ p'' j₂

Tactic:
cat_disch
-- 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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
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₁)) ≫
      pullHom (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯) f₁ (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₂))) ≫
      (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₂)) ≫
        pullHom (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯) f₂ (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)) (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' 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)) (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯)

Tactic:
rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) _ _ rfl (by cat_disch) (by cat_disch),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) _ _ rfl (by cat_disch) (by cat_disch),
      map_eq_pullHom_assoc _ _ (f₁ ≫ p' j₁) (f₁ ≫ p'' j₁) (by cat_disch) (by cat_disch),
      map_eq_pullHom _ _ (f₂ ≫ p' j₂) (f₂ ≫ p'' j₂) (by cat_disch) (by cat_disch)]

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, 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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
simp :
  (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      pullHom (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯) f₁ (f₁ ≫ p' j₁) (f₁ ≫ p'' 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₂) ⋯ ⋯ ≫
        pullHom (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯) f₂ (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₁)) ≫
      pullHom (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯) f₁ (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₂))) ≫
      (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₂)) ≫
        pullHom (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯) f₂ (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 only [Cat.Hom.hom_inv_id_toNatTrans_app_assoc, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app_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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
rw : f₁ ≫ f' j₁ ≫ p = q ≫ p
rw₁ rw₂ : q ≫ p = q ≫ p
⊢ f₁ ≫ p' j₁ ≫ f (α j₁) = q ≫ p

Tactic:
rw [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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
rw : f₂ ≫ f' j₂ ≫ p = q ≫ p
rw₁ rw₂ : q ≫ p = q ≫ p
⊢ f₂ ≫ p' j₂ ≫ f (α j₂) = q ≫ p

Tactic:
rw [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
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
X_1 Y : F.DescentData f
φ : X_1 ⟶ Y
h :
  ∀ (j : ι'),
    Hom.hom
        ((pullFunctor F w).map φ ≫
          Iso.hom
            ((fun (D : F.DescentData f) ↦
                (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯ :
                  (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
              Y))
        j =
      Hom.hom
        (Iso.hom
            ((fun (D : F.DescentData f) ↦
                (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯ :
                  (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
              X_1) ≫
          (pullFunctor F w').map φ)
        j
⊢ (pullFunctor F w).map φ ≫
      Iso.hom
        ((fun (D : F.DescentData f) ↦
            (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯ :
              (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
          Y) =
    Iso.hom
        ((fun (D : F.DescentData f) ↦
            (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯ :
              (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
          X_1) ≫
      (pullFunctor F w').map φ

Tactic:
ext j
-- 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
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
X_1 Y : F.DescentData f
φ : X_1 ⟶ Y
j : ι'
⊢ Hom.hom
      ((pullFunctor F w).map φ ≫
        Iso.hom
          ((fun (D : F.DescentData f) ↦
              (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯ :
                (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
            Y))
      j =
    Hom.hom
      (Iso.hom
          ((fun (D : F.DescentData f) ↦
              (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯ :
                (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
            X_1) ≫
        (pullFunctor F w').map φ)
      j

Tactic:
exact φ.comm _ _ _ rfl (by cat_disch)

Premises used: rfl, CategoryTheory.Pseudofunctor.DescentData.Hom.comm
-- 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
⊢ ∀ (j : ι), (fun (x : ι) ↦ (𝟙 (X x) : X x ⟶ X x)) j ≫ f j = f j ≫ 𝟙 S

Tactic:
simp