Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ ((F.map f₁.op.toLoc).toFunctor.map
          ((F.mapComp' (f (α i₁)).op.toLoc (p' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.mapComp' (p.op.toLoc ≫ (f' i₁).op.toLoc) f₁.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).inv.toNatTrans.app M ≫
          (F.mapComp' p.op.toLoc q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app M ≫
            (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app
              ((F.map p.op.toLoc).toFunctor.obj M)) ≫
      (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc
                (@CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso._proof_1 C inst✝ S' ι' X' f'
                  Y q i₂ f₂ hf₂)).inv.toNatTrans.app
        ((F.map p.op.toLoc).toFunctor.obj M) =
    (((F.mapComp' (p' i₁).op.toLoc f₁.op.toLoc ((p' i₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app
            ((F.map (f (α i₁)).op.toLoc).toFunctor.obj M) ≫
          ((F.mapComp' (f (α i₁)).op.toLoc ((p' i₁).op.toLoc ≫ f₁.op.toLoc) (p.op.toLoc ≫ q.op.toLoc)
                        ⋯).inv.toNatTrans.app
                M ≫
              (F.mapComp' (f (α i₂)).op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) (p.op.toLoc ≫ q.op.toLoc)
                        ⋯).hom.toNatTrans.app
                M) ≫
            (F.mapComp' (p' i₂).op.toLoc f₂.op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
              ((F.map (f (α i₂)).op.toLoc).toFunctor.obj M)) ≫
        (F.map f₂.op.toLoc).toFunctor.map
            ((F.mapComp' (f (α i₂)).op.toLoc (p' i₂).op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) ⋯).inv.toNatTrans.app M) ≫
          (F.map f₂.op.toLoc).toFunctor.map
            ((F.mapComp' p.op.toLoc (f' i₂).op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) ⋯).hom.toNatTrans.app M)) ≫
      (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc
                (@CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso._proof_1 C inst✝ S' ι' X' f'
                  Y q i₂ f₂ hf₂)).inv.toNatTrans.app
        ((F.map p.op.toLoc).toFunctor.obj M)

Tactic:
simp only [Category.assoc,
          ← F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app p.op.toLoc
            (f' i₂).op.toLoc f₂.op.toLoc _ q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) rfl
            (by grind) (by grind) M,
          ← F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc (f (α i₁)).op.toLoc
            (p' i₁).op.toLoc f₁.op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) _
            (p.op.toLoc ≫ q.op.toLoc) (by grind) rfl (by grind) M,
          F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc (f (α i₂)).op.toLoc
            (p' i₂).op.toLoc f₂.op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) _
            (p.op.toLoc ≫ q.op.toLoc) (by grind) rfl (by grind) M]

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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (f (α i₁)).op.toLoc (p' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) ⋯).inv.toNatTrans.app M) ≫
      (F.mapComp' (p.op.toLoc ≫ (f' i₁).op.toLoc) f₁.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' p.op.toLoc q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app M ≫
          (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app
              ((F.map p.op.toLoc).toFunctor.obj M) ≫
            (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc
                      (@CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso._proof_1 C inst✝ S' ι'
                        X' f' Y q i₂ f₂ hf₂)).inv.toNatTrans.app
              ((F.map p.op.toLoc).toFunctor.obj M) =
    (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (f (α i₁)).op.toLoc (p' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc)
                  (@CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso._proof_6 C inst✝ ι S X f S'
                    p ι' X' f' α p' w i₁)).inv.toNatTrans.app
          M) ≫
      (F.mapComp' (p.op.toLoc ≫ (f' i₁).op.toLoc) f₁.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' (f (α i₂)).op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app
            M ≫
          (F.mapComp' (p' i₂).op.toLoc f₂.op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
              ((F.map (f (α i₂)).op.toLoc).toFunctor.obj M) ≫
            (F.mapComp' (p' i₂).op.toLoc f₂.op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) ⋯).inv.toNatTrans.app
                ((F.map (f (α i₂)).op.toLoc).toFunctor.obj M) ≫
              (F.mapComp' (f (α i₂)).op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) (p.op.toLoc ≫ q.op.toLoc)
                          ⋯).inv.toNatTrans.app
                  M ≫
                (F.mapComp' p.op.toLoc q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app M