awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P_1 : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j : (J.Cover (unop X))ᵒᵖ
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) j ⟶ Functor.obj (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j))
    (Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j)).index P) (Functor.obj (J.diagram P (unop X)) j)
        (fun (I : (unop ((J.pullback f.unop).op.obj j)).shape.L) ↦
          Multiequalizer.ι ((unop j).index P) (Cover.Arrow.base I))
        ⋯ ≫
      NatTrans.app (J.diagramNatTrans η (unop Y)) ((J.pullback f.unop).op.obj j))
    (NatTrans.app (J.diagramNatTrans η (unop X)) j ≫
      Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j)).index Q) (Functor.obj (J.diagram Q (unop X)) j)
        (fun (I : (unop ((J.pullback f.unop).op.obj j)).shape.L) ↦
          Multiequalizer.ι ((unop j).index Q) (Cover.Arrow.base I))
        ⋯)

Tactic:
exact Multiequalizer.hom_ext _ _ _ (fun I => by simp)

Premises used: CategoryTheory.Limits.Multiequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
w : ∀ (x : Cᵒᵖ), NatTrans.app (J.plusMap (𝟙 P)) x = NatTrans.app (𝟙 (J.plusObj P)) x
⊢ J.plusMap (𝟙 P) = 𝟙 (J.plusObj P)

Tactic:
ext : 2
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
w :
  Eq (α :=
    colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)) ⟶
      colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
    (colimMap (J.diagramNatTrans (𝟙 P) (unop x)))
    (NatTrans.app
      (𝟙
        { obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)),
          map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
            CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
              (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op),
          map_id := ⋯, map_comp := ⋯ })
      x)
⊢ NatTrans.app (J.plusMap (𝟙 P)) x = NatTrans.app (𝟙 (J.plusObj P)) x

Tactic:
dsimp only [plusMap, plusObj]

Premises used: CategoryTheory.GrothendieckTopology.plusMap, CategoryTheory.GrothendieckTopology.plusObj
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
w :
  Eq (α :=
    colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)) ⟶
      colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
    (colimMap (𝟙 (J.diagram P (unop x))))
    (𝟙
      (Functor.obj.{v, w', u, w}
        { obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)),
          map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
            CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
              (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op),
          map_id := ⋯, map_comp := ⋯ }
        x))
⊢ Eq (α :=
    colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)) ⟶
      colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
    (colimMap (J.diagramNatTrans (𝟙 P) (unop x)))
    (NatTrans.app
      (𝟙
        { obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)),
          map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
            CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
              (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op),
          map_id := ⋯, map_comp := ⋯ })
      x)

Tactic:
rw [J.diagramNatTrans_id, NatTrans.id_app]

Premises used: CategoryTheory.NatTrans.id_app, CategoryTheory.GrothendieckTopology.diagramNatTrans_id
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
w :
  ∀ (j : (J.Cover (unop x))ᵒᵖ),
    Eq (α := Functor.obj (J.diagram P (unop x)) j ⟶ colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
        (colimit.ι (J.diagram P (unop x)) j) (colimMap (𝟙 (J.diagram P (unop x)))))
      (colimit.ι (J.diagram P (unop x)) j ≫
        𝟙
          (Functor.obj.{v, w', u, w}
            { obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)),
              map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
                CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
                  (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op),
              map_id := ⋯, map_comp := ⋯ : Functor.{v, w', u, w} Cᵒᵖ D }
            x))
⊢ Eq (α :=
    colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)) ⟶
      colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
    (colimMap (𝟙 (J.diagram P (unop x))))
    (𝟙
      (Functor.obj.{v, w', u, w}
        { obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)),
          map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
            CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
              (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op),
          map_id := ⋯, map_comp := ⋯ }
        x))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
j : (J.Cover (unop x))ᵒᵖ
⊢ Eq (α := Functor.obj (J.diagram P (unop x)) j ⟶ colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
      (colimit.ι (J.diagram P (unop x)) j) (colimMap (𝟙 (J.diagram P (unop x)))))
    (colimit.ι (J.diagram P (unop x)) j ≫
      𝟙
        (Functor.obj.{v, w', u, w}
          { obj := fun (X : Cᵒᵖ) ↦ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)),
            map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦
              CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
                (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op),
            map_id := ⋯, map_comp := ⋯ : Functor.{v, w', u, w} Cᵒᵖ D }
          x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
w :
  ∀ (x : Cᵒᵖ),
    Eq.{w' + 1} (α := (J.plusObj P).obj x ⟶ (J.plusObj Q).obj x) (NatTrans.app (J.plusMap 0) x) (NatTrans.app 0 x)
⊢ Eq (α := J.plusObj P ⟶ J.plusObj Q) (J.plusMap 0) 0

Tactic:
ext : 2
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
⊢ Eq.{w' + 1} (α := (J.plusObj P).obj x ⟶ (J.plusObj Q).obj x) (NatTrans.app (J.plusMap 0) x) (NatTrans.app 0 x)

Tactic:
colimit.hom_ext (fun S => ?_)

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
w :
  ∀ (S : (J.Cover (unop x))ᵒᵖ),
    Eq (α := Functor.obj (J.diagram P (unop x)) S ⟶ (J.plusObj Q).obj x)
      (colimit.ι (J.diagram P (unop x)) S ≫ NatTrans.app (J.plusMap 0) x)
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
        (colimit.ι (J.diagram P (unop x)) S) (NatTrans.app 0 x))
⊢ Eq.{w' + 1} (α := (J.plusObj P).obj x ⟶ (J.plusObj Q).obj x) (NatTrans.app (J.plusMap 0) x) (NatTrans.app 0 x)

Tactic:
refine colimit.hom_ext (fun S => ?_)

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
S : (J.Cover (unop x))ᵒᵖ
⊢ Eq (α := Functor.obj (J.diagram P (unop x)) S ⟶ (J.plusObj Q).obj x)
    (colimit.ι (J.diagram P (unop x)) S ≫ NatTrans.app (J.plusMap 0) x)
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x)))
      (colimit.ι (J.diagram P (unop x)) S) (NatTrans.app 0 x))

Tactic:
simp [plusMap]

Premises used: CategoryTheory.GrothendieckTopology.plusMap
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
w :
  ∀ (x : Cᵒᵖ),
    Eq (α := (J.plusObj P).obj x ⟶ (J.plusObj R).obj x) (NatTrans.app (J.plusMap (η ≫ γ)) x)
      (NatTrans.app (J.plusMap η ≫ J.plusMap γ) x)
⊢ Eq (α := J.plusObj P ⟶ J.plusObj R) (J.plusMap (η ≫ γ)) (J.plusMap η ≫ J.plusMap γ)

Tactic:
ext : 2
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
x : Cᵒᵖ
⊢ Eq (α := (J.plusObj P).obj x ⟶ (J.plusObj R).obj x) (NatTrans.app (J.plusMap (η ≫ γ)) x)
    (NatTrans.app (J.plusMap η ≫ J.plusMap γ) x)

Tactic:
colimit.hom_ext (fun S => ?_)

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
x : Cᵒᵖ
w :
  ∀ (S : (J.Cover (unop x))ᵒᵖ),
    Eq (α := Functor.obj (J.diagram P (unop x)) S ⟶ (J.plusObj R).obj x)
      (colimit.ι (J.diagram P (unop x)) S ≫ NatTrans.app (J.plusMap (η ≫ γ)) x)
      (colimit.ι (J.diagram P (unop x)) S ≫ NatTrans.app (J.plusMap η ≫ J.plusMap γ) x)
⊢ Eq (α := (J.plusObj P).obj x ⟶ (J.plusObj R).obj x) (NatTrans.app (J.plusMap (η ≫ γ)) x)
    (NatTrans.app (J.plusMap η ≫ J.plusMap γ) x)

Tactic:
refine colimit.hom_ext (fun S => ?_)

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
x : Cᵒᵖ
S : (J.Cover (unop x))ᵒᵖ
⊢ Eq (α := Functor.obj (J.diagram P (unop x)) S ⟶ (J.plusObj R).obj x)
    (colimit.ι (J.diagram P (unop x)) S ≫ NatTrans.app (J.plusMap (η ≫ γ)) x)
    (colimit.ι (J.diagram P (unop x)) S ≫ NatTrans.app (J.plusMap η ≫ J.plusMap γ) x)

Tactic:
simp [plusMap, J.diagramNatTrans_comp]

Premises used: CategoryTheory.GrothendieckTopology.plusMap, CategoryTheory.GrothendieckTopology.diagramNatTrans_comp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
dsimp :
  Eq (α := P.obj X ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y)))
    (P.map f ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop Y)) (op ⊤)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop X)) (op ⊤)))
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
        (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op)))
⊢ P.map f ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop Y)) (op ⊤)) =
    CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop X)) (op ⊤)) ≫
      (J.plusObj P).map f

Tactic:
dsimp [plusObj]

Premises used: CategoryTheory.GrothendieckTopology.plusObj
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
delta :
  Eq (α := P.obj X ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y)))
    (P.map f ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (colimit.ι (J.diagram P (unop Y)) (op ⊤)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (colimit.ι (J.diagram P (unop X)) (op ⊤)))
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
        (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op)))
⊢ Eq (α := P.obj X ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y)))
    (P.map f ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop Y)) (op ⊤)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop X)) (op ⊤)))
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
        (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op)))

Tactic:
delta Cover.toMultiequalizer

Premises used: CategoryTheory.GrothendieckTopology.Cover.toMultiequalizer
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
simp :
  Eq (α := P.obj X ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y)))
    (P.map f ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (colimit.ι (J.diagram P (unop Y)) (op ⊤)))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
      (CategoryStruct.comp (Y := ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)).obj (op ⊤))
        (Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj (op ⊤))).index P)
          (Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤))
          (fun (I : (unop ((J.pullback f.unop).op.obj (op ⊤))).shape.L) ↦
            Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I))
          ⋯)
        (colimit.ι (J.diagram P (unop Y)) ((J.pullback f.unop).op.obj (op ⊤)))))
⊢ Eq (α := P.obj X ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y)))
    (P.map f ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (colimit.ι (J.diagram P (unop Y)) (op ⊤)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (colimit.ι (J.diagram P (unop X)) (op ⊤)))
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
        (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op)))

Tactic:
simp only [diagramPullback_app, colimit.ι_pre, ι_colimMap_assoc, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.colimit.ι_pre, CategoryTheory.GrothendieckTopology.diagramPullback_app
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
e_a :
  Eq (α := P.obj X ⟶ Functor.obj (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤)))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
      (P.map f ≫
        Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
      (Functor.map (J.diagram P (unop Y)) e.op))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
      (Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P)
        (Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤))
        (fun (I : ((J.pullback f.unop).obj ⊤).shape.L) ↦ Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I)) ⋯))
⊢ Eq (α := P.obj X ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y)))
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (P.map f ≫
          Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
            (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (Functor.map (J.diagram P (unop Y)) e.op) ≫
      colimit.ι (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤)))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := (J.Cover (unop X))ᵒᵖ)
        (Functor.comp (D := (J.Cover (unop Y))ᵒᵖ)
          { obj := fun (X_1 : (J.Cover (unop X))ᵒᵖ) ↦ op ((J.pullback f.unop).obj (unop X_1)),
            map := fun {X_1 Y_1 : (J.Cover (unop X))ᵒᵖ} (f_1 : X_1 ⟶ Y_1) ↦ ((J.pullback f.unop).map f_1.unop).op,
            map_id := ⋯, map_comp := ⋯ }
          (J.diagram P (unop Y)))
        (op ⊤))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P)
          (Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤))
          (fun (I : ((J.pullback f.unop).obj ⊤).shape.L) ↦ Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I)) ⋯))
      (colimit.ι (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤))))

Tactic:
congr 1