awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_4 : CreatesFiniteCoproducts F
x : Type
x_1 : Fintype x
inst : CreatesColimitsOfShape (Discrete x)ᵒᵖ F
⊢ CreatesLimitsOfShape (Discrete x) F.leftOp

Tactic:
apply +allowSynthFailures createsLimitsOfShapeLeftOp

Premises used: CategoryTheory.Limits.createsLimitsOfShapeLeftOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
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
⊢ CreatesColimitsOfShape (Discrete x)ᵒᵖ F

Tactic:
exact createsColimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm, CategoryTheory.createsColimitsOfShapeOfEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
inst_4 : CreatesFiniteCoproducts F
x : Type
x_1 : Fintype x
inst : CreatesColimitsOfShape (Discrete x)ᵒᵖ F
⊢ CreatesLimitsOfShape (Discrete x) F.rightOp

Tactic:
apply +allowSynthFailures createsLimitsOfShapeRightOp

Premises used: CategoryTheory.Limits.createsLimitsOfShapeRightOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
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
⊢ CreatesColimitsOfShape (Discrete x)ᵒᵖ F

Tactic:
exact createsColimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm, CategoryTheory.createsColimitsOfShapeOfEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
inst_4 : CreatesFiniteCoproducts F
x : Type
x_1 : Fintype x
inst : CreatesColimitsOfShape (Discrete x)ᵒᵖ F
⊢ CreatesLimitsOfShape (Discrete x) F.unop

Tactic:
apply +allowSynthFailures createsLimitsOfShapeUnop

Premises used: CategoryTheory.Limits.createsLimitsOfShapeUnop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
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
⊢ CreatesColimitsOfShape (Discrete x)ᵒᵖ F

Tactic:
exact createsColimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm, CategoryTheory.createsColimitsOfShapeOfEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesFiniteProducts F
x : Type
x_1 : Fintype x
inst : CreatesLimitsOfShape (Discrete x)ᵒᵖ F
⊢ CreatesColimitsOfShape (Discrete x) F.op

Tactic:
apply +allowSynthFailures createsColimitsOfShapeOp

Premises used: CategoryTheory.Limits.createsColimitsOfShapeOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
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
⊢ CreatesLimitsOfShape (Discrete x)ᵒᵖ F

Tactic:
exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.createsLimitsOfShapeOfEquiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_4 : CreatesFiniteProducts F
x : Type
x_1 : Fintype x
inst : CreatesLimitsOfShape (Discrete x)ᵒᵖ F
⊢ CreatesColimitsOfShape (Discrete x) F.leftOp

Tactic:
apply +allowSynthFailures createsColimitsOfShapeLeftOp

Premises used: CategoryTheory.Limits.createsColimitsOfShapeLeftOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
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
⊢ CreatesLimitsOfShape (Discrete x)ᵒᵖ F

Tactic:
exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.createsLimitsOfShapeOfEquiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
inst_4 : CreatesFiniteProducts F
x : Type
x_1 : Fintype x
inst : CreatesLimitsOfShape (Discrete x)ᵒᵖ F
⊢ CreatesColimitsOfShape (Discrete x) F.rightOp

Tactic:
apply +allowSynthFailures createsColimitsOfShapeRightOp

Premises used: CategoryTheory.Limits.createsColimitsOfShapeRightOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
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
⊢ CreatesLimitsOfShape (Discrete x)ᵒᵖ F

Tactic:
exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.createsLimitsOfShapeOfEquiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
inst_4 : CreatesFiniteProducts F
x : Type
x_1 : Fintype x
inst : CreatesLimitsOfShape (Discrete x)ᵒᵖ F
⊢ CreatesColimitsOfShape (Discrete x) F.unop

Tactic:
apply +allowSynthFailures createsColimitsOfShapeUnop

Premises used: CategoryTheory.Limits.createsColimitsOfShapeUnop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_2 : CreatesLimit (cospan f g) F
inst_3 : HasPullback (F.map f) (F.map g)
⊢ HasPullback f g

Tactic:
have : HasLimit (cospan f g ⋙ F) := hasLimit_of_iso (cospanCompIso F f g).symm
  hasLimit_of_created _ F

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Limits.cospanCompIso, CategoryTheory.Limits.cospan, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Pullbacks
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y S : C
f : S ⟶ X
g : S ⟶ Y
inst_2 : CreatesColimit (span f g) F
inst_3 : HasPushout (F.map f) (F.map g)
⊢ HasPushout f g

Tactic:
have : HasColimit (span f g ⋙ F) := hasColimit_of_iso (spanCompIso F f g)
  hasColimit_of_created _ F

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.spanCompIso, CategoryTheory.Limits.span, CategoryTheory.hasColimit_of_created
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
⊢ IsFiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))

Tactic:
haveI := IsFiltered.of_equivalence e.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
this : IsFiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesColimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F

Tactic:
preservesColimitsOfShape_of_equiv e F

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
this : IsFiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesColimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F

Tactic:
exact preservesColimitsOfShape_of_equiv e F

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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 : PreservesFilteredColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F
⊢ PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

Tactic:
preservesFilteredColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Premises used: CategoryTheory.Limits.preservesFilteredColimitsOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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 : PreservesFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
⊢ PreservesFilteredColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
preservesFilteredColimitsOfSize_shrink F

Premises used: CategoryTheory.Limits.preservesFilteredColimitsOfSize_shrink
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
⊢ IsFiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))

Tactic:
haveI := IsFiltered.of_equivalence e.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
this : IsFiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsColimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F

Tactic:
reflectsColimitsOfShape_of_equiv e F

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
this : IsFiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsColimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F

Tactic:
exact reflectsColimitsOfShape_of_equiv e F

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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 : ReflectsFilteredColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F
⊢ ReflectsFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

Tactic:
reflectsFilteredColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Premises used: CategoryTheory.Limits.reflectsFilteredColimitsOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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 : ReflectsFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
⊢ ReflectsFilteredColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
reflectsFilteredColimitsOfSize_shrink F

Premises used: CategoryTheory.Limits.reflectsFilteredColimitsOfSize_shrink
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
⊢ IsCofiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))

Tactic:
haveI := IsCofiltered.of_equivalence e.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
this : IsCofiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesLimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F

Tactic:
preservesLimitsOfShape_of_equiv e F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
this : IsCofiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesLimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F

Tactic:
exact preservesLimitsOfShape_of_equiv e F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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 : PreservesCofilteredLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F
⊢ PreservesCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

Tactic:
preservesCofilteredLimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Premises used: CategoryTheory.Limits.preservesCofilteredLimitsOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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 : PreservesCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
⊢ PreservesCofilteredLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
preservesCofilteredLimitsOfSize_shrink F

Premises used: CategoryTheory.Limits.preservesCofilteredLimitsOfSize_shrink
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
⊢ IsCofiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))

Tactic:
haveI := IsCofiltered.of_equivalence e.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
this : IsCofiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsLimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F

Tactic:
reflectsLimitsOfShape_of_equiv e F

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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)))
this : IsCofiltered.{w', w₂'} (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsLimitsOfShape.{w, w₂, v₁, v₂, u₁, u₂} J F

Tactic:
exact reflectsLimitsOfShape_of_equiv e F

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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 : ReflectsCofilteredLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F
⊢ ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

Tactic:
reflectsCofilteredLimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Premises used: CategoryTheory.Limits.reflectsCofilteredLimitsOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered
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 : ReflectsCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
⊢ ReflectsCofilteredLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
reflectsCofilteredLimitsOfSize_shrink F

Premises used: CategoryTheory.Limits.reflectsCofilteredLimitsOfSize_shrink
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Finite
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
inst_4 : PreservesFiniteLimits F
J : Type w
inst_5 : SmallCategory J
inst_6 : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
apply preservesLimitsOfShape_of_equiv (FinCategory.equivAsType J)

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.FinCategory.equivAsType
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Finite
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
⊢ PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
haveI := preservesSmallestLimits_of_preservesLimits F
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Finite
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
this : PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesLimitsOfShape J F

Tactic:
preservesLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.FinCategory.equivAsType
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Finite
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
this : PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesLimitsOfShape J F

Tactic:
exact preservesLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.FinCategory.equivAsType
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Finite
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 w
inst_3 : SmallCategory J
K : Functor.{w, v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesFiniteLimits F

Tactic:
PreservesLimitsOfSize.preservesFiniteLimits F

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Finite
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 w
inst_3 : SmallCategory J
K : Functor.{w, v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : PreservesLimits F
⊢ PreservesFiniteLimits F

Tactic:
PreservesLimitsOfSize.preservesFiniteLimits F

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Finite
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.{w, w, v₁, v₂, u₁, u₂} (ULiftHom (ULift.{w, 0} J)) F

Tactic:
haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift