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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
haveI :
  ∀ (this : FinCategory (AsSmall (FinCategory.AsType K))),
    PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) K (plusPlusSheaf J D (FD := FD) (CD := CD))
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) K (plusPlusSheaf J D (FD := FD) (CD := CD))

Tactic:
haveI : FinCategory (AsSmall.{t} (FinCategory.AsType K)) := by
    constructor
    · change Fintype (ULift _)
      infer_instance
    · intro j j'
      change Fintype (ULift _)
      infer_instance
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this_1 : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) K (plusPlusSheaf J D (FD := FD) (CD := CD))

Tactic:
@preservesLimitsOfShape_of_equiv _ _ _ _ _ _ _ _ e.symm _ (show _ from ?_)

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this_1 : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
refine :
  PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) (AsSmall (FinCategory.AsType K))
    (plusPlusSheaf J D (FD := FD) (CD := CD))
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) K (plusPlusSheaf J D (FD := FD) (CD := CD))

Tactic:
refine @preservesLimitsOfShape_of_equiv _ _ _ _ _ _ _ _ e.symm _ (show _ from ?_)

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this_1 : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
preservesLimit :
  autoParam
    (∀ {K_1 : AsSmall (FinCategory.AsType K) ⥤ Functor.{v, t, u, w} Cᵒᵖ D},
      PreservesLimit K_1 (plusPlusSheaf J D (FD := FD) (CD := CD)))
    PreservesLimitsOfShape.preservesLimit._autoParam
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) (AsSmall (FinCategory.AsType K))
    (plusPlusSheaf J D (FD := FD) (CD := CD))

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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this_1 : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Functor.{v, t, u, w} Cᵒᵖ D
preservesLimit :
  ∀ {c : Cone F} (hc : IsLimit c),
    Nonempty
      (IsLimit (F := F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD))
        (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) c))
⊢ PreservesLimit F (plusPlusSheaf J D (FD := FD) (CD := CD))

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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this_1 : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Functor.{v, t, u, w} Cᵒᵖ D
S : Cone F
hS : IsLimit S
preservesLimit :
  IsLimit (F := F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD))
    (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) S)
⊢ Nonempty
    (IsLimit (F := F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD))
      (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) S))

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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this_1 : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Functor.{v, t, u, w} Cᵒᵖ D
S : Cone F
hS : IsLimit S
preservesLimit :
  IsLimit (F := (F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD)) ⋙ sheafToPresheaf J D)
    (Functor.mapCone (sheafToPresheaf J D) (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) S))
⊢ IsLimit (F := F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD))
    (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) S)

Tactic:
apply isLimitOfReflects (sheafToPresheaf J D)

Premises used: CategoryTheory.Limits.isLimitOfReflects, CategoryTheory.sheafToPresheaf
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this_1 : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Functor.{v, t, u, w} Cᵒᵖ D
S : Cone F
hS : IsLimit S
⊢ ReflectsLimitsOfShape (AsSmall (FinCategory.AsType K)) (forget D (FC := FD) (CC := CD))

Tactic:
have : ReflectsLimitsOfShape (AsSmall.{t} (FinCategory.AsType K)) (forget D) :=
    reflectsLimitsOfShape_of_reflectsIsomorphisms
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : Equivalence.{w', t, w', t} K (AsSmall (FinCategory.AsType K)) :=
  Equivalence.trans (Equivalence.symm (FinCategory.equivAsType K)) AsSmall.equiv
this_1 : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
this_2 : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Functor.{v, t, u, w} Cᵒᵖ D
S : Cone F
hS : IsLimit S
this : ReflectsLimitsOfShape (AsSmall (FinCategory.AsType K)) (forget D (FC := FD) (CC := CD))
⊢ IsLimit (F := (F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD)) ⋙ sheafToPresheaf J D)
    (Functor.mapCone (sheafToPresheaf J D) (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) S))

Tactic:
apply isLimitOfPreserves (J.sheafification D) hS

Premises used: CategoryTheory.GrothendieckTopology.sheafification, CategoryTheory.Limits.isLimitOfPreserves
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
inst_14 : HasFiniteLimits.{t, w} D
h :
  ∀ (J_1 : Type t) {𝒥 : SmallCategory J_1} (x : FinCategory J_1),
    PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) J_1 (plusPlusSheaf J D (FD := FD) (CD := CD))
⊢ PreservesFiniteLimits (C := Functor.{v, t, u, w} Cᵒᵖ D) (plusPlusSheaf J D (FD := FD) (CD := CD))

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{t}
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
K : Type w'
inst_9 : SmallCategory K
inst_10 : FinCategory K
inst_11 : HasLimitsOfShape.{w', w', t, w} K D
inst_12 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_13 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
inst_14 : HasFiniteLimits.{t, w} D
J_1 : Type t
𝒥 : SmallCategory J_1
x : FinCategory J_1
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) J_1 (plusPlusSheaf J D (FD := FD) (CD := CD))

Tactic:
infer_instance
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
P : Functor.{v, t, u, w} Cᵒᵖ D
⊢ Eq (α :=
    Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P ⟶
      Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P))
    (CategoryStruct.comp (Y := Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafToPresheaf J D) P)
      (NatTrans.app (Adjunction.unit (plusPlusAdjunction J D (FD := FD) (CD := CD))) P)
      (Functor.map (sheafToPresheaf J D)
        (NatTrans.app
          (Iso.hom
            (Adjunction.leftAdjointUniq (plusPlusAdjunction J D (FD := FD) (CD := CD)) (sheafificationAdjunction J D)))
          P)))
    (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P)

Tactic:
Adjunction.unit_leftAdjointUniq_hom_app (plusPlusAdjunction J D) (sheafificationAdjunction J D)
      P

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.plusPlusAdjunction, CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
P : Functor.{v, t, u, w} Cᵒᵖ D
h :
  (P ⟶ sheafify J P) =
      (Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P ⟶
        Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P)) →
    P = Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P →
      J.sheafify P = Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafToPresheaf J D) P →
        Eq (α := (P : Functor.{v, t, u, w} Cᵒᵖ D) → P ⟶ J.sheafify P) J.toSheafify
          (NatTrans.app (Adjunction.unit (plusPlusAdjunction J D (FD := FD) (CD := CD))))
⊢ Eq (α := P ⟶ sheafify J P)
    (CategoryStruct.comp (Y := J.sheafify P) (J.toSheafify P)
        (Iso.hom (plusPlusIsoSheafify J D (FD := FD) (CD := CD) P)) :
      P ⟶ sheafify J P)
    (toSheafify J P : P ⟶ sheafify J P)

Tactic:
convert!
    Adjunction.unit_leftAdjointUniq_hom_app (plusPlusAdjunction J D) (sheafificationAdjunction J D)
      P

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.plusPlusAdjunction, CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
P : Functor.{v, t, u, w} Cᵒᵖ D
e_1 :
  (P ⟶ sheafify J P) =
    (Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P ⟶
      Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P))
e_3 : P = Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P
e_4 : J.sheafify P = Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafToPresheaf J D) P
h :
  ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D),
    Eq (α := P ⟶ J.sheafify P) (J.toSheafify P)
      (NatTrans.app (Adjunction.unit (plusPlusAdjunction J D (FD := FD) (CD := CD))) P)
⊢ Eq (α := (P : Functor.{v, t, u, w} Cᵒᵖ D) → P ⟶ J.sheafify P) J.toSheafify
    (NatTrans.app (Adjunction.unit (plusPlusAdjunction J D (FD := FD) (CD := CD))))

Tactic:
ext1 P
-- 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 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
inst_8 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
P_1 : Functor.{v, t, u, w} Cᵒᵖ D
e_1 :
  (P_1 ⟶ sheafify J P_1) =
    (Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P_1 ⟶
      Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P_1))
e_3 : P_1 = Functor.obj (𝟭 (Functor.{v, t, u, w} Cᵒᵖ D)) P_1
e_4 : J.sheafify P_1 = Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafToPresheaf J D) P_1
P : Functor.{v, t, u, w} Cᵒᵖ D
h : J.toPlus P ≫ J.plusMap (J.toPlus P) = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ 𝟙 (J.sheafify P)
⊢ Eq (α := P ⟶ J.sheafify P) (J.toSheafify P)
    (NatTrans.app (Adjunction.unit (plusPlusAdjunction J D (FD := FD) (CD := CD))) P)

Tactic:
dsimp [GrothendieckTopology.toSheafify, plusPlusAdjunction]

Premises used: CategoryTheory.GrothendieckTopology.toSheafify, CategoryTheory.plusPlusAdjunction