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₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  ((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₂))
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂

Tactic:
dsimp 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₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  ((F.mapComp' (p' j₁).op.toLoc a₁.op.toLoc ((p' j₁).op.toLoc ≫ a₁.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 ((p' j₁).op.toLoc ≫ a₁.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α 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₁) (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.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₁) (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.mapComp' (p' j₂).op.toLoc a₂.op.toLoc ((p' j₂).op.toLoc ≫ a₂.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 ((p' j₂).op.toLoc ≫ a₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂))
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂