awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape.{s, s, t, w} K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
k : K
⊢ Eq (α := (J.plusObj (limit F)).obj (op X) ⟶ (J.plusObj (F.obj k)).obj (op X))
    (NatTrans.app (J.plusMap (limit.π F k)) (op X))
    (CategoryStruct.comp (Y := colimit (limit (F ⋙ J.diagramFunctor D X)))
      (Iso.hom
          (HasColimit.isoOfNatIso
            (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F))
              (limit.isLimit (F ⋙ J.diagramFunctor D X)))) :
        (J.plusObj (limit F)).obj (op X) ⟶ colimit (limit (F ⋙ J.diagramFunctor D X)))
      (CategoryStruct.comp (Y := limit (colimit (F ⋙ J.diagramFunctor D X).flip))
          (Iso.hom (colimitLimitIso (F ⋙ J.diagramFunctor D X)) :
            colimit (limit (F ⋙ J.diagramFunctor D X)) ⟶ limit (colimit (F ⋙ J.diagramFunctor D X).flip))
          (CategoryStruct.comp (Y := limit (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)))
              (Iso.inv
                (HasLimit.isoOfNatIso
                  (Iso.symm
                    (NatIso.ofComponents
                      (fun (k : K) ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯))))
              (limit.π (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X)) k) :
            limit (colimit (F ⋙ J.diagramFunctor D X).flip) ⟶ (J.plusObj (F.obj k)).obj (op X)) :
        colimit (limit (F ⋙ J.diagramFunctor D X)) ⟶ (J.plusObj (F.obj k)).obj (op X)))

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

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape.{s, s, t, w} K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
e_a :
  Eq (α := multiequalizer ((unop j).index (F.obj k)) ⟶ colimit (J.diagram (F.obj k) X))
    (colimit.ι (J.diagram (F.obj k) X) j : (J.diagram (F.obj k) X).obj j ⟶ colimit (J.diagram (F.obj k) X))
    (CategoryStruct.comp (Y := (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
        (NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
          ((F ⋙ J.diagramFunctor D X).flip.obj j).obj k ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
        (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) :
          (colimit (F ⋙ J.diagramFunctor D X).flip).obj k ⟶ (J.plusObj (F.obj k)).obj (op X)) :
      ((F ⋙ J.diagramFunctor D X).obj k).obj j ⟶ (J.plusObj (F.obj k)).obj (op X))
⊢ Eq (α := multiequalizer ((unop j).index (limit F)) ⟶ (J.plusObj (F.obj k)).obj (op X))
    (Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
          (fun (x : (unop j).Arrow) ↦
            Multiequalizer.ι ((unop j).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
          ⋯ ≫
        colimit.ι (J.diagram (F.obj k) X) j :
      multiequalizer ((unop j).index (limit F)) ⟶ colimit (J.diagram (F.obj k) X))
    (NatTrans.app (NatTrans.app (Cone.π (Functor.mapCone (J.diagramFunctor D X) (limit.cone F))) k) j ≫
        CategoryStruct.comp (Y := (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
          (NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
            ((F ⋙ J.diagramFunctor D X).flip.obj j).obj k ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
          (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) :
            (colimit (F ⋙ J.diagramFunctor D X).flip).obj k ⟶ (J.plusObj (F.obj k)).obj (op X)) :
      multiequalizer ((unop j).index (limit F)) ⟶ (J.plusObj (F.obj k)).obj (op X))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape.{s, s, t, w} K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
e_a :
  Eq (α := (J.diagram (F.obj k) X).obj j ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
    (CategoryStruct.comp (Y := colimit (J.diagram (F.obj k) X))
        (colimit.ι (J.diagram (F.obj k) X) j : (J.diagram (F.obj k) X).obj j ⟶ colimit (J.diagram (F.obj k) X))
        (Iso.inv (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) :
          colimit (J.diagram (F.obj k) X) ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k) :
      (J.diagram (F.obj k) X).obj j ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
    (NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
      ((F ⋙ J.diagramFunctor D X).flip.obj j).obj k ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
⊢ Eq (α := multiequalizer ((unop j).index (F.obj k)) ⟶ colimit (J.diagram (F.obj k) X))
    (colimit.ι (J.diagram (F.obj k) X) j : (J.diagram (F.obj k) X).obj j ⟶ colimit (J.diagram (F.obj k) X))
    (CategoryStruct.comp (Y := (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
        (NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
          ((F ⋙ J.diagramFunctor D X).flip.obj j).obj k ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
        (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) :
          (colimit (F ⋙ J.diagramFunctor D X).flip).obj k ⟶ (J.plusObj (F.obj k)).obj (op X)) :
      ((F ⋙ J.diagramFunctor D X).obj k).obj j ⟶ (J.plusObj (F.obj k)).obj (op X))

Tactic:
rw [← Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape.{s, s, t, w} K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
e_a :
  Eq (α := (J.diagram (F.obj k) X).obj j ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
    (NatTrans.app
        (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation K D) k) (colimit.cocone (F ⋙ J.diagramFunctor D X).flip)))
        j :
      (J.diagram (F.obj k) X).obj j ⟶
        Functor.obj
          (Functor.obj (Functor.const (J.Cover X)ᵒᵖ)
            (Cocone.pt (F := J.diagram (F.obj k) X)
              (Functor.mapCocone (Functor.obj (evaluation K D) k) (colimit.cocone (F ⋙ J.diagramFunctor D X).flip) :
                Cocone ((F ⋙ J.diagramFunctor D X).flip ⋙ Functor.obj (evaluation K D) k))))
          j)
    (NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
      ((F ⋙ J.diagramFunctor D X).flip.obj j).obj k ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
⊢ Eq (α := (J.diagram (F.obj k) X).obj j ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
    (CategoryStruct.comp (Y := colimit (J.diagram (F.obj k) X))
        (colimit.ι (J.diagram (F.obj k) X) j : (J.diagram (F.obj k) X).obj j ⟶ colimit (J.diagram (F.obj k) X))
        (Iso.inv (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) :
          colimit (J.diagram (F.obj k) X) ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k) :
      (J.diagram (F.obj k) X).obj j ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
    (NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
      ((F ⋙ J.diagramFunctor D X).flip.obj j).obj k ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)

Tactic:
erw [colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape.{s, s, t, w} K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ Eq (α := (J.diagram (F.obj k) X).obj j ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)
    (NatTrans.app
        (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation K D) k) (colimit.cocone (F ⋙ J.diagramFunctor D X).flip)))
        j :
      (J.diagram (F.obj k) X).obj j ⟶
        Functor.obj
          (Functor.obj (Functor.const (J.Cover X)ᵒᵖ)
            (Cocone.pt (F := J.diagram (F.obj k) X)
              (Functor.mapCocone (Functor.obj (evaluation K D) k) (colimit.cocone (F ⋙ J.diagramFunctor D X).flip) :
                Cocone ((F ⋙ J.diagramFunctor D X).flip ⋙ Functor.obj (evaluation K D) k))))
          j)
    (NatTrans.app (colimit.ι (F ⋙ J.diagramFunctor D X).flip j) k :
      ((F ⋙ J.diagramFunctor D X).flip.obj j).obj k ⟶ (colimit (F ⋙ J.diagramFunctor D X).flip).obj k)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
preservesLimit :
  autoParam (∀ {K_1 : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D}, PreservesLimit K_1 (J.plusFunctor D))
    PreservesLimitsOfShape.preservesLimit._autoParam
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) K (J.plusFunctor D)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
preservesLimit : ∀ (k : Cᵒᵖ), PreservesLimit F (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) k)
⊢ PreservesLimit F (J.plusFunctor D)

Tactic:
apply preservesLimit_of_evaluation

Premises used: CategoryTheory.Limits.preservesLimit_of_evaluation
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : Cᵒᵖ
preservesLimit :
  IsLimit (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
    (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))
⊢ PreservesLimit F (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)

Tactic:
apply preservesLimit_of_preserves_limit_cone (limit.isLimit F)

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : Cᵒᵖ
preservesLimit :
  ∀ (s : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)) (j : K),
    CategoryStruct.comp (Y :=
        Cone.pt (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
          (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F)))
        ((fun (S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)) ↦
              (liftToPlusObjLimitObj (FD := FD) (CD := CD) F (unop X) S :
                S.pt ⟶ (J.plusObj (limit F)).obj (op (unop X))))
            s :
          s.pt ⟶ (J.plusObj (limit F)).obj (op (unop X)))
        (NatTrans.app (Cone.π (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))) j :
          Functor.obj
              (Functor.obj (Functor.const K)
                (Cone.pt (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
                  (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))))
              j ⟶
            (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X).obj j) =
      s.π.app j
preservesLimit₁ :
  ∀ (s : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X))
    (m :
      s.pt ⟶
        Cone.pt (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
          (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))),
    (∀ (j : K),
        m ≫
            NatTrans.app (Cone.π (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F)))
              j =
          s.π.app j) →
      m =
        (fun (S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)) ↦
            (liftToPlusObjLimitObj (FD := FD) (CD := CD) F (unop X) S : S.pt ⟶ (J.plusObj (limit F)).obj (op (unop X))))
          s
⊢ IsLimit (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
    (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))

Tactic:
refine ⟨fun S => liftToPlusObjLimitObj F X.unop S, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : Cᵒᵖ
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
k : K
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
        (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F)))
      ((fun (S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)) ↦
            (liftToPlusObjLimitObj (FD := FD) (CD := CD) F (unop X) S : S.pt ⟶ (J.plusObj (limit F)).obj (op (unop X))))
          S :
        S.pt ⟶ (J.plusObj (limit F)).obj (op (unop X)))
      (NatTrans.app (Cone.π (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))) k :
        Functor.obj
            (Functor.obj (Functor.const K)
              (Cone.pt (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
                (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))))
            k ⟶
          (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X).obj k) =
    S.π.app k

Tactic:
apply liftToPlusObjLimitObj_fac

Premises used: CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst_4 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst_8 : SmallCategory K
inst_9 : FinCategory K
inst_10 : HasLimitsOfShape K D
inst_11 : PreservesLimitsOfShape K (forget D (FC := FD) (CC := CD))
inst_12 : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
X : Cᵒᵖ
S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
m :
  S.pt ⟶
    Cone.pt (F := F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)
      (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))
hm :
  ∀ (j : K),
    m ≫ NatTrans.app (Cone.π (Functor.mapCone (J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) (limit.cone F))) j =
      S.π.app j
preservesLimit :
  m =
    CategoryStruct.comp (Y := limit (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X))
      (limit.lift (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X) S)
      (CategoryStruct.comp (Y :=
        limit (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X)))))
        (Iso.hom
          (HasLimit.isoOfNatIso
            (Iso.symm
              (NatIso.ofComponents
                (fun (k : K) ↦ colimitObjIsoColimitCompEvaluation (Functor.flip (F ⋙ J.diagramFunctor D (unop X))) k)
                ⋯))))
        (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))))
          (Iso.inv (colimitLimitIso (F ⋙ J.diagramFunctor D (unop X))) :
            limit (colimit (J := (J.Cover (unop X))ᵒᵖ) (Functor.flip (F ⋙ J.diagramFunctor D (unop X)))) ⟶
              colimit (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))))
          (Iso.inv
              (HasColimit.isoOfNatIso
                (IsLimit.conePointUniqueUpToIso (isLimitOfPreserves (J.diagramFunctor D (unop X)) (limit.isLimit F))
                  (limit.isLimit (F ⋙ J.diagramFunctor D (unop X))))) :
            colimit (J := (J.Cover (unop X))ᵒᵖ) (limit (F ⋙ J.diagramFunctor D (unop X))) ⟶
              (J.plusObj (limit F)).obj X)))
⊢ m =
    (fun (S : Cone (F ⋙ J.plusFunctor D ⋙ Functor.obj (evaluation Cᵒᵖ D) X)) ↦
        (liftToPlusObjLimitObj (FD := FD) (CD := CD) F (unop X) S : S.pt ⟶ (J.plusObj (limit F)).obj (op (unop X))))
      S

Tactic:
dsimp [liftToPlusObjLimitObj]

Premises used: CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj