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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
w :
  Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) S)
      (colimMap
        (J.diagramNatTrans
          {
            app := fun (X : Cᵒᵖ) ↦
              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 ⊤)),
            naturality := ⋯ }
          (unop X))))
    (colimit.ι (J.diagram P (unop X)) S ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (Cover.toMultiequalizer ⊤ (J.plusObj P)) (colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)))
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (colimit.ι (J.diagram P (unop X)) S ≫ NatTrans.app (J.plusMap (J.toPlus P)) X)
    (colimit.ι (J.diagram P (unop X)) S ≫ NatTrans.app (J.toPlus (J.plusObj P)) X)

Tactic:
dsimp only [plusMap, toPlus]

Premises used: CategoryTheory.GrothendieckTopology.plusMap, CategoryTheory.GrothendieckTopology.toPlus
-- 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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
w :
  Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (NatTrans.app
        (J.diagramNatTrans
          {
            app := fun (X : Cᵒᵖ) ↦
              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 ⊤)),
            naturality := ⋯ }
          (unop X))
        S ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) S)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
        (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op) ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) (op (unop S)))
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) S)
      (colimMap
        (J.diagramNatTrans
          {
            app := fun (X : Cᵒᵖ) ↦
              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 ⊤)),
            naturality := ⋯ }
          (unop X))))
    (colimit.ι (J.diagram P (unop X)) S ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (Cover.toMultiequalizer ⊤ (J.plusObj P)) (colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)))

Tactic:
rw [ι_colimMap, ← colimit.w _ e.op, ← Category.assoc, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.op, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.colimit.w
-- 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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
w :
  Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ Functor.obj (J.diagram (J.plusObj P) (unop X)) S)
    (NatTrans.app
      (J.diagramNatTrans
        {
          app := fun (X : Cᵒᵖ) ↦
            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 ⊤)),
          naturality := ⋯ }
        (unop X))
      S)
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
      (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
      (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op))
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (NatTrans.app
        (J.diagramNatTrans
          {
            app := fun (X : Cᵒᵖ) ↦
              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 ⊤)),
            naturality := ⋯ }
          (unop X))
        S ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) S)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
        (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op) ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) (op (unop S)))

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 : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ Functor.obj (J.diagram (J.plusObj P) (unop X)) S)
    (NatTrans.app
      (J.diagramNatTrans
        {
          app := fun (X : Cᵒᵖ) ↦
            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 ⊤)),
          naturality := ⋯ }
        (unop X))
      S)
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
      (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
      (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op))

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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
w :
  ∀ (I : (unop S).shape.L),
    NatTrans.app
          (J.diagramNatTrans
            {
              app := fun (X : Cᵒᵖ) ↦
                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 ⊤)),
              naturality := ⋯ }
            (unop X))
          S ≫
        Multiequalizer.ι ((unop S).index (J.plusObj P)) I =
      CategoryStruct.comp (Y := multiequalizer ((unop S).index (J.plusObj P)))
        (CategoryStruct.comp (Y :=
          multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
          (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
          (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op))
        (Multiequalizer.ι ((unop S).index (J.plusObj P)) I)
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ Functor.obj (J.diagram (J.plusObj P) (unop X)) S)
    (NatTrans.app
      (J.diagramNatTrans
        {
          app := fun (X : Cᵒᵖ) ↦
            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 ⊤)),
          naturality := ⋯ }
        (unop X))
      S)
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
      (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
      (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op))

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

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)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
w :
  Multiequalizer.ι ((unop S).index P) I ≫
      NatTrans.app
        {
          app := fun (X : Cᵒᵖ) ↦
            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 ⊤)),
          naturality := ⋯ }
        (op I.Y) =
    CategoryStruct.comp (Y := multiequalizer ((unop S).index (J.plusObj P)))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
        (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op))
      (Multiequalizer.ι ((unop S).index (J.plusObj P)) I)
⊢ NatTrans.app
        (J.diagramNatTrans
          {
            app := fun (X : Cᵒᵖ) ↦
              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 ⊤)),
            naturality := ⋯ }
          (unop X))
        S ≫
      Multiequalizer.ι ((unop S).index (J.plusObj P)) I =
    CategoryStruct.comp (Y := multiequalizer ((unop S).index (J.plusObj P)))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
        (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op))
      (Multiequalizer.ι ((unop S).index (J.plusObj P)) I)

Tactic:
erw [Multiequalizer.lift_ι]

Premises used: 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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
w :
  Multiequalizer.ι ((unop S).index P) I ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P I.Y) (op ⊤)) =
    colimit.ι (J.diagram P (unop X)) S ≫ (J.plusObj P).map (Cover.Arrow.map I e.op.unop).f.op
⊢ Multiequalizer.ι ((unop S).index P) I ≫
      NatTrans.app
        {
          app := fun (X : Cᵒᵖ) ↦
            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 ⊤)),
          naturality := ⋯ }
        (op I.Y) =
    CategoryStruct.comp (Y := multiequalizer ((unop S).index (J.plusObj P)))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
        (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op))
      (Multiequalizer.ι ((unop S).index (J.plusObj P)) I)

Tactic:
simp only [unop_op, op_unop, diagram_map, Category.assoc, limit.lift_π,
    Multifork.ofι_π_app]

Premises used: CategoryTheory.Category.assoc, Opposite.op_unop, CategoryTheory.GrothendieckTopology.diagram_map, Opposite.unop_op, CategoryTheory.Limits.Multifork.ofι_π_app, CategoryTheory.Limits.limit.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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
w :
  Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ ((unop S).index (J.plusObj P)).left I)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op) ≫
      colimit.ι (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))))
    (CategoryStruct.comp (Y :=
      ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op ⋙
            J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y))).obj
        S)
      (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        (Functor.obj (J.diagram P (unop X)) S)
        (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
          Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1))
        ⋯)
      (colimit.ι (J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y)))
        ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)))
⊢ Multiequalizer.ι ((unop S).index P) I ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P I.Y) (op ⊤)) =
    colimit.ι (J.diagram P (unop X)) S ≫ (J.plusObj P).map (Cover.Arrow.map I e.op.unop).f.op

Tactic:
erw [← colimit.w _ ee.op, ι_colimMap_assoc, colimit.ι_pre, diagramPullback_app,
    ← Category.assoc, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.op, CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.colimit.ι_pre, CategoryTheory.GrothendieckTopology.diagramPullback_app, CategoryTheory.Limits.colimit.w
-- 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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
w :
  Eq (α :=
    Functor.obj (J.diagram P (unop X)) S ⟶
      Functor.obj (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op))
    (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
      (Functor.obj (J.diagram P (unop X)) S)
      (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
        Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1))
      ⋯)
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ ((unop S).index (J.plusObj P)).left I)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op) ≫
      colimit.ι (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))))
    (CategoryStruct.comp (Y :=
      ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op ⋙
            J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y))).obj
        S)
      (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        (Functor.obj (J.diagram P (unop X)) S)
        (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
          Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1))
        ⋯)
      (colimit.ι (J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y)))
        ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)))

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 : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ Eq (α :=
    Functor.obj (J.diagram P (unop X)) S ⟶
      Functor.obj (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op))
    (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
      (Functor.obj (J.diagram P (unop X)) S)
      (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
        Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1))
      ⋯)

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

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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
w :
  ∀ (II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L),
    Eq (α :=
      Functor.obj (J.diagram P (unop X)) S ⟶
        ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II)
      (CategoryStruct.comp (Y :=
        multiequalizer ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P))
        (CategoryStruct.comp (Y :=
          multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
          (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op))
        (Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II))
      (CategoryStruct.comp (Y :=
        multiequalizer ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P))
        (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
          (Functor.obj (J.diagram P (unop X)) S)
          (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
            Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1))
          ⋯)
        (Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II))
⊢ Eq (α :=
    Functor.obj (J.diagram P (unop X)) S ⟶
      Functor.obj (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op))
    (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
      (Functor.obj (J.diagram P (unop X)) S)
      (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
        Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1))
      ⋯)

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

Premises used: CategoryTheory.Limits.Multiequalizer.hom_ext