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
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ (F.map (p ≫ f₁).op.toLoc).toFunctor.map (hom w hf' φ i₁) =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        (F.map p.op.toLoc).toFunctor.map ((F.map f₂.op.toLoc).toFunctor.map (hom w hf' φ i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)

Tactic:
rw [← F.mapComp'_naturality_1 f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc (by grind),
    map_hom _ _ _ _ g (by grind), map_hom _ _ _ _ g (by grind),
    mor_eq _ _ _ _ (by grind) (p ≫ q) _ (by grind) rfl,
    mor_eq _ _ _ _ (by grind) (p ≫ q) _ (by grind) rfl,
    map_eq_pullHom _ _ _ _ rfl rfl, map_eq_pullHom _ _ _ _ rfl rfl,
    pullHom_hom _ _ _ _ rfl _ _ hf₁ hf₂ _ _ rfl rfl,
    pullHom_hom _ _ _ _ rfl _ _ hf₂ hf₁ _ _ rfl rfl]

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
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ D₁.hom (p ≫ q) (p ≫ f₁) (g ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) g (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫ D₂.hom (p ≫ q) (g ≫ p' j) (p ≫ f₁) ⋯ ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      ((F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₁) ≫
          D₁.hom (p ≫ q) (p ≫ f₁) (p ≫ f₂) ⋯ ⋯ ≫
            (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₂)) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            (D₁.hom (p ≫ q) (p ≫ f₂) (g ≫ p' j) ⋯ ⋯ ≫
                pullHom (φ.hom j) g (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫ D₂.hom (p ≫ q) (g ≫ p' j) (p ≫ f₂) ⋯ ⋯) ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) ≫
              D₂.hom (p ≫ q) (p ≫ f₂) (p ≫ f₁) ⋯ ⋯ ≫
                (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₁)) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)