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₃)
obj : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj j))
hom_comp :
  ∀ (i₁ i₂ i₃ : ι),
    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
        pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
      pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback
left : φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁
left_1 : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
dsimp :
  ((F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
            (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) ≫
          (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj i₂)) ≫
      (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc ⋯).hom.toNatTrans.app (obj i₂) ≫
        Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
            (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ≫
          (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc ⋯).inv.toNatTrans.app (obj i₃) =
    (F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
          (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ≫
        (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc ⋯).inv.toNatTrans.app (obj i₃)
⊢ pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) φ f₁ f₂ ⋯ ⋯ ≫
      pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) φ f₂ f₃ ⋯ ⋯ =
    pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) φ f₁ f₃ ⋯ ⋯

Tactic:
dsimp [pullHom]

Premises used: CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.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₃)
obj : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj j))
hom_comp :
  ∀ (i₁ i₂ i₃ : ι),
    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
        pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
      pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback
left : φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁
left_1 : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
⊢ ((F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
            (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) ≫
          (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj i₂)) ≫
      (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc ⋯).hom.toNatTrans.app (obj i₂) ≫
        Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
            (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ≫
          (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc ⋯).inv.toNatTrans.app (obj i₃) =
    (F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
          (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ≫
        (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc ⋯).inv.toNatTrans.app (obj i₃)

Tactic:
simp [← Functor.map_comp_assoc, hom_comp]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- 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' sq sq₃
Y : C
q : Y ⟶ S
i : ι
g : Y ⟶ X i
hg : g ≫ f i = q
⊢ pullHom' D.hom q g g hg hg = 𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map g.op.toLoc)) (D.obj i))

Tactic:
pullHom'_self' _ D.pullHom'_hom_self _ _

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self', CategoryTheory.Pseudofunctor.DescentData'.pullHom'_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' sq sq₃
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
⊢ pullHom' D.hom q f₁ f₂ hf₁ hf₂ ≫ pullHom' D.hom q f₂ f₃ hf₂ hf₃ = pullHom' D.hom q f₁ f₃ hf₁ hf₃

Tactic:
comp_pullHom'' _ D.pullHom'_hom_comp _ _ _ _ hf₁ hf₂ hf₃

Premises used: CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'', CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp
-- 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' sq sq₃
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ pullHom' D.hom q f₁ f₂ hf₁ hf₂ ≫ pullHom' D.hom q f₂ f₁ hf₂ hf₁ =
    𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (D.obj i₁))

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' sq sq₃
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ pullHom' D.hom q f₂ f₁ hf₂ hf₁ ≫ pullHom' D.hom q f₁ f₂ hf₁ hf₂ =
    𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (D.obj i₂))

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' sq sq₃
i₁ i₂ : ι
⊢ (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p₂ ≫ f i₂

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' sq sq₃
i₁ i₂ : ι
⊢ pullHom' D.hom ((sq i₁ i₂).p₂ ≫ f i₂) (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯ = D.hom i₁ i₂

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' sq sq₃
i₁ i₂ : ι
⊢ IsIso (D.hom i₁ i₂)

Tactic:
simpa using (inferInstance : IsIso (pullHom' D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂))

Premises used: inferInstance
-- 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_1 : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f_1 i) (f_1 j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
f g : D₁ ⟶ D₂
h : ∀ (i : ι), f.hom i = g.hom i
⊢ f = g

Tactic:
Hom.ext (funext h)

Premises used: CategoryTheory.Pseudofunctor.DescentData'.Hom.ext, funext
-- 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₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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),
    p ≫ (sq i₁ i₂).p₁ = f₁ →
      p ≫ (sq i₁ i₂).p₂ = f₂ →
        Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom' D₂.hom q f₁ f₂ hf₁ hf₂ =
          pullHom' D₁.hom q f₁ f₂ hf₁ hf₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom' D₂.hom q f₁ f₂ hf₁ hf₂ =
    pullHom' D₁.hom q f₁ f₂ hf₁ hf₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)

Tactic:
obtain ⟨p, _, _⟩ := (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₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
rw :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom (D₂.hom i₁ i₂) p f₁ f₂ ⋯ ⋯ =
    pullHom (D₁.hom i₁ i₂) p f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom' D₂.hom q f₁ f₂ hf₁ hf₂ =
    pullHom' D₁.hom q f₁ f₂ hf₁ hf₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)

Tactic:
rw [← pullHom_pullHom' D₂.hom p (sq i₁ i₂).p q (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ f₁ f₂,
    ← pullHom_pullHom' D₁.hom p (sq i₁ i₂).p q (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ f₁ f₂,
    pullHom'_p₁_p₂, pullHom'_p₁_p₂]

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom', CategoryTheory.Limits.ChosenPullback.p₂, CategoryTheory.Limits.ChosenPullback.p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_p₁_p₂, CategoryTheory.Pseudofunctor.DescentData'.hom, 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₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
dsimp :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫
      (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom (D₂.hom i₁ i₂) p f₁ f₂ ⋯ ⋯ =
    pullHom (D₁.hom i₁ i₂) p f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)

Tactic:
dsimp only [pullHom]

Premises used: CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.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₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
rw :
  (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (CategoryStruct.comp (Y := F.obj { as := op (sq i₁ i₂).pullback : LocallyDiscrete Cᵒᵖ })
              (F.map (sq i₁ i₂).p₁.op.toLoc) (F.map p.op.toLoc)))
          (φ.hom i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫
      (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)

Tactic:
rw [NatTrans.naturality_assoc]

Premises used: CategoryTheory.NatTrans.naturality_assoc
-- 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₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
dsimp :
  (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
          (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (φ.hom i₁)) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (CategoryStruct.comp (Y := F.obj { as := op (sq i₁ i₂).pullback : LocallyDiscrete Cᵒᵖ })
              (F.map (sq i₁ i₂).p₁.op.toLoc) (F.map p.op.toLoc)))
          (φ.hom i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)

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₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
rw :
  (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
          (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (φ.hom i₁)) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)

Tactic:
rw [← Functor.map_comp_assoc, φ.comm, Functor.map_comp_assoc, mapComp'_inv_naturality]

Premises used: CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Pseudofunctor.DescentData'.Hom.comm
-- 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₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 : ι
⊢ 𝟙 (X i) ≫ f i = 𝟙 (X i) ≫ f i

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
i : ι
obtain :
  ∀ (p : X i ⟶ (sq i i).pullback) (h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)) (h₂ : 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)))
⊢ 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:
obtain ⟨p, h₁, h₂⟩ := (sq i i).isPullback.exists_lift (𝟙 _) (𝟙 _) (by simp)

Premises used: CategoryTheory.Limits.ChosenPullback.isPullback, CategoryTheory.CategoryStruct.id, 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
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
rw : p ≫ (sq i i).p₁ ≫ f i = f i
rw₁ rw₂ : f i = f i
⊢ p ≫ (sq i i).p = f i

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

Premises used: CategoryTheory.Limits.ChosenPullback.hp₁