-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D D₁ D₂ : F.DescentData f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ ⦃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),
    Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯ =
      D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom
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
rw :
  (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫ D₁.hom q f₁ f₂ ⋯ ⋯) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
    (D₂.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom
rw₁ :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
    (D₂.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom
rw₂ :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
    D₂.hom q f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).inv ≫
        Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom
rw₃ :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
    D₂.hom q f₁ f₂ ⋯ ⋯ ≫ 𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (D₂.obj i₂))
rw₄ :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
    D₂.hom q f₁ f₂ ⋯ ⋯
rw₅ :
  Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).hom ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
        D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
    Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯
rw₆ :
  D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
    Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯
rw₇ rw₈ :
  D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫ D₁.hom q f₁ f₂ ⋯ ⋯ =
    D₂.hom q f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).inv

Tactic:
rw [← cancel_mono ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom), Category.assoc,
          Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
          ← cancel_epi ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom),
          Iso.map_hom_inv_id_assoc, comm q f₁ f₂ hf₁ hf₂]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.op, CategoryTheory.Iso.map_hom_inv_id_assoc, CategoryTheory.Pseudofunctor.toPrelaxFunctor, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct, CategoryTheory.Functor.map, CategoryTheory.Iso.map_inv_hom_id, Prefunctor.map, Quiver.Hom.toLoc, CategoryTheory.PrelaxFunctorStruct.toPrefunctor, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Cat.Hom.toFunctor