awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
inst_3 : CreatesFiniteCoproducts F
x : Type
x_1 : Fintype x
⊢ CreatesLimitsOfShape (Discrete x) F.rightOp
have inst : CreatesColimitsOfShape (Discrete x)ᵒᵖ F
Tactic: apply +allowSynthFailures createsLimitsOfShapeRightOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
inst_3 : CreatesFiniteCoproducts F
x : Type
x_1 : Fintype x
⊢ CreatesLimitsOfShape (Discrete x) F.unop
have inst : CreatesColimitsOfShape (Discrete x)ᵒᵖ F
Tactic: apply +allowSynthFailures createsLimitsOfShapeUnop
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesFiniteProducts F
x : Type
x_1 : Fintype x
⊢ CreatesColimitsOfShape (Discrete x) F.op
have inst : CreatesLimitsOfShape (Discrete x)ᵒᵖ F
Tactic: apply +allowSynthFailures createsColimitsOfShapeOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_3 : CreatesFiniteProducts F
x : Type
x_1 : Fintype x
⊢ CreatesColimitsOfShape (Discrete x) F.leftOp
have inst : CreatesLimitsOfShape (Discrete x)ᵒᵖ F
Tactic: apply +allowSynthFailures createsColimitsOfShapeLeftOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
inst_3 : CreatesFiniteProducts F
x : Type
x_1 : Fintype x
⊢ CreatesColimitsOfShape (Discrete x) F.rightOp
have inst : CreatesLimitsOfShape (Discrete x)ᵒᵖ F
Tactic: apply +allowSynthFailures createsColimitsOfShapeRightOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
inst_3 : CreatesFiniteProducts F
x : Type
x_1 : Fintype x
⊢ CreatesColimitsOfShape (Discrete x) F.unop
have inst : CreatesLimitsOfShape (Discrete x)ᵒᵖ F
Tactic: apply +allowSynthFailures createsColimitsOfShapeUnop
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Filtered (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : UnivLE.{w, w'}
inst_3 : UnivLE.{w₂, w₂'}
inst_4 : PreservesFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x : Category.{w, w₂} J
h : IsFiltered.{w, w₂} J
e : Equivalence.{w', w, w₂', w₂} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J)) J :=
  Equivalence.symm (Equivalence.trans (ShrinkHoms.equivalence J) (Shrink.equivalence (ShrinkHoms.{w₂} J)))
⊢ PreservesColimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F
have this : IsFiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
Tactic: haveI := IsFiltered.of_equivalence e.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Filtered (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : UnivLE.{w, w'}
inst_3 : UnivLE.{w₂, w₂'}
inst_4 : ReflectsFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x : Category.{w, w₂} J
h : IsFiltered.{w, w₂} J
e : Equivalence.{w', w, w₂', w₂} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J)) J :=
  Equivalence.symm (Equivalence.trans (ShrinkHoms.equivalence J) (Shrink.equivalence (ShrinkHoms.{w₂} J)))
⊢ ReflectsColimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F
have this : IsFiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
Tactic: haveI := IsFiltered.of_equivalence e.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Filtered (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : UnivLE.{w, w'}
inst_3 : UnivLE.{w₂, w₂'}
inst_4 : PreservesCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x : Category.{w, w₂} J
h : IsCofiltered.{w, w₂} J
e : Equivalence.{w', w, w₂', w₂} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J)) J :=
  Equivalence.symm (Equivalence.trans (ShrinkHoms.equivalence J) (Shrink.equivalence (ShrinkHoms.{w₂} J)))
⊢ PreservesLimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F
have this : IsCofiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
Tactic: haveI := IsCofiltered.of_equivalence e.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Filtered (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : UnivLE.{w, w'}
inst_3 : UnivLE.{w₂, w₂'}
inst_4 : ReflectsCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x : Category.{w, w₂} J
h : IsCofiltered.{w, w₂} J
e : Equivalence.{w', w, w₂', w₂} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J)) J :=
  Equivalence.symm (Equivalence.trans (ShrinkHoms.equivalence J) (Shrink.equivalence (ShrinkHoms.{w₂} J)))
⊢ ReflectsLimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F
have this : IsCofiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
Tactic: haveI := IsCofiltered.of_equivalence e.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Finite (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesLimitsOfShape J F
have this : PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
Tactic: haveI := preservesSmallestLimits_of_preservesLimits F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Finite (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J F
J : Type
x : SmallCategory J
x_1 : FinCategory J
⊢ PreservesLimitsOfShape J F
have this : PreservesLimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (ULiftHom (ULift.{w, 0} J)) F
Tactic: haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Finite (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J_1 : Type w
inst_3 : SmallCategory J_1
K : Functor.{w, v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Type u
inst_4 : Finite J
inst_5 : PreservesFiniteProducts F
⊢ PreservesLimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F
have obtain : ∀ (n : ℕ) (e : J ≃ Fin n), PreservesLimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Finite (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J_1 : Type w
inst_3 : SmallCategory J_1
K : Functor.{w, v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Type u
inst_4 : Finite J
inst_5 : PreservesFiniteProducts F
n : ℕ
e : J ≃ Fin n
⊢ PreservesLimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F
have this : PreservesLimitsOfShape (Discrete (Fin n)) F
Tactic: have := PreservesFiniteProducts.preserves (F := F) n
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Finite (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsLimitsOfShape J F
have this : ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
Tactic: haveI := reflectsSmallestLimits_of_reflectsLimits F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Finite (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J F
have this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
Tactic: haveI := preservesSmallestColimits_of_preservesColimits F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Finite (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesColimitsOfShape J F
J : Type
x : SmallCategory J
x_1 : FinCategory J
this : Category.{w, w} (ULiftHom (ULift.{w, 0} J)) := ULiftHom.category
⊢ PreservesColimitsOfShape J F
have this₁ : PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (ULiftHom (ULift.{w, 0} J)) F
Tactic: haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Finite (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsColimitsOfShape J F
have this : ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
Tactic: haveI := reflectsSmallestColimits_of_reflectsColimits F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v₁, u} C
D : Type u₂
inst_1 : Category.{u, u₂} D
inst_2 : HasBinaryProducts.{u, u₂} D
inst_3 : HasColimits.{u, u₂} D
inst_4 : ∀ (X : D), PreservesColimits.{u, u, u₂, u₂} (obj prod.functor X)
F : Functor.{v₁, u, u, u₂} C D
J : Type u
inst_5 : Category.{u, u} J
K : J ⥤ Functor.{v₁, u, u, u₂} C D
c : Cocone K
t : IsColimit c
⊢ IsColimit (F := K ⋙ obj prod.functor F) (mapCocone (obj prod.functor F) c)
have apply : {k : C} →
  IsColimit (F := (K ⋙ obj prod.functor F) ⋙ obj (evaluation C D) k)
    (mapCocone (obj (evaluation C D) k) (mapCocone (obj prod.functor F) c))
Tactic: apply evaluationJointlyReflectsColimits _ fun {k} => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v₁, u} C
D : Type u₂
inst_1 : Category.{u, u₂} D
inst_2 : HasBinaryProducts.{u, u₂} D
inst_3 : HasColimits.{u, u₂} D
inst_4 : ∀ (X : D), PreservesColimits.{u, u, u₂, u₂} (obj prod.functor X)
F : Functor.{v₁, u, u, u₂} C D
J : Type u
inst_5 : Category.{u, u} J
K : J ⥤ Functor.{v₁, u, u, u₂} C D
c : Cocone K
t : IsColimit c
k : C
⊢ IsColimit (F := (K ⋙ obj prod.functor F) ⋙ obj (evaluation C D) k)
    (mapCocone (obj (evaluation C D) k) (mapCocone (obj prod.functor F) c))
have change : IsColimit ((obj prod.functor F ⋙ obj (evaluation C D) k).mapCocone c)
Tactic: change IsColimit ((prod.functor.obj F ⋙ (evaluation _ _).obj k).mapCocone c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v₁, u} C
D : Type u₂
inst_1 : Category.{u, u₂} D
inst_2 : HasBinaryProducts.{u, u₂} D
inst_3 : HasColimits.{u, u₂} D
inst_4 : ∀ (X : D), PreservesColimits.{u, u, u₂, u₂} (obj prod.functor X)
F : Functor.{v₁, u, u, u₂} C D
J : Type u
inst_5 : Category.{u, u} J
K : J ⥤ Functor.{v₁, u, u, u₂} C D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (F := K ⋙ obj (evaluation C D) k ⋙ obj prod.functor (F.obj k))
  (mapCocone (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) c) :=
  isColimitOfPreserves (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) t
⊢ IsColimit ((obj prod.functor F ⋙ obj (evaluation C D) k).mapCocone c)
have apply : obj (evaluation C D) k ⋙ obj prod.functor (F.obj k) ≅ obj prod.functor F ⋙ obj (evaluation C D) k
Tactic: apply IsColimit.mapCoconeEquiv _ this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v₁, u} C
D : Type u₂
inst_1 : Category.{u, u₂} D
inst_2 : HasBinaryProducts.{u, u₂} D
inst_3 : HasColimits.{u, u₂} D
inst_4 : ∀ (X : D), PreservesColimits.{u, u, u₂, u₂} (obj prod.functor X)
F : Functor.{v₁, u, u, u₂} C D
J : Type u
inst_5 : Category.{u, u} J
K : J ⥤ Functor.{v₁, u, u, u₂} C D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (F := K ⋙ obj (evaluation C D) k ⋙ obj prod.functor (F.obj k))
  (mapCocone (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) c) :=
  isColimitOfPreserves (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) t
⊢ obj (evaluation C D) k ⋙ obj prod.functor (F.obj k) ≅ obj prod.functor F ⋙ obj (evaluation C D) k
have apply : (X : Functor.{v₁, u, u, u₂} C D) →
  (obj prod.functor F ⋙ obj (evaluation C D) k).obj X ≅ obj (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) X
Tactic: apply (NatIso.ofComponents _ _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v₁, u} C
D : Type u₂
inst_1 : Category.{u, u₂} D
inst_2 : HasBinaryProducts.{u, u₂} D
inst_3 : HasColimits.{u, u₂} D
inst_4 : ∀ (X : D), PreservesColimits.{u, u, u₂, u₂} (obj prod.functor X)
F : Functor.{v₁, u, u, u₂} C D
J : Type u
inst_5 : Category.{u, u} J
K : J ⥤ Functor.{v₁, u, u, u₂} C D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (F := K ⋙ obj (evaluation C D) k ⋙ obj prod.functor (F.obj k))
  (mapCocone (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) c) :=
  isColimitOfPreserves (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) t
apply :
  (X : Functor.{v₁, u, u, u₂} C D) →
    (obj prod.functor F ⋙ obj (evaluation C D) k).obj X ≅ obj (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) X
⊢ obj (evaluation C D) k ⋙ obj prod.functor (F.obj k) ≅ obj prod.functor F ⋙ obj (evaluation C D) k
have apply₁ : ∀ {X Y : Functor.{v₁, u, u, u₂} C D} (f : X ⟶ Y),
  Eq (α :=
    (obj prod.functor F ⋙ obj (evaluation C D) k).obj X ⟶ obj (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) Y)
    ((obj prod.functor F ⋙ obj (evaluation C D) k).map f ≫
      Iso.hom (asIso (prodComparison (obj (evaluation C D) k) F Y)))
    (Iso.hom (asIso (prodComparison (obj (evaluation C D) k) F X)) ≫
      map (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) f)
Tactic: apply (NatIso.ofComponents _ _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasLimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cone K
hc : IsLimit c
⊢ IsLimit (F := K ⋙ obj (whiskeringLeft C E D) F) (mapCone (obj (whiskeringLeft C E D) F) c)
have t : (k : C) →
  IsLimit (F := (K ⋙ obj (whiskeringLeft C E D) F) ⋙ obj (evaluation C D) k)
    (mapCone (obj (evaluation C D) k) (mapCone (obj (whiskeringLeft C E D) F) c))
Tactic: apply evaluationJointlyReflectsLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasLimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cone K
hc : IsLimit c
Y : C
⊢ IsLimit (F := (K ⋙ obj (whiskeringLeft C E D) F) ⋙ obj (evaluation C D) Y)
    (mapCone (obj (evaluation C D) Y) (mapCone (obj (whiskeringLeft C E D) F) c))
have t : IsLimit (F := K ⋙ obj (evaluation E D) (F.obj Y)) (mapCone (obj (evaluation E D) (F.obj Y)) c)
Tactic: change IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cocone K
hc : IsColimit c
⊢ IsColimit (F := K ⋙ obj (whiskeringLeft C E D) F) (mapCocone (obj (whiskeringLeft C E D) F) c)
have t : (k : C) →
  IsColimit (F := (K ⋙ obj (whiskeringLeft C E D) F) ⋙ obj (evaluation C D) k)
    (mapCocone (obj (evaluation C D) k) (mapCocone (obj (whiskeringLeft C E D) F) c))
Tactic: apply evaluationJointlyReflectsColimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cocone K
hc : IsColimit c
Y : C
⊢ IsColimit (F := (K ⋙ obj (whiskeringLeft C E D) F) ⋙ obj (evaluation C D) Y)
    (mapCocone (obj (evaluation C D) Y) (mapCocone (obj (whiskeringLeft C E D) F) c))
have t : IsColimit (F := K ⋙ obj (evaluation E D) (F.obj Y)) (mapCocone (obj (evaluation E D) (F.obj Y)) c)
Tactic: change IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit c
⊢ IsLimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCone (obj (whiskeringRight C D E) F) c)
have apply : (k : C) →
  IsLimit (F := (K ⋙ obj (whiskeringRight C D E) F) ⋙ obj (evaluation C E) k)
    (mapCone (obj (evaluation C E) k) (mapCone (obj (whiskeringRight C D E) F) c))
Tactic: apply evaluationJointlyReflectsLimits _ (fun k => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit c
k : C
⊢ IsLimit (F := (K ⋙ obj (whiskeringRight C D E) F) ⋙ obj (evaluation C E) k)
    (mapCone (obj (evaluation C E) k) (mapCone (obj (whiskeringRight C D E) F) c))
have change : IsLimit (F := K ⋙ obj (evaluation C D) k ⋙ F) (mapCone (obj (evaluation C D) k ⋙ F) c)
Tactic: change IsLimit (((evaluation _ _).obj k ⋙ F).mapCone c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_3, u_3} J E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : ReflectsLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCone (obj (whiskeringRight C D E) F) c)
⊢ IsLimit c
have apply : (k : C) → IsLimit (F := K ⋙ obj (evaluation C D) k) (mapCone (obj (evaluation C D) k) c)
Tactic: apply evaluationJointlyReflectsLimits _ (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_3, u_3} J E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : ReflectsLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCone (obj (whiskeringRight C D E) F) c)
k : C
⊢ IsLimit (F := K ⋙ obj (evaluation C D) k) (mapCone (obj (evaluation C D) k) c)
have t : IsLimit (F := (K ⋙ obj (evaluation C D) k) ⋙ F) (F.mapCone (mapCone (obj (evaluation C D) k) c))
Tactic: apply isLimitOfReflects F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasColimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesColimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cocone K
hc : IsColimit c
⊢ IsColimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCocone (obj (whiskeringRight C D E) F) c)
have apply : (k : C) →
  IsColimit (F := (K ⋙ obj (whiskeringRight C D E) F) ⋙ obj (evaluation C E) k)
    (mapCocone (obj (evaluation C E) k) (mapCocone (obj (whiskeringRight C D E) F) c))
Tactic: apply evaluationJointlyReflectsColimits _ (fun k => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasColimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesColimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cocone K
hc : IsColimit c
k : C
⊢ IsColimit (F := (K ⋙ obj (whiskeringRight C D E) F) ⋙ obj (evaluation C E) k)
    (mapCocone (obj (evaluation C E) k) (mapCocone (obj (whiskeringRight C D E) F) c))
have change : IsColimit (F := K ⋙ obj (evaluation C D) k ⋙ F) (mapCocone (obj (evaluation C D) k ⋙ F) c)
Tactic: change IsColimit (((evaluation _ _).obj k ⋙ F).mapCocone c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
H : Type u₂
inst_1 : Category.{v₂, u₂} H
J : Type u₃
inst_2 : Category.{v₃, u₃} J
F : C ⥤ Cat
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
inst_4 : HasLimitsOfShape.{v₃, u₃, v₂, u₂} J H
inst_5 : ∀ (c : C), HasColimitsOfShape.{v₄, u₄, v₂, u₂} (↑(F.obj c) : Type u₄) H
inst_6 : PreservesLimitsOfShape (C := Functor.{v₁, v₂, u₁, u₂} C H) J colim
inst_7 : ∀ (c : C), PreservesLimitsOfShape (C := Functor.{v₄, v₂, u₄, u₂} (↑(F.obj c) : Type u₄) H) J colim
⊢ PreservesLimitsOfShape (C := Grothendieck F ⥤ H) J colim
have preservesLimit : autoParam (∀ {K : J ⥤ Grothendieck F ⥤ H}, PreservesLimit K colim) PreservesLimitsOfShape.preservesLimit._autoParam
Tactic: constructor