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)
obj 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))
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
obtain :
  ∀ (hp₁ : ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₁ = f₁) (hp₂ : ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₂ = f₂),
    pullHom' hom q f₁ f₂ hf₁ hf₂ = pullHom (hom i₁ i₂) (⋯.lift f₁ f₂ ⋯) f₁ f₂ ⋯ ⋯
⊢ pullHom' hom q f₁ f₂ hf₁ hf₂ = pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯

Tactic:
obtain rfl : p = (sq i₁ i₂).isPullback.lift f₁ f₂ (by rw [hf₁, hf₂]) := by
    apply (sq i₁ i₂).isPullback.hom_ext <;> cat_disch

Premises used: CategoryTheory.Limits.ChosenPullback.isPullback, CategoryTheory.IsPullback.lift, rfl
-- 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)
obj 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))
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
hp₁ : ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₂ = f₂
⊢ pullHom' hom q f₁ f₂ hf₁ hf₂ = pullHom (hom i₁ i₂) (⋯.lift f₁ f₂ ⋯) f₁ f₂ ⋯ ⋯

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

Tactic:
pullHom'_eq_pullHom _ _ _ ..

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
obj 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))
i₁ i₂ i₃ : ι
⊢ pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom (hom i₁ i₃) (sq₃ i₁ i₂ i₃).p₁₃ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯

Tactic:
pullHom'_eq_pullHom _ _ _ ..

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
obj 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))
i₁ i₂ i₃ : ι
⊢ pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom (hom i₂ i₃) (sq₃ i₁ i₂ i₃).p₂₃ (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯

Tactic:
pullHom'_eq_pullHom _ _ _ ..

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj 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))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
rw : pullHom (pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ = pullHom (hom i₁ i₂) (g ≫ p) gf₁ gf₂ ⋯ ⋯
⊢ pullHom (pullHom' hom q f₁ f₂ hf₁ hf₂) g gf₁ gf₂ ⋯ ⋯ = pullHom' hom q' gf₁ gf₂ ⋯ ⋯

Tactic:
rw [pullHom'_eq_pullHom _ _ _ _ p, pullHom'_eq_pullHom _ _ _ _ (g ≫ p)]

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom, CategoryTheory.CategoryStruct.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)
obj 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))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
dsimp :
  (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
          ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
            Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂) ≫
              (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)) ≫
        (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
                ⋯).hom.toNatTrans.app
        (obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
          (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                  ⋯).inv.toNatTrans.app
          (obj' i₂)
⊢ pullHom (pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ = pullHom (hom i₁ i₂) (g ≫ p) gf₁ gf₂ ⋯ ⋯

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)
obj 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))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
rw :
  Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (Quiver.Hom.toLoc ((sq i₁ i₂).p₁.op ≫ p.op)) f₁.op.toLoc
rw₁ :
  Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) (p ≫ (sq i₁ i₂).p₁).op.toLoc f₁.op.toLoc
rw₂ rw₃ : Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) f₁.op.toLoc f₁.op.toLoc
⊢ Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (sq i₁ i₂).pullback }) (sq i₁ i₂).p₁.op.toLoc p.op.toLoc) f₁.op.toLoc

Tactic:
rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst]

Premises used: CategoryTheory.op_comp, Quiver.Hom.comp_toLoc, CategoryTheory.IsPullback.lift_fst
-- 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)
obj 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))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
rw :
  Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (Quiver.Hom.toLoc ((sq i₁ i₂).p₂.op ≫ p.op)) f₂.op.toLoc
rw₁ :
  Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) (p ≫ (sq i₁ i₂).p₂).op.toLoc f₂.op.toLoc
rw₂ rw₃ : Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) f₂.op.toLoc f₂.op.toLoc
⊢ Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (sq i₁ i₂).pullback }) (sq i₁ i₂).p₂.op.toLoc p.op.toLoc) f₂.op.toLoc

Tactic:
rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]

Premises used: CategoryTheory.op_comp, Quiver.Hom.comp_toLoc, CategoryTheory.IsPullback.lift_snd
-- 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)
obj 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))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ CategoryStruct.comp (Y :=
      Functor.obj (C := (↑(F.obj { as := op (sq i₁ i₂).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
        (Cat.Hom.toFunctor (F.map (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)))
        (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (obj i₁)))
      (NatTrans.app
        (Cat.Hom₂.toNatTrans
          (Iso.hom
            (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)
              gf₁.op.toLoc ⋯)))
        (obj i₁))
      (NatTrans.app
          (Cat.Hom₂.toNatTrans
            (Iso.hom
              (F.mapComp' p.op.toLoc g.op.toLoc
                (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) ⋯)))
          (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (obj i₁)) ≫
        Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂)) ≫
          NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.inv
                  (F.mapComp' p.op.toLoc g.op.toLoc
                    (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) ⋯)))
              (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (obj' i₂)) ≫
            NatTrans.app
              (Cat.Hom₂.toNatTrans
                (Iso.inv
                  (F.mapComp' (sq i₁ i₂).p₂.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc)
                    gf₂.op.toLoc ⋯)))
              (obj' i₂)) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc
                (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
                ⋯).hom.toNatTrans.app
        (obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
          (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                  ⋯).inv.toNatTrans.app
          (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₃)
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))
i₁ i₂ : ι
⊢ (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
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))
i₁ i₂ : ι
⊢ (sq i₁ i₂).p₂ ≫ f i₂ = (sq i₁ i₂).p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
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))
i₁ i₂ : ι
⊢ pullHom' hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯ = hom i₁ i₂

Tactic:
simp [pullHom'_eq_pullHom hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ (𝟙 _)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.ChosenPullback.p₂, CategoryTheory.Limits.ChosenPullback.p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom, 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)
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_self :
  ∀ (i : ι),
    pullHom' hom (f i) (𝟙 (X i)) (𝟙 (X i)) ⋯ ⋯ =
      𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (obj i))
Y : C
q : Y ⟶ S
i : ι
g : Y ⟶ X i
hg : g ≫ f i = q
⊢ pullHom' hom q g g hg hg = 𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map g.op.toLoc)) (obj i))

Tactic:
simp [← pullHom_pullHom' hom g (f i) q (𝟙 (X i)) (𝟙 (X i)) g g hg, hom_self, pullHom]

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom', CategoryTheory.CategoryStruct.id, 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
obtain :
  ∀ (φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback),
    φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁ →
      φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂ →
        φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃ → pullHom' hom q f₁ f₂ ⋯ ⋯ ≫ pullHom' hom q f₂ f₃ ⋯ ⋯ = pullHom' hom q f₁ f₃ ⋯ ⋯
⊢ pullHom' hom q f₁ f₂ ⋯ ⋯ ≫ pullHom' hom q f₂ f₃ ⋯ ⋯ = pullHom' hom q f₁ f₃ ⋯ ⋯

Tactic:
obtain ⟨φ, _, _, _⟩ := (sq₃ i₁ i₂ i₃).exists_lift f₁ f₂ f₃ q hf₁ hf₂ hf₃

Premises used: CategoryTheory.Limits.ChosenPullback₃.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₃)
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₃
rw :
  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₃ ⋯ ⋯
⊢ pullHom' hom q f₁ f₂ ⋯ ⋯ ≫ pullHom' hom q f₂ f₃ ⋯ ⋯ = pullHom' hom q f₁ f₃ ⋯ ⋯

Tactic:
rw [← pullHom_pullHom'_assoc hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ _ _,
    ← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ _ _,
    ← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ _ _]

Premises used: CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom', CategoryTheory.Limits.ChosenPullback₃.p₂, CategoryTheory.Limits.ChosenPullback₃.p₃, CategoryTheory.Limits.ChosenPullback₃.p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'_assoc, CategoryTheory.Limits.ChosenPullback₃.p