awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (G.imageSieve g).arrows f) → X ⟶ Z
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi :
  StructuredArrow.hom (StructuredArrow.mk (op g₁)) ≫ G.op.map (op i) =
    StructuredArrow.hom (StructuredArrow.mk (op (G.map i ≫ g₁)))
I :
  GrothendieckTopology.Cover.Arrow
    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₂) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₂)
      (G.imageSieve (G.map i ≫ g₁)) ⋯)
I' : GrothendieckTopology.Cover.Arrow
  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯) :=
  { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
⊢ f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op =
    ⋯.amalgamate
        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯)
        (fun
            (I :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁)
                  (G.imageSieve g₁) ⋯)) ↦
          f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₁ U I.f g₁ ⋯).op)
        ⋯ ≫
      Y.obj (P := Presheaf.IsSheaf J).map (op i ≫ I.f.op)
have refine_2 : f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) sorry).op =
  f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I'.Y W₁ U I'.f g₁ sorry).op
Tactic: refine Eq.trans ?_ (Y.2.amalgamate_map _ _ _ I').symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (G.imageSieve g).arrows f) → X ⟶ Z
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi :
  StructuredArrow.hom (StructuredArrow.mk (op g₁)) ≫ G.op.map (op i) =
    StructuredArrow.hom (StructuredArrow.mk (op (G.map i ≫ g₁)))
I :
  GrothendieckTopology.Cover.Arrow
    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₂) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₂)
      (G.imageSieve (G.map i ≫ g₁)) ⋯)
I' : GrothendieckTopology.Cover.Arrow
  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W₁) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W₁) (G.imageSieve g₁) ⋯) :=
  { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
⊢ f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op =
    f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I'.Y W₁ U I'.f g₁ ⋯).op
have apply : ∀ (V : C) (iUV : V ⟶ I.Y) (hiUV : iUV ≫ l I.Y W₂ U I.f (G.map i ≫ g₁) sorry = iUV ≫ l I.Y W₁ U I'.f g₁ sorry),
  Eq (α := (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).map iUV.op) :
          (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op I.Y))) →
            (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
        (f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y W₂ U I.f (G.map i ≫ g₁) sorry).op) :
      (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).map iUV.op) :
          (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op I.Y))) →
            (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
        (f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I'.Y W₁ U I'.f g₁ sorry).op) :
      (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
Tactic: apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
          (l _ _ _ _ _ I'.hf) (by simp [I', hl]))).isSeparatedFor.ext
            fun V iUV (hiUV : _ = _) ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
⊢ IsIso (X := obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)
    (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y)
have inst : IsIso (X :=
  obj (sheafToPresheaf J A) (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y))
  (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
Tactic: apply +allowSynthFailures ReflectsIsomorphisms.reflects (sheafToPresheaf J A)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
⊢ IsIso (X :=
    obj (sheafToPresheaf J A) (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y))
    (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
have inst : ∀ (X : Cᵒᵖ),
  IsIso (X :=
    (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
      X)
    (NatTrans.app (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
      X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
⊢ IsIso (X :=
    (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
      (op U))
    (NatTrans.app (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
      (op U))
have inst : IsIso (X :=
  obj yoneda
    ((obj (sheafToPresheaf J A) (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
      (op U)))
  (map yoneda
    (NatTrans.app (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
      (op U)))
Tactic: apply +allowSynthFailures ReflectsIsomorphisms.reflects yoneda
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
⊢ IsIso (X :=
    obj yoneda
      ((obj (sheafToPresheaf J A)
            (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
        (op U)))
    (map yoneda
      (NatTrans.app
        (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y)) (op U)))
have inst : ∀ (X : Aᵒᵖ),
  IsIso (X :=
    obj
      (obj yoneda
        ((obj (sheafToPresheaf J A)
              (obj (G.sheafPushforwardCocontinuous A J K ⋙ G.sheafPushforwardContinuous A J K) Y)).obj
          (op U)))
      X)
    (NatTrans.app
      (map yoneda
        (NatTrans.app
          (map (sheafToPresheaf J A) (NatTrans.app (Adjunction.counit (G.sheafAdjunctionCocontinuous A J K)) Y))
          (op U)))
      X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- 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
⊢ 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 : (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫ 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₂).inv) ≫
    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₂]
-- 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
⊢ 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₁ : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
    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₂).inv) ≫
    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₂]
-- 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
⊢ 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₂ : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
    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₂).inv ≫
      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₂]
-- 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
⊢ 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₃ : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
    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.obj (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (D₂.obj i₂))
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₂]
-- 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₂))
⊢ 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₄ : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (e i₁).inv ≫
    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
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₂]
-- 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₂ ⋯ ⋯
⊢ 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₅ : 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₂ sorry sorry ≫ 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₂ sorry sorry
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₂]