Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: 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
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj 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'
this :
  (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).hom.toNatTrans.app (((pullFunctor F ⋯).obj D₁).obj j) ≫
      (F.map r.op.toLoc).toFunctor.map ((F.map a.op.toLoc).toFunctor.map (φ.hom j)) ≫
        (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).inv.toNatTrans.app (((pullFunctor F ⋯).obj D₂).obj j) =
    (F.map a'.op.toLoc).toFunctor.map (φ.hom j)
⊢ 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' ⋯ ⋯

Tactic:
dsimp [pullHom] at this ⊢

Goal state after:
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
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj 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'
this :
  (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map (p' j).op.toLoc).toFunctor.obj (D₁.obj (α j))) ≫
      (F.map r.op.toLoc).toFunctor.map ((F.map a.op.toLoc).toFunctor.map (φ.hom j)) ≫
        (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).inv.toNatTrans.app
          ((F.map (p' j).op.toLoc).toFunctor.obj (D₂.obj (α j))) =
    (F.map a'.op.toLoc).toFunctor.map (φ.hom j)
⊢ ((F.mapComp' q.op.toLoc r.op.toLoc r'.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i) ≫
        (F.map r.op.toLoc).toFunctor.map (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯) ≫
          (F.mapComp' ((p' j).op.toLoc ≫ a.op.toLoc) r.op.toLoc (((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc)
                    ⋯).inv.toNatTrans.app
            (D₁.obj (α j))) ≫
      ((F.mapComp' (p' j).op.toLoc a'.op.toLoc (((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc) ⋯).hom.toNatTrans.app
            (D₁.obj (α j)) ≫
          (F.map a'.op.toLoc).toFunctor.map (φ.hom j) ≫
            (F.mapComp' (p' j).op.toLoc a'.op.toLoc (((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc) ⋯).inv.toNatTrans.app
              (D₂.obj (α j))) ≫
        (F.mapComp' ((p' j).op.toLoc ≫ a.op.toLoc) r.op.toLoc (((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc)
                    ⋯).hom.toNatTrans.app
            (D₂.obj (α j)) ≫
          (F.map r.op.toLoc).toFunctor.map (D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯) ≫
            (F.mapComp' q.op.toLoc r.op.toLoc r'.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i) =
    (F.mapComp' q.op.toLoc r.op.toLoc r'.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i) ≫
      (F.map r.op.toLoc).toFunctor.map
          (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
            ((F.mapComp' (p' j).op.toLoc a.op.toLoc ((p' j).op.toLoc ≫ a.op.toLoc) ⋯).hom.toNatTrans.app
                  (D₁.obj (α j)) ≫
                (F.map a.op.toLoc).toFunctor.map (φ.hom j) ≫
                  (F.mapComp' (p' j).op.toLoc a.op.toLoc ((p' j).op.toLoc ≫ a.op.toLoc) ⋯).inv.toNatTrans.app
                    (D₂.obj (α j))) ≫
              D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯) ≫
        (F.mapComp' q.op.toLoc r.op.toLoc r'.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i)