Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : 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 S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this✝¹ :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
Z : Over (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
this :
  (F.map Z.hom.op.toLoc).toFunctor.map (ψ.hom i) ≫ D₂.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫ (F.map (p ≫ p' j).op.toLoc).toFunctor.map (ψ.hom (α j))
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk Z.hom ⋯).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 (p ≫ p' j) (p ≫ p' j) ⋯ ⋯ ≫
        D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯

Tactic:
dsimp [presheafHomObjHomEquiv, pullHom] at this ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : 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 S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this✝¹ :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
Z : Over (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
this :
  (F.map Z.hom.op.toLoc).toFunctor.map (ψ.hom i) ≫ D₂.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫ (F.map ((p' j).op.toLoc ≫ p.op.toLoc)).toFunctor.map (ψ.hom (α j))
⊢ (F.mapComp' (𝟙 { as := op (X i) }) Z.hom.op.toLoc Z.hom.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i) ≫
      (F.map Z.hom.op.toLoc).toFunctor.map
          ((F.mapId { as := op (X i) }).hom.toNatTrans.app (D₁.obj i) ≫
            ψ.hom i ≫ (F.mapId { as := op (X i) }).inv.toNatTrans.app (D₂.obj i)) ≫
        (F.mapComp' (𝟙 { as := op (X i) }) Z.hom.op.toLoc Z.hom.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i) =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
      ((F.mapComp' (p' j).op.toLoc p.op.toLoc ((p' j).op.toLoc ≫ p.op.toLoc) ⋯).hom.toNatTrans.app (D₁.obj (α j)) ≫
          (F.map p.op.toLoc).toFunctor.map ((F.map (p' j).op.toLoc).toFunctor.map (ψ.hom (α j))) ≫
            (F.mapComp' (p' j).op.toLoc p.op.toLoc ((p' j).op.toLoc ≫ p.op.toLoc) ⋯).inv.toNatTrans.app
              (D₂.obj (α j))) ≫
        D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯