-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
i₁ i₂ : ι
rw :
  (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₁ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₂ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv ≫
        Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₃ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫ 𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (D₂.obj i₂))
rw₄ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂
rw₅ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
        D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂
rw₆ :
  D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂
rw₇ rw₈ :
  D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
⊢ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂ =
    D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv

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

Premises used: CategoryTheory.Category.assoc, 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, CategoryTheory.PrelaxFunctorStruct.toPrefunctor, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Cat.Hom.toFunctor