awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
inst_3 : PreservesFiniteCoproducts F
x : ℕ
inst : PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ PreservesLimitsOfShape (Discrete (Fin x)) F.unop

Tactic:
apply +allowSynthFailures preservesLimitsOfShape_unop

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_unop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesFiniteProducts F
x : ℕ
inst : PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ PreservesColimitsOfShape (Discrete (Fin x)) F.op

Tactic:
apply +allowSynthFailures preservesColimitsOfShape_op

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_3 : PreservesFiniteProducts F
x : ℕ
inst : PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ PreservesColimitsOfShape (Discrete (Fin x)) F.leftOp

Tactic:
apply +allowSynthFailures preservesColimitsOfShape_leftOp

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_leftOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
inst_3 : PreservesFiniteProducts F
x : ℕ
inst : PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ PreservesColimitsOfShape (Discrete (Fin x)) F.rightOp

Tactic:
apply +allowSynthFailures preservesColimitsOfShape_rightOp

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_rightOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
inst_3 : PreservesFiniteProducts F
x : ℕ
inst : PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ PreservesColimitsOfShape (Discrete (Fin x)) F.unop

Tactic:
apply +allowSynthFailures preservesColimitsOfShape_unop

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_unop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ReflectsFiniteCoproducts F
n : ℕ
inst : ReflectsColimitsOfShape (Discrete (Fin n))ᵒᵖ F
⊢ ReflectsLimitsOfShape (Discrete (Fin n)) F.op

Tactic:
apply +allowSynthFailures reflectsLimitsOfShape_op

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteCoproducts F
n : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin n))ᵒᵖ F

Tactic:
reflectsColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteCoproducts F
n : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin n))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_3 : ReflectsFiniteCoproducts F
x : ℕ
inst : ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ ReflectsLimitsOfShape (Discrete (Fin x)) F.leftOp

Tactic:
apply +allowSynthFailures reflectsLimitsOfShape_leftOp

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_leftOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
reflectsColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
inst_3 : ReflectsFiniteCoproducts F
x : ℕ
inst : ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ ReflectsLimitsOfShape (Discrete (Fin x)) F.rightOp

Tactic:
apply +allowSynthFailures reflectsLimitsOfShape_rightOp

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_rightOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
reflectsColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
inst_3 : ReflectsFiniteCoproducts F
x : ℕ
inst : ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ ReflectsLimitsOfShape (Discrete (Fin x)) F.unop

Tactic:
apply +allowSynthFailures reflectsLimitsOfShape_unop

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_unop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
reflectsColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ReflectsFiniteProducts F
x : ℕ
inst : ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ ReflectsColimitsOfShape (Discrete (Fin x)) F.op

Tactic:
apply +allowSynthFailures reflectsColimitsOfShape_op

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
reflectsLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_3 : ReflectsFiniteProducts F
x : ℕ
inst : ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ ReflectsColimitsOfShape (Discrete (Fin x)) F.leftOp

Tactic:
apply +allowSynthFailures reflectsColimitsOfShape_leftOp

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_leftOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
reflectsLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
inst_3 : ReflectsFiniteProducts F
x : ℕ
inst : ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ ReflectsColimitsOfShape (Discrete (Fin x)) F.rightOp

Tactic:
apply +allowSynthFailures reflectsColimitsOfShape_rightOp

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_rightOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
reflectsLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
inst_3 : ReflectsFiniteProducts F
x : ℕ
inst : ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ ReflectsColimitsOfShape (Discrete (Fin x)) F.unop

Tactic:
apply +allowSynthFailures reflectsColimitsOfShape_unop

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_unop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
reflectsLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F

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

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ PreservesCofilteredLimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (C := Over.{v_1, u_1} X) (Over.forget X)

Tactic:
⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Limits.IsLimit.ofExistsUnique, CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.mk, CategoryTheory.Limits.PreservesLimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
refine :
  ∀ (J : Type u_3) (hJ : Category.{u_2, u_3} J) (hJ' : IsCofiltered.{u_2, u_3} J) {F : J ⥤ Over.{v_1, u_1} X}
    {c : Cone F} (hc : IsLimit c) (s : Cone (F ⋙ Over.forget X)),
    ∃! l : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c),
      ∀ (j : J), l ≫ NatTrans.app (Cone.π (Functor.mapCone (Over.forget X) c)) j = s.π.app j
⊢ PreservesCofilteredLimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (C := Over.{v_1, u_1} X) (Over.forget X)

Tactic:
refine ⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
obtain :
  ∀ (i : J),
    ∃! l : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c),
      ∀ (j : J), l ≫ NatTrans.app (Cone.π (Functor.mapCone (Over.forget X) c)) j = s.π.app j
⊢ ∃! l : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c),
    ∀ (j : J), l ≫ NatTrans.app (Cone.π (Functor.mapCone (Over.forget X) c)) j = s.π.app j

Tactic:
obtain i := Nonempty.some ((inferInstance : Nonempty J))

Premises used: inferInstance, Nonempty.some
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j : J
obtain :
  ∀ (k : J) (hik : k ⟶ i) (hjk : k ⟶ j),
    s.π.app j ≫ (F.obj j).hom =
      (Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j).hom
⊢ s.π.app j ≫ (F.obj j).hom = (Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j).hom

Tactic:
obtain ⟨k, hik, hjk, -⟩ := IsCofilteredOrEmpty.cone_objs i j

Premises used: CategoryTheory.IsCofilteredOrEmpty.cone_objs
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
hik : k ⟶ i
hjk : k ⟶ j
simp :
  (s.π.app k ≫ (F ⋙ Over.forget X).map hjk) ≫ (F.obj j).hom = (s.π.app k ≫ (F ⋙ Over.forget X).map hik) ≫ (F.obj i).hom
⊢ s.π.app j ≫ (F.obj j).hom = (Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j).hom

Tactic:
simp only [Functor.const_obj_obj, Over.mk_left, Over.mk_hom,
      ← s.w hjk, ← s.w hik]

Premises used: CategoryTheory.Over.mk_left, CategoryTheory.Over.mk_hom, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
hik : k ⟶ i
hjk : k ⟶ j
⊢ (s.π.app k ≫ (F ⋙ Over.forget X).map hjk) ≫ (F.obj j).hom = (s.π.app k ≫ (F ⋙ Over.forget X).map hik) ≫ (F.obj i).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
e : j ⟶ k
h :
  Eq (α := (Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j).left ⟶ (F.obj k).left)
    (Over.Hom.left
      (Functor.map (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) e ≫
        (fun (j : J) ↦
            (Over.homMk (s.π.app j) ⋯ :
              Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j ⟶ F.obj j))
          k))
    (Over.Hom.left
      ((fun (j : J) ↦
            (Over.homMk (s.π.app j) ⋯ :
              Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j ⟶ F.obj j))
          j ≫
        F.map e))
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) e ≫
      (fun (j : J) ↦
          (Over.homMk (s.π.app j) ⋯ :
            Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j ⟶ F.obj j))
        k)
    ((fun (j : J) ↦
          (Over.homMk (s.π.app j) ⋯ :
            Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j ⟶ F.obj j))
        j ≫
      F.map e)

Tactic:
ext