awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this_1 :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
Z : Over.{v, u} (X i)
Y : C
j : ι'
p : Z.left ⟶ X' j
ψ : D₁ ⟶ D₂
hp : p ≫ f' j = Over.Hom.left (Over.homMk Z.hom ⋯) ≫ f i
this : Over.Hom.left (Over.homMk Z.hom ⋯) = Z.hom
⊢ Functor.map (Cat.Hom.toFunctor (F.map Z.hom.op.toLoc)) (ψ.hom i) ≫ D₂.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map (p ≫ p' j).op.toLoc)) (ψ.hom (α j))

Tactic:
have := ψ.comm _ Z.hom (p ≫ p' j) rfl (by grind)
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this_1 :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
Y : C
j : ι'
p : Z.left ⟶ X' j
hp : p ≫ f' j = Over.Hom.left g ≫ f i
this : Over.Hom.left g = Z.hom
⊢ ∀ (ψ : D₁ ⟶ D₂),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        ((F.presheafHomObjHomEquiv :
              (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
            (ψ.hom i) :
          (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i))))) =
      D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
        pullHom (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (ψ.hom (α j))) p (p ≫ p' j) (p ≫ p' j) ⋯ ⋯ ≫
          D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯

Tactic:
have (ψ : D₁ ⟶ D₂) :
      (F.presheafHom _ _).map g.op (F.presheafHomObjHomEquiv (ψ.hom i)) =
        D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ≫
          pullHom ((F.map (p' j).op.toLoc).toFunctor.map (ψ.hom (α j))) p _ _ ≫
          D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom := by
      obtain rfl : g = Over.homMk Z.hom := by cat_disch
      have := ψ.comm _ Z.hom (p ≫ p' j) rfl (by grind)
      dsimp [presheafHomObjHomEquiv, pullHom] at this ⊢
      simp [mapComp'_inv_naturality, Cat.Hom.comp_toFunctor,
        Functor.comp_obj, Cat.Hom.hom_inv_id_toNatTrans_app_assoc, ← reassoc_of% this,
        D₂.hom_self _ _ rfl, F.mapComp'_id_comp_inv_app, ← Functor.map_comp,
        F.mapComp'_id_comp_hom_app_assoc]
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this_1 :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
Y : C
j : ι'
p : Z.left ⟶ X' j
hp : p ≫ f' j = Over.Hom.left g ≫ f i
this_2 : Over.Hom.left g = Z.hom
this :
  ∀ (ψ : D₁ ⟶ D₂),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        ((F.presheafHomObjHomEquiv :
              (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
            (ψ.hom i) :
          (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i))))) =
      D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
        pullHom (Functor.map (Cat.Hom.toFunctor (F.map (p' j).op.toLoc)) (ψ.hom (α j))) p (p ≫ p' j) (p ≫ p' j) ⋯ ⋯ ≫
          D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯
⊢ ((pullFunctor F ⋯).map φ).hom j = ((pullFunctor F ⋯).map φ').hom j

Tactic:
replace hφ := congr_fun (congr_arg DescentData.Hom.hom hφ) j
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
i : ι
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i)))) (sieve f f' i)

Tactic:
simpa only [J.mem_over_iff, Equiv.apply_symm_apply] using J.pullback_stable (f i) hf'

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
⊢ (sieve f f' i).arrows (Y := Over.mk q) (Over.homMk q ⋯)

Tactic:
⟨_, a, f' j, ⟨j⟩, fac⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.functorPullback, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
i : ι
Z : C
q : Z ⟶ X i
hq : (sieve f f' i).arrows (Y := Over.mk q) (Over.homMk q ⋯)
obtain :
  ∀ ⦃Y : C⦄ (j : ι') (q_1 : Functor.obj (Over.forget (X i)) (Over.mk q) ⟶ X' j)
    (fac : q_1 ≫ f' j = Functor.map (Over.forget (X i)) (Over.homMk q ⋯) ≫ f i),
    ∃ (j : ι') (a : Z ⟶ X' j), a ≫ f' j = q ≫ f i
⊢ ∃ (j : ι') (a : Z ⟶ X' j), a ≫ f' j = q ≫ f i

Tactic:
obtain ⟨_, q, _, ⟨j⟩, fac⟩ := hq
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
i : ι
Z : C
q_1 : Z ⟶ X i
Y : C
j : ι'
q : Functor.obj (Over.forget (X i)) (Over.mk q_1) ⟶ X' j
fac : q ≫ f' j = Functor.map (Over.forget (X i)) (Over.homMk q_1 ⋯) ≫ f i
⊢ ∃ (j : ι') (a : Z ⟶ X' j), a ≫ f' j = q_1 ≫ f i

Tactic:
⟨j, q, fac⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
i : ι
Z : C
q_1 : Z ⟶ X i
Y : C
j : ι'
q : Functor.obj (Over.forget (X i)) (Over.mk q_1) ⟶ X' j
fac : q ≫ f' j = Functor.map (Over.forget (X i)) (Over.homMk q_1 ⋯) ≫ f i
⊢ ∃ (j : ι') (a : Z ⟶ X' j), a ≫ f' j = q_1 ≫ f i

Tactic:
exact ⟨j, q, fac⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
i : ι
Z : C
q : Z ⟶ X i
hq : (sieve f f' i).arrows (Y := Over.mk q) (Over.homMk q ⋯)
⊢ hom hq ≫ f' (idx hq) = q ≫ f i

Tactic:
(exists_fac hq).choose_spec.choose_spec

Premises used: Exists.choose_spec, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.exists_fac, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.idx, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.hom
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
q' : Z ⟶ S
a' : Z ⟶ X (α j)
hq' : q ≫ f i = q'
ha' : a ≫ p' j = a'
subst :
  mor w φ q a fac =
    D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯
⊢ mor w φ q a fac = D₁.hom q' q a' ⋯ ⋯ ≫ pullHom (φ.hom j) a a' a' ⋯ ⋯ ≫ D₂.hom q' a' q ⋯ ⋯

Tactic:
subst hq' ha'
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
⊢ mor w φ q a fac =
    D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
dsimp : mor w φ r' a' ⋯ = pullHom (mor w φ q a fac) r r' r' ⋯ ⋯
⊢ mor w φ r' a' ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Quiver.Hom.op (Over.homMk r ⋯))) :
        (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk q)))) →
          (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk r'))))
      (mor w φ q a fac)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
rw :
  pullHom (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯) r r' (r ≫ a ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) a' (r ≫ a ≫ p' j) (r ≫ a ≫ p' j) ⋯ ⋯ ≫
        pullHom (D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯) r (r ≫ a ≫ p' j) r' ⋯ ⋯ =
    pullHom
      (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
        pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯)
      r r' r' ⋯ ⋯
⊢ mor w φ r' a' ⋯ = pullHom (mor w φ q a fac) r r' r' ⋯ ⋯

Tactic:
rw [mor_eq _ _ _ _ _ (r ≫ q ≫ f i) (r ≫ a ≫ p' j),
    mor_eq _ _ _ _ _ _ _ rfl rfl,
    ← D₁.pullHom_hom r (q ≫ f i) _ rfl q (a ≫ p' j) rfl (by cat_disch) r' _ hr' rfl,
    ← D₂.pullHom_hom r (q ≫ f i) _ rfl (a ≫ p' j) q (by cat_disch) rfl _ r' rfl hr']

Premises used: CategoryTheory.Pseudofunctor.DescentData.pullHom_hom, CategoryTheory.CategoryStruct.comp, rfl, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_eq
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
⊢ Functor.map (Cat.Hom.toFunctor (F.map a₁.op.toLoc)) (φ.hom j₁) ≫
      hom (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂) (q ≫ f i) a₁ a₂ ⋯ ⋯ =
    hom (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁) (q ≫ f i) a₁ a₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map a₂.op.toLoc)) (φ.hom j₂)

Tactic:
have := φ.comm (q ≫ f i) a₁ a₂ fac₁ fac₂
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  Functor.map (Cat.Hom.toFunctor (F.map a₁.op.toLoc)) (φ.hom j₁) ≫
      (F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj (α j₁)) ≫
        D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj (α j₂)) =
    ((F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
        D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj (α j₂))) ≫
      Functor.map (Cat.Hom.toFunctor (F.map a₂.op.toLoc)) (φ.hom j₂)
⊢ a₁ ≫ p' j₁ = a₁ ≫ p' j₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  Functor.map (Cat.Hom.toFunctor (F.map a₁.op.toLoc)) (φ.hom j₁) ≫
      (F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj (α j₁)) ≫
        D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj (α j₂)) =
    ((F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
        D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj (α j₂))) ≫
      Functor.map (Cat.Hom.toFunctor (F.map a₂.op.toLoc)) (φ.hom j₂)
⊢ a₁ ≫ p' j₁ = a₁ ≫ p' j₁

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  Functor.map (Cat.Hom.toFunctor (F.map a₁.op.toLoc)) (φ.hom j₁) ≫
      pullFunctorObjHom (p := 𝟙 S) ⋯ D₂ (a₁ ≫ f' j₁) a₁ a₂ ⋯ ⋯ =
    pullFunctorObjHom (p := 𝟙 S) ⋯ D₁ (a₁ ≫ f' j₁) a₁ a₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map a₂.op.toLoc)) (φ.hom j₂)
⊢ ((F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
        pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫
          (F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj (α j₁))) ≫
      (F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj (α j₁)) ≫
        D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj (α j₂)) =
    ((F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc (a₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
        D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj (α j₂))) ≫
      (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj (α j₂)) ≫
        pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc (a₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj (α j₂))

Tactic:
rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) rfl,
    pullFunctorObjHom_eq _ _ _ _ _ (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) rfl,
    map_eq_pullHom _ _ _ _ (by exact rfl) rfl, map_eq_pullHom _ _ _ _ rfl rfl] at this

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op (X' j₂) : LocallyDiscrete Cᵒᵖ }) (p' j₂).op.toLoc a₂.op.toLoc)
                  ⋯).hom.toNatTrans.app
          (D₂.obj (α j₂)) =
    D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
      pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc a₂.op.toLoc
                  (CategoryStruct.comp (Y := { as := op (X' j₂) }) (p' j₂).op.toLoc a₂.op.toLoc) ⋯).hom.toNatTrans.app
          (D₂.obj (α j₂))
⊢ pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯

Tactic:
simp only [← Category.assoc, cancel_mono] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯
⊢ pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯

Tactic:
rw [← cancel_mono (D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q), Category.assoc,
    D₂.hom_comp] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Pseudofunctor.DescentData.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.DescentData.hom_comp