-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
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₂ ⋯ ⋯
⊢ 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
have rw₇ : D₁.hom q f₁ f₂ sorry sorry ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom =
  D₁.hom q f₁ f₂ sorry sorry ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (e i₂).hom
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₂]