awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ Eq (α := F.obj (obj (J.diagram P (unop X)) W) ⟶ (J.plusObj (P ⋙ F)).obj X)
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))
        (NatTrans.app (Cocone.ι (colimit.cocone (J.diagram P (unop X) ⋙ F))) W :
          obj (J.diagram P (unop X) ⋙ F) W ⟶
            obj
              (obj (const (J.Cover (unop X))ᵒᵖ)
                (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
                  (colimit.cocone (J.diagram P (unop X) ⋙ F))))
              W)
        (Iso.hom
            (HasColimit.isoOfNatIso
              (NatIso.ofComponents
                (fun (W : (J.Cover (unop X))ᵒᵖ) ↦
                  Iso.trans (Y := limit (((unop W).index P).multicospan ⋙ F))
                    (IsLimit.conePointUniqueUpToIso
                      (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
                      (limit.isLimit (((unop W).index P).multicospan ⋙ F)))
                    (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm))
                ⋯)) :
          colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F) ⟶ (J.plusObj (P ⋙ F)).obj X) :
      F.obj (obj (J.diagram P (unop X)) W) ⟶ (J.plusObj (P ⋙ F)).obj X)
    (CategoryStruct.comp (Y := obj (J.diagram (P ⋙ F) (unop X)) W)
        (CategoryStruct.comp (Y := limit (((unop W).index P).multicospan ⋙ F))
          (Iso.hom
            (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan))
              (limit.isLimit (((unop W).index P).multicospan ⋙ F))))
          (Iso.hom (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm)))
        (colimit.ι (J.diagram (P ⋙ F) (unop X)) W) :
      obj (J.diagram P (unop X) ⋙ F) W ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (P ⋙ F) (unop X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : Functor.{v_1, v_2, u_1, u_2} D E
η : F ⟶ G
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan G
w :
  ∀ (X : Cᵒᵖ),
    Eq (α := (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
      (NatTrans.app ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P)) X :
        (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
      (NatTrans.app
          (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
            (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
            (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)))
          X :
        (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
⊢ Eq (α := J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ G))
    ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ G))
    (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
        (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)) :
      J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ G))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : Functor.{v_1, v_2, u_1, u_2} D E
η : F ⟶ G
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
w :
  ∀ (j : (J.Cover (unop X))ᵒᵖ),
    Eq (α := obj (J.diagram P (unop X) ⋙ F) j ⟶ (J.plusObj (P ⋙ G)).obj X)
      (CategoryStruct.comp (Y :=
        obj
          (obj (const (J.Cover (unop X))ᵒᵖ)
            (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
              (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
          j)
        (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
        (NatTrans.app ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P)) X))
      (CategoryStruct.comp (Y :=
        obj
          (obj (const (J.Cover (unop X))ᵒᵖ)
            (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
              (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
          j)
        (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
        (NatTrans.app
          (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
            (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
            (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)))
          X))
⊢ Eq (α := (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
    (NatTrans.app ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P)) X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
    (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)))
        X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)

Tactic:
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.colimit.isColimit, Opposite.unop, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.GrothendieckTopology.diagram
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ D
η : P ⟶ Q
w :
  ∀ (X : Cᵒᵖ),
    Eq (α := (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
      (NatTrans.app (whiskerRight (J.plusMap η) F ≫ Iso.hom (J.plusCompIso F Q)) X :
        (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
      (NatTrans.app
          (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
            (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
            (J.plusMap (whiskerRight η F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (Q ⋙ F)))
          X :
        (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
⊢ Eq (α := J.plusObj P ⋙ F ⟶ J.plusObj (Q ⋙ F))
    (whiskerRight (J.plusMap η) F ≫ Iso.hom (J.plusCompIso F Q) : J.plusObj P ⋙ F ⟶ J.plusObj (Q ⋙ F))
    (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
        (J.plusMap (whiskerRight η F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (Q ⋙ F)) :
      J.plusObj P ⋙ F ⟶ J.plusObj (Q ⋙ F))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ D
η : P ⟶ Q
X : Cᵒᵖ
w :
  ∀ (j : (J.Cover (unop X))ᵒᵖ),
    Eq (α := obj (J.diagram P (unop X) ⋙ F) j ⟶ (J.plusObj (Q ⋙ F)).obj X)
      (CategoryStruct.comp (Y :=
        obj
          (obj (const (J.Cover (unop X))ᵒᵖ)
            (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
              (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
          j)
        (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
        (NatTrans.app (whiskerRight (J.plusMap η) F ≫ Iso.hom (J.plusCompIso F Q)) X))
      (CategoryStruct.comp (Y :=
        obj
          (obj (const (J.Cover (unop X))ᵒᵖ)
            (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
              (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
          j)
        (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
        (NatTrans.app
          (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
            (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
            (J.plusMap (whiskerRight η F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (Q ⋙ F)))
          X))
⊢ Eq (α := (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
    (NatTrans.app (whiskerRight (J.plusMap η) F ≫ Iso.hom (J.plusCompIso F Q)) X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
    (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (whiskerRight η F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (Q ⋙ F)))
        X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)

Tactic:
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.colimit.isColimit, Opposite.unop, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.GrothendieckTopology.diagram
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
a : (unop W).shape.L
⊢ Eq (α := F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (Q.obj (op a.Y)))
    (CategoryStruct.comp (Y := F.obj (multiequalizer ((unop W).index Q)))
      (F.map
        (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
          (fun (x : (unop W).Arrow) ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯))
      (F.map (Multiequalizer.ι ((unop W).index Q) a)))
    (F.map (Multiequalizer.ι ((unop W).index P) a) ≫ F.map (η.app (op a.Y)))

Tactic:
simp only [← F.map_comp, Multiequalizer.lift_ι]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Limits.Multiequalizer.lift_ι
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
w :
  ∀ (x : Cᵒᵖ),
    Eq (α := (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)
      (NatTrans.app
          (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
            (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F)))
          x :
        (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)
      (NatTrans.app (J.toPlus (P ⋙ F)) x : (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)
⊢ Eq (α := P ⋙ F ⟶ J.plusObj (P ⋙ F))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F)) :
      P ⋙ F ⟶ J.plusObj (P ⋙ F))
    (J.toPlus (P ⋙ F) : P ⋙ F ⟶ J.plusObj (P ⋙ F))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x : Cᵒᵖ
w :
  Eq (α := F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y := F.obj ((J.plusObj P).obj x))
        (F.map
            (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 ⊤))) :
          F.obj (P.obj x) ⟶ F.obj ((J.plusObj P).obj x))
        (NatTrans.app (Iso.hom (J.plusCompIso F P)) x : (J.plusObj P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
        (Cover.toMultiequalizer ⊤ (P ⋙ F)) (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
⊢ Eq (α := (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)
    (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F)))
        x :
      (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)
    (NatTrans.app (J.toPlus (P ⋙ F)) x : (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)

Tactic:
dsimp [toPlus]

Premises used: CategoryTheory.GrothendieckTopology.toPlus
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x : Cᵒᵖ
w :
  Eq (α := F.obj (P.obj x) ⟶ obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
    (CategoryStruct.comp (Y :=
        F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
        (F.map (Cover.toMultiequalizer ⊤ P) :
          F.obj (P.obj x) ⟶
            F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
        (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop x))) (op ⊤) :
          obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x) ⋙ F) (op ⊤) ⟶
            obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
      F.obj (P.obj x) ⟶ obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
    (Cover.toMultiequalizer ⊤ (P ⋙ F) :
      (P ⋙ F).obj (op (unop x)) ⟶
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
⊢ Eq (α := F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y := obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
        (CategoryStruct.comp (Y :=
            F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
            (F.map (Cover.toMultiequalizer ⊤ P) :
              F.obj (P.obj x) ⟶
                F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
            (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop x))) (op ⊤) :
              obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x) ⋙ F) (op ⊤) ⟶
                obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
          F.obj (P.obj x) ⟶ obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
        (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤) :
          obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤) ⟶
            colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x))) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
        (Cover.toMultiequalizer ⊤ (P ⋙ F)) (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x : Cᵒᵖ
a : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L
⊢ F.map
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P))
        (Cover.toMultiequalizer ⊤ P) (Multiequalizer.ι (Cover.index (unop (op ⊤)) P) a)) =
    CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
      (Cover.toMultiequalizer ⊤ (P ⋙ F)) (Multiequalizer.ι (Cover.index ⊤ (P ⋙ F)) a)

Tactic:
simp only [unop_op, limit.lift_π, Multifork.ofι_π_app, Functor.comp_obj, Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_obj, Opposite.unop_op, CategoryTheory.Limits.Multifork.ofι_π_app, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
⊢ Eq (α := P ⋙ F ⟶ J.plusObj P ⋙ F)
    (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (J.toPlus (P ⋙ F) : P ⋙ F ⟶ J.plusObj (P ⋙ F))
        (Iso.inv (J.plusCompIso F P) : J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F) :
      P ⋙ F ⟶ J.plusObj P ⋙ F)
    (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Sites.CompatiblePlus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)
hγ :
  Eq (α := P ⋙ F ⟶ J.plusObj P ⋙ F)
    (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (J.toPlus (P ⋙ F) : P ⋙ F ⟶ J.plusObj (P ⋙ F))
        (Iso.inv (J.plusCompIso F P) : J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F) :
      P ⋙ F ⟶ J.plusObj P ⋙ F)
    (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
⊢ Eq (α := J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F) (Iso.inv (J.plusCompIso F P) : J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F)
    (J.plusLift (whiskerRight (J.toPlus P) F) hP : J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F)

Tactic:
apply J.plusLift_unique

Premises used: CategoryTheory.GrothendieckTopology.plusLift_unique