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
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).Arrow
⊢ Eq (α := (J.diagram P X ⋙ F).obj W ⟶ ((unop W).index (P ⋙ F)).left i)
    (CategoryStruct.comp (Y := (J.diagram (P ⋙ F) X).obj W)
        (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (W : (J.Cover 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))
                ⋯))
            W :
          (J.diagram P X ⋙ F).obj W ⟶ (J.diagram (P ⋙ F) X).obj W)
        (Multiequalizer.ι ((unop W).index (P ⋙ F)) i :
          multiequalizer ((unop W).index (P ⋙ F)) ⟶ ((unop W).index (P ⋙ F)).left i) :
      (J.diagram P X ⋙ F).obj W ⟶ ((unop W).index (P ⋙ F)).left i)
    (F.map (Multiequalizer.ι ((unop W).index P) i) :
      F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (((unop W).index P).left i))

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
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ᵒᵖ
refine : (J.plusObj P ⋙ F).obj X ≅ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F)
⊢ (J.plusObj P ⋙ F).obj X ≅ (J.plusObj (P ⋙ F)).obj X

Tactic:
refine ?_ ≪≫ HasColimit.isoOfNatIso (J.diagramCompIso F P X.unop)

Premises used: CategoryTheory.GrothendieckTopology.diagramCompIso, Opposite.unop, CategoryTheory.Limits.HasColimit.isoOfNatIso
-- 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ᵒᵖ
⊢ (J.plusObj P ⋙ F).obj X ≅ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F)

Tactic:
refine
        (isColimitOfPreserves F
              (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
          (colimit.isColimit _)

Premises used: CategoryTheory.Limits.colimit.isColimit, Opposite.unop, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.GrothendieckTopology.diagram, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a : NatTrans.app (Cocone.ι (colimit.cocone (J.diagram P (unop X) ⋙ F))) W
| (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
      (F.map (colimit.ι (J.diagram P (unop X)) W))
      (Iso.hom
        (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X))))
          (colimit.isColimit (J.diagram P (unop X) ⋙ F)))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X) ⋙ F))

Tactic:
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, 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
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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a :
  F.map
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) W)
      (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)))
| CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
    (F.map (colimit.ι (J.diagram P (unop X)) W))
    (CategoryStruct.comp (Y := F.obj (colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))))
      (F.map (colimMap (J.diagramPullback P f.unop)))
      (F.map (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op)))

Tactic:
simp only [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a :
  (F.map
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
        (colimit.ι (J.diagram P (unop X)) W)
        (colimit.desc (J.diagram P (unop X))
            (obj (Cocone.precompose (J.diagramPullback P f.unop))
              (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))) ≫
          colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
            (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y)))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
| F.map
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) W)
      (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:
dsimp [colimMap, IsColimit.map, colimit.pre]

Premises used: CategoryTheory.Limits.colimMap, CategoryTheory.Limits.colimit.pre, CategoryTheory.Limits.IsColimit.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
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a :
  (F.map
      ((obj (Cocone.precompose (J.diagramPullback P f.unop))
                (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))).ι.app
          W ≫
        colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
          (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
| (F.map
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
        (colimit.ι (J.diagram P (unop X)) W)
        (colimit.desc (J.diagram P (unop X))
            (obj (Cocone.precompose (J.diagramPullback P f.unop))
              (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))) ≫
          colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
            (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y)))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))

Tactic:
simp only [colimit.ι_desc_assoc, colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.ι_desc_assoc
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a :
  (F.map
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
        (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯ ≫
          colimit.ι ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)) W)
        (colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
          (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y)))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
| (F.map
      ((obj (Cocone.precompose (J.diagramPullback P f.unop))
                (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))).ι.app
          W ≫
        colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
          (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))

Tactic:
dsimp [Cocone.precompose]

Premises used: CategoryTheory.Limits.Cocone.precompose
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a :
  F.map
    (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index P))
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯)
      (NatTrans.app (Cocone.ι (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y))))) W))
| (F.map
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
        (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯ ≫
          colimit.ι ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)) W)
        (colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
          (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y)))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))

Tactic:
simp only [Category.assoc, colimit.ι_desc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_desc
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a :
  F.map
    (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index P))
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯)
      (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
| F.map
    (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index P))
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯)
      (NatTrans.app (Cocone.ι (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y))))) W))

Tactic:
dsimp [Cocone.whisker]

Premises used: CategoryTheory.Limits.Cocone.whisker
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a :
  CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
    (F.map
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯))
    (F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
| F.map
    (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index P))
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯)
      (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))

Tactic:
rw [F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a :
  CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
    (F.map
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯))
    (F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
| CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
    (F.map (colimit.ι (J.diagram P (unop X)) W))
    (CategoryStruct.comp (Y := F.obj (colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))))
      (F.map (colimMap (J.diagramPullback P f.unop)))
      (F.map (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op)))

Tactic:
simp only [← F.map_comp]
        dsimp [colimMap, IsColimit.map, colimit.pre]
        simp only [colimit.ι_desc_assoc, colimit.ι_desc]
        dsimp [Cocone.precompose]
        simp only [Category.assoc, colimit.ι_desc]
        dsimp [Cocone.whisker]
        rw [F.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.ι_desc_assoc, CategoryTheory.Limits.colimMap, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.colimit.pre, CategoryTheory.Limits.IsColimit.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
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
a : NatTrans.app (Cocone.ι (colimit.cocone (J.diagram P (unop Y) ⋙ F))) (op ((unop W).pullback f.unop))
| (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
      (F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
      (Iso.hom
        (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y))))
          (colimit.isColimit (J.diagram P (unop Y) ⋙ F)))) :
    F.obj (multiequalizer (((unop W).pullback f.unop).index P)) ⟶
      colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y) ⋙ F))

Tactic:
erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P Y.unop))).fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.colimit.isColimit, Opposite.unop, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.GrothendieckTopology.diagram