awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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
k_1 : K
k : (J.Cover (unop X))ᵒᵖ
⊢ Eq (α :=
    multiequalizer ((unop k).index (limit F)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
    (CategoryStruct.comp (Y := Functor.obj (limit (F ⋙ J.diagramFunctor D (unop X))) k)
        (NatTrans.app
          (limit.lift (F ⋙ J.diagramFunctor D (unop X)) (Functor.mapCone (J.diagramFunctor D (unop X)) (limit.cone F)))
          k)
        (NatTrans.app (limit.π (F ⋙ J.diagramFunctor D (unop X)) k_1) k ≫
          colimit.ι (Functor.flip (F ⋙ J.diagramFunctor D (unop X)) ⋙ Functor.obj (evaluation K D) k_1) k) :
      multiequalizer ((unop k).index (limit F)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
    (NatTrans.app (J.diagramNatTrans (limit.π F k_1) (unop X)) k ≫ colimit.ι (J.diagram (F.obj k_1) (unop X)) k :
      Functor.obj (J.diagram (limit F) (unop X)) k ⟶
        colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
have preservesLimit : Eq (α :=
  multiequalizer ((unop k).index (limit F)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
  (NatTrans.app (NatTrans.app (Cone.π (Functor.mapCone (J.diagramFunctor D (unop X)) (limit.cone F))) k_1) k ≫
      colimit.ι (Functor.flip (F ⋙ J.diagramFunctor D (unop X)) ⋙ Functor.obj (evaluation K D) k_1) k :
    multiequalizer ((unop k).index (limit F)) ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
  (NatTrans.app (J.diagramNatTrans (limit.π F k_1) (unop X)) k ≫ colimit.ι (J.diagram (F.obj k_1) (unop X)) k :
    Functor.obj (J.diagram (limit F) (unop X)) k ⟶ colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram (F.obj k_1) (unop X)))
Tactic: rw [← Category.assoc, ← NatTrans.comp_app, limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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)ᵒᵖ
inst_8 : HasFiniteLimits.{t, w} D
inst_9 : PreservesFiniteLimits (forget D (FC := FD) (CC := CD))
inst_10 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
⊢ PreservesFiniteLimits (C := Functor.{v, t, u, w} Cᵒᵖ D) (J.plusFunctor D)
have h : ∀ (J_1 : Type t) {𝒥 : SmallCategory J_1} (x : FinCategory J_1),
  PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) J_1 (J.plusFunctor D)
Tactic: apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{t}
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (hypothesis)
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)ᵒᵖ
inst_8 : HasFiniteLimits.{t, w} D
inst_9 : PreservesFiniteLimits (forget D (FC := FD) (CC := CD))
inst_10 : Functor.ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
K : Type t
𝒥 : SmallCategory K
x : FinCategory K
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) K (J.plusFunctor D)
have this : ReflectsLimitsOfShape K (forget D (FC := FD) (CC := CD))
Tactic: have : ReflectsLimitsOfShape K (forget D) := reflectsLimitsOfShape_of_reflectsIsomorphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (hypothesis)
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
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) K (plusPlusSheaf J D (FD := FD) (CD := CD))
have this : HasLimitsOfShape.{t, t, t, w} (AsSmall (FinCategory.AsType K)) D
Tactic: haveI : HasLimitsOfShape (AsSmall.{t} (FinCategory.AsType K)) D :=
    Limits.hasLimitsOfShape_of_equivalence e
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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
⊢ FinCategory (AsSmall (FinCategory.AsType K))
have fintypeObj : autoParam (Fintype (AsSmall (FinCategory.AsType K))) FinCategory.fintypeObj._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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
fintypeObj : autoParam (Fintype (AsSmall (FinCategory.AsType K))) FinCategory.fintypeObj._autoParam
⊢ FinCategory (AsSmall (FinCategory.AsType K))
have fintypeHom : autoParam ((j j' : AsSmall (FinCategory.AsType K)) → Fintype (j ⟶ j')) FinCategory.fintypeHom._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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
⊢ PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) K (plusPlusSheaf J D (FD := FD) (CD := CD))
have haveI : ∀ (this : FinCategory (AsSmall (FinCategory.AsType K))),
  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
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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))
have refine : PreservesLimitsOfShape (C := Functor.{v, t, u, w} Cᵒᵖ D) (AsSmall (FinCategory.AsType K))
  (plusPlusSheaf J D (FD := FD) (CD := CD))
Tactic: refine @preservesLimitsOfShape_of_equiv _ _ _ _ _ _ _ _ e.symm _ (show _ from ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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) (AsSmall (FinCategory.AsType K))
    (plusPlusSheaf J D (FD := FD) (CD := CD))
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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 F (plusPlusSheaf J D (FD := FD) (CD := CD))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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
⊢ Nonempty
    (IsLimit (F := F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD))
      (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) S))
have preservesLimit : IsLimit (F := F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD)) (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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
⊢ IsLimit (F := F ⋙ plusPlusSheaf J D (FD := FD) (CD := CD))
    (Functor.mapCone (plusPlusSheaf J D (FD := FD) (CD := CD)) S)
have 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))
Tactic: apply isLimitOfReflects (sheafToPresheaf J D)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (hypothesis)
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
⊢ 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))
have this₁ : ReflectsLimitsOfShape (AsSmall (FinCategory.AsType K)) (forget D (FC := FD) (CC := CD))
Tactic: have : ReflectsLimitsOfShape (AsSmall.{t} (FinCategory.AsType K)) (forget D) :=
    reflectsLimitsOfShape_of_reflectsIsomorphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LeftExact (goal)
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
⊢ PreservesFiniteLimits (C := Functor.{v, t, u, w} Cᵒᵖ D) (plusPlusSheaf J D (FD := FD) (CD := CD))
have 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))
Tactic: apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{t}