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 : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
⊢ Eq (α :=
    Functor.obj (J.diagram P (unop X)) S ⟶
      Functor.obj (J.diagram P (unop Z)) (op (((unop S).pullback f.unop).pullback g.unop)))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.comp (D := (J.Cover (unop Z))ᵒᵖ)
          { obj := fun (X_1 : (J.Cover (unop X))ᵒᵖ) ↦ op ((unop X_1).pullback (g.unop ≫ f.unop)),
            map := fun {X_1 Y_1 : (J.Cover (unop X))ᵒᵖ} (f_1 : X_1 ⟶ Y_1) ↦
              ((J.pullback (g.unop ≫ f.unop)).map f_1.unop).op,
            map_id := ⋯, map_comp := ⋯ }
          (J.diagram P (unop Z)))
        S)
      (Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) (Functor.obj (J.diagram P (unop X)) S)
        (fun (I : ((unop S).pullback (g.unop ≫ f.unop)).shape.L) ↦
          Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I))
        ⋯)
      (Functor.map (J.diagram P (unop Z)) e.inv.op))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.comp (D := (J.Cover (unop Y))ᵒᵖ)
          { obj := fun (X_1 : (J.Cover (unop X))ᵒᵖ) ↦ op ((unop X_1).pullback f.unop),
            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)))
        S)
      (Multiequalizer.lift (((unop S).pullback f.unop).index P) (Functor.obj (J.diagram P (unop X)) S)
        (fun (I : ((unop S).pullback f.unop).shape.L) ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯)
      (Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
        (Functor.obj (J.diagram P (unop Y)) (op ((unop S).pullback f.unop)))
        (fun (I : (((unop S).pullback f.unop).pullback g.unop).shape.L) ↦
          Multiequalizer.ι (((unop S).pullback f.unop).index P) (Cover.Arrow.base I))
        ⋯))

Tactic:
Multiequalizer.hom_ext _ _ _ (fun I => ?_)

Premises used: CategoryTheory.Limits.limit, 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)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
I : (unop (op (((unop S).pullback f.unop).pullback g.unop))).shape.L
e_a :
  Eq (α := multiequalizer ((unop S).index P) ⟶ P.obj (op I.Y))
    (Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I e.inv).base :
      multiequalizer ((unop S).index P) ⟶ ((unop S).index P).left (Cover.Arrow.map I e.inv).base)
    (Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I).base)
⊢ Eq (α := multiequalizer ((unop S).index P) ⟶ P.obj (op I.Y))
    (CategoryStruct.comp (Y := multiequalizer ((((unop S).pullback f.unop).pullback g.unop).index P))
      (CategoryStruct.comp (Y := multiequalizer (((unop S).pullback (g.unop ≫ f.unop)).index P))
        (Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) (multiequalizer ((unop S).index P))
          (fun (I : ((unop S).pullback (g.unop ≫ f.unop)).Arrow) ↦ Multiequalizer.ι ((unop S).index P) I.base) ⋯)
        (Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          (multiequalizer (((unop S).pullback (g.unop ≫ f.unop)).index P))
          (fun (I : (((unop S).pullback f.unop).pullback g.unop).Arrow) ↦
            Multiequalizer.ι (((unop S).pullback (g.unop ≫ f.unop)).index P) (I.map e.inv))
          ⋯))
      (Multiequalizer.ι ((((unop S).pullback f.unop).pullback g.unop).index P) I))
    (CategoryStruct.comp (Y := multiequalizer ((((unop S).pullback f.unop).pullback g.unop).index P))
      (CategoryStruct.comp (Y := multiequalizer (((unop S).pullback f.unop).index P))
        (Multiequalizer.lift (((unop S).pullback f.unop).index P) (multiequalizer ((unop S).index P))
          (fun (I : ((unop S).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop S).index P) I.base) ⋯)
        (Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          (multiequalizer (((unop S).pullback f.unop).index P))
          (fun (I : (((unop S).pullback f.unop).pullback g.unop).Arrow) ↦
            Multiequalizer.ι (((unop S).pullback f.unop).index P) I.base)
          ⋯))
      (Multiequalizer.ι ((((unop S).pullback f.unop).pullback g.unop).index P) I))

Tactic:
simp only [Multiequalizer.lift_ι, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Multiequalizer.lift_ι
-- 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 Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
I : (unop (op (((unop S).pullback f.unop).pullback g.unop))).shape.L
e_a :
  ∀ (Y_1 : C) (f_1 : Y_1 ⟶ unop Z)
    (hf : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop))) : Sieve (unop Z)).arrows f_1),
    Eq (α :=
      multiequalizer ((unop S).index P) ⟶
        P.obj (op { Y := Y_1, f := f_1, hf := hf : (unop (op (((unop S).pullback f.unop).pullback g.unop))).Arrow }.Y))
      (Multiequalizer.ι ((unop S).index P)
          ({ Y := Y_1, f := f_1, hf := hf : (unop (op (((unop S).pullback f.unop).pullback g.unop))).Arrow }.map
              e.inv).base :
        multiequalizer ((unop S).index P) ⟶
          ((unop S).index P).left
            ({ Y := Y_1, f := f_1, hf := hf : (unop (op (((unop S).pullback f.unop).pullback g.unop))).Arrow }.map
                e.inv).base)
      (Multiequalizer.ι ((unop S).index P)
        { Y := Y_1, f := f_1, hf := hf : (unop (op (((unop S).pullback f.unop).pullback g.unop))).Arrow }.base.base)
⊢ Eq (α := multiequalizer ((unop S).index P) ⟶ P.obj (op I.Y))
    (Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I e.inv).base :
      multiequalizer ((unop S).index P) ⟶ ((unop S).index P).left (Cover.Arrow.map I e.inv).base)
    (Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I).base)

Tactic:
cases I
-- 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 Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
Y_1 : C
f_1 : Y_1 ⟶ unop Z
hf : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop))) : Sieve (unop Z)).arrows f_1
e_a :
  Eq (α := multiequalizer ((unop S).index P) ⟶ P.obj (op Y_1))
    (Multiequalizer.ι ((unop S).index P) { Y := Y_1, f := f_1 ≫ g.unop ≫ f.unop, hf := ⋯ } :
      multiequalizer ((unop S).index P) ⟶ ((unop S).index P).left { Y := Y_1, f := f_1 ≫ g.unop ≫ f.unop, hf := ⋯ })
    (Multiequalizer.ι ((unop S).index P) { Y := Y_1, f := (f_1 ≫ g.unop) ≫ f.unop, hf := ⋯ })
⊢ Eq (α :=
    multiequalizer ((unop S).index P) ⟶
      P.obj (op { Y := Y_1, f := f_1, hf := hf : (unop (op (((unop S).pullback f.unop).pullback g.unop))).Arrow }.Y))
    (Multiequalizer.ι ((unop S).index P)
        ({ Y := Y_1, f := f_1, hf := hf : (unop (op (((unop S).pullback f.unop).pullback g.unop))).Arrow }.map
            e.inv).base :
      multiequalizer ((unop S).index P) ⟶
        ((unop S).index P).left
          ({ Y := Y_1, f := f_1, hf := hf : (unop (op (((unop S).pullback f.unop).pullback g.unop))).Arrow }.map
              e.inv).base)
    (Multiequalizer.ι ((unop S).index P)
      { Y := Y_1, f := f_1, hf := hf : (unop (op (((unop S).pullback f.unop).pullback g.unop))).Arrow }.base.base)

Tactic:
dsimp only [Cover.Arrow.base, Cover.Arrow.map]

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.base, CategoryTheory.GrothendieckTopology.Cover.Arrow.map
-- 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 Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
Y_1 : C
f_1 : Y_1 ⟶ unop Z
hf : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop))) : Sieve (unop Z)).arrows f_1
e_a : f_1 ≫ g.unop ≫ f.unop = (f_1 ≫ g.unop) ≫ f.unop
⊢ Eq (α := multiequalizer ((unop S).index P) ⟶ P.obj (op Y_1))
    (Multiequalizer.ι ((unop S).index P) { Y := Y_1, f := f_1 ≫ g.unop ≫ f.unop, hf := ⋯ } :
      multiequalizer ((unop S).index P) ⟶ ((unop S).index P).left { Y := Y_1, f := f_1 ≫ g.unop ≫ f.unop, hf := ⋯ })
    (Multiequalizer.ι ((unop S).index P) { Y := Y_1, f := (f_1 ≫ g.unop) ≫ f.unop, hf := ⋯ })

Tactic:
congr 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)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
Y_1 : C
f_1 : Y_1 ⟶ unop Z
hf : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop))) : Sieve (unop Z)).arrows f_1
⊢ f_1 ≫ g.unop ≫ f.unop = (f_1 ≫ g.unop) ≫ f.unop

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)
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
dsimp :
  Eq (α :=
    colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) ⟶
      colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram Q (unop Y)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop 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))
      (colimMap (J.diagramNatTrans η (unop Y))))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X)))
      (colimMap (J.diagramNatTrans η (unop X)))
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)))
        (colimMap (J.diagramPullback Q f.unop)) (colimit.pre (J.diagram Q (unop Y)) (J.pullback f.unop).op)))
⊢ (J.plusObj P).map f ≫ colimMap (J.diagramNatTrans η (unop Y)) =
    colimMap (J.diagramNatTrans η (unop X)) ≫ (J.plusObj Q).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_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
w :
  ∀ (j : (J.Cover (unop X))ᵒᵖ),
    Eq (α := Functor.obj (J.diagram P (unop X)) j ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram Q (unop Y)))
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
        (colimit.ι (J.diagram P (unop X)) j)
        (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop 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))
          (colimMap (J.diagramNatTrans η (unop Y)))))
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
        (colimit.ι (J.diagram P (unop X)) j)
        (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X)))
          (colimMap (J.diagramNatTrans η (unop X)))
          (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)))
            (colimMap (J.diagramPullback Q f.unop)) (colimit.pre (J.diagram Q (unop Y)) (J.pullback f.unop).op))))
⊢ Eq (α :=
    colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) ⟶
      colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram Q (unop Y)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop 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))
      (colimMap (J.diagramNatTrans η (unop Y))))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X)))
      (colimMap (J.diagramNatTrans η (unop X)))
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)))
        (colimMap (J.diagramPullback Q f.unop)) (colimit.pre (J.diagram Q (unop Y)) (J.pullback f.unop).op)))

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)
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))ᵒᵖ
w :
  Eq (α := Functor.obj (J.diagram P (unop X)) j ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram Q (unop Y)))
    (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) ≫
        colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j))
    (NatTrans.app (J.diagramNatTrans η (unop X)) j ≫
      CategoryStruct.comp (Y := ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)).obj 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))
          ⋯)
        (colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j)))
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) j ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram Q (unop Y)))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) j)
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop 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))
        (colimMap (J.diagramNatTrans η (unop Y)))))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) j)
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram Q (unop X)))
        (colimMap (J.diagramNatTrans η (unop X)))
        (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)))
          (colimMap (J.diagramPullback Q f.unop)) (colimit.pre (J.diagram Q (unop Y)) (J.pullback f.unop).op))))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_pre_assoc, CategoryTheory.Limits.ι_colimMap, 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_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))ᵒᵖ
w :
  Eq (α := Functor.obj (J.diagram P (unop X)) j ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram Q (unop Y)))
    ((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)) ≫
      colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j))
    (CategoryStruct.comp (Y := ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)).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))
          ⋯)
      (colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j)))
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) j ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram Q (unop Y)))
    (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) ≫
        colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j))
    (NatTrans.app (J.diagramNatTrans η (unop X)) j ≫
      CategoryStruct.comp (Y := ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)).obj 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))
          ⋯)
        (colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j)))

Tactic:
simp_rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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))ᵒᵖ
w :
  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))
        ⋯)
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) j ⟶ colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram Q (unop Y)))
    ((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)) ≫
      colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j))
    (CategoryStruct.comp (Y := ((J.pullback f.unop).op ⋙ J.diagram Q (unop Y)).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))
          ⋯)
      (colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j)))

Tactic:
congr 1
-- 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))ᵒᵖ
I : (unop ((J.pullback f.unop).op.obj j)).shape.L
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) j ⟶ ((unop ((J.pullback f.unop).op.obj j)).index Q).left I)
    (CategoryStruct.comp (Y := multiequalizer ((unop ((J.pullback f.unop).op.obj j)).index Q))
      (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) :
        Functor.obj (J.diagram P (unop X)) j ⟶ Functor.obj (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j))
      (Multiequalizer.ι ((unop ((J.pullback f.unop).op.obj j)).index Q) I))
    (CategoryStruct.comp (Y := multiequalizer ((unop ((J.pullback f.unop).op.obj j)).index Q))
      (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))
          ⋯)
      (Multiequalizer.ι ((unop ((J.pullback f.unop).op.obj j)).index Q) I))

Tactic:
simp