Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      (F.map g.op.toLoc).toFunctor.map
          ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁)) ≫
        (F.map g.op.toLoc).toFunctor.map ((F.map p.op.toLoc).toFunctor.map (hom i₁ i₂)) ≫
          (F.map g.op.toLoc).toFunctor.map
              ((F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)) ≫
            (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (p.op.toLoc ≫ g.op.toLoc) gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      (F.map (p.op.toLoc ≫ g.op.toLoc)).toFunctor.map (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc (p.op.toLoc ≫ g.op.toLoc) gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)

Tactic:
rw [F.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc
    _ _ _ _ _ _ (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst])
    rfl (by cat_disch),
    F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app _ _ _ _ _ _
      (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]) rfl (by cat_disch)]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (p.op.toLoc ≫ g.op.toLoc) gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      (F.mapComp' p.op.toLoc g.op.toLoc (p.op.toLoc ≫ g.op.toLoc) ⋯).hom.toNatTrans.app
          ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.obj (obj i₁)) ≫
        (F.map g.op.toLoc).toFunctor.map ((F.map p.op.toLoc).toFunctor.map (hom i₁ i₂)) ≫
          (F.mapComp' p.op.toLoc g.op.toLoc (p.op.toLoc ≫ g.op.toLoc) ⋯).inv.toNatTrans.app
              ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.obj (obj' i₂)) ≫
            (F.mapComp' (sq i₁ i₂).p₂.op.toLoc (p.op.toLoc ≫ g.op.toLoc) gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (p.op.toLoc ≫ g.op.toLoc) gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      (F.map (p.op.toLoc ≫ g.op.toLoc)).toFunctor.map (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc (p.op.toLoc ≫ g.op.toLoc) gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)