awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : PreservesLimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesLimitsOfShape J F

Tactic:
preservesLimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.ULiftHomULiftCategory.equiv, CategoryTheory.Equivalence.symm
-- 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
this : PreservesLimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesLimitsOfShape J F

Tactic:
exact preservesLimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.ULiftHomULiftCategory.equiv, CategoryTheory.Equivalence.symm
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : PreservesFiniteLimits F
inst_4 : PreservesFiniteLimits G
⊢ PreservesFiniteLimits (F ⋙ G)

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesFiniteLimits.mk
-- 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
J : Type u
inst_4 : Finite J
inst_5 : PreservesFiniteProducts F
obtain : ∀ (n : ℕ) (e : J ≃ Fin n), PreservesLimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F
⊢ PreservesLimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J

Premises used: Finite.exists_equiv_fin
-- 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
J : Type u
inst_4 : Finite J
inst_5 : PreservesFiniteProducts F
n : ℕ
e : J ≃ Fin n
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F

Tactic:
have := PreservesFiniteProducts.preserves (F := F) n
-- 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
J : Type u
inst_4 : Finite J
inst_5 : PreservesFiniteProducts F
n : ℕ
e : J ≃ Fin n
this : PreservesLimitsOfShape (Discrete (Fin n)) F
⊢ PreservesLimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F

Tactic:
preservesLimitsOfShape_of_equiv (Discrete.equivalence e.symm) F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.equivalence, Equiv.symm
-- 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
J : Type u
inst_4 : Finite J
inst_5 : PreservesFiniteProducts F
n : ℕ
e : J ≃ Fin n
this : PreservesLimitsOfShape (Discrete (Fin n)) F
⊢ PreservesLimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F

Tactic:
exact preservesLimitsOfShape_of_equiv (Discrete.equivalence e.symm) F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Discrete.equivalence, Equiv.symm
-- 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 : ReflectsFiniteProducts F
J : Type u
inst_5 : Finite J
⊢ ReflectsLimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F

Tactic:
let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
  have := ReflectsFiniteProducts.reflects (F := F) n
  reflectsLimitsOfShape_of_equiv (Discrete.equivalence e.symm) _

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv, CategoryTheory.Limits.ReflectsFiniteProducts.reflects, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.ReflectsLimitsOfShape, Finite.exists_equiv_fin, Equiv.symm, _private.0.CategoryTheory.Limits.instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite.match_1, CategoryTheory.Discrete
-- 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 : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
haveI := reflectsSmallestLimits_of_reflectsLimits 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 : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsLimitsOfShape J F

Tactic:
reflectsLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_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 : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsLimitsOfShape J F

Tactic:
exact reflectsLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_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 : ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsFiniteLimits F

Tactic:
ReflectsLimitsOfSize.reflectsFiniteLimits F

Premises used: CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits
-- 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 : ReflectsLimits F
⊢ ReflectsFiniteLimits F

Tactic:
ReflectsLimitsOfSize.reflectsFiniteLimits F

Premises used: CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits
-- 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 : PreservesFiniteColimits F
J : Type w
inst_5 : SmallCategory J
inst_6 : FinCategory J
⊢ PreservesColimitsOfShape J F

Tactic:
apply preservesColimitsOfShape_of_equiv (FinCategory.equivAsType J)

Premises used: CategoryTheory.FinCategory.equivAsType, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv
-- 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 : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
haveI := preservesSmallestColimits_of_preservesColimits 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 : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfShape J F

Tactic:
preservesColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Premises used: CategoryTheory.FinCategory.equivAsType, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv
-- 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 : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfShape J F

Tactic:
exact preservesColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Premises used: CategoryTheory.FinCategory.equivAsType, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv
-- 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 : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesFiniteColimits F

Tactic:
PreservesColimitsOfSize.preservesFiniteColimits F

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits
-- 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 : PreservesColimits F
⊢ PreservesFiniteColimits F

Tactic:
PreservesColimitsOfSize.preservesFiniteColimits F

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits
-- 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), PreservesColimitsOfShape J F
J : Type
x : SmallCategory J
x_1 : FinCategory J
this : Category.{w, w} (ULiftHom (ULift.{w, 0} J)) := ULiftHom.category
⊢ PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (ULiftHom (ULift.{w, 0} J)) F

Tactic:
haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
-- 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), PreservesColimitsOfShape J F
J : Type
x : SmallCategory J
x_1 : FinCategory J
this_1 : Category.{w, w} (ULiftHom (ULift.{w, 0} J)) := ULiftHom.category
this : PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesColimitsOfShape J F

Tactic:
preservesColimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

Premises used: CategoryTheory.ULiftHomULiftCategory.equiv, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm
-- 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), PreservesColimitsOfShape J F
J : Type
x : SmallCategory J
x_1 : FinCategory J
this_1 : Category.{w, w} (ULiftHom (ULift.{w, 0} J)) := ULiftHom.category
this : PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesColimitsOfShape J F

Tactic:
exact preservesColimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

Premises used: CategoryTheory.ULiftHomULiftCategory.equiv, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : PreservesFiniteColimits F
inst_4 : PreservesFiniteColimits G
⊢ PreservesFiniteColimits (F ⋙ G)

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: CategoryTheory.Limits.PreservesFiniteColimits.mk, inferInstance
-- 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
J : Type u
inst_4 : Finite J
inst_5 : PreservesFiniteCoproducts F
⊢ PreservesColimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F

Tactic:
let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
  have := PreservesFiniteCoproducts.preserves (F := F) n
  preservesColimitsOfShape_of_equiv (Discrete.equivalence e.symm) F

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, Finite.exists_equiv_fin, CategoryTheory.Limits.PreservesColimitsOfShape, CategoryTheory.Limits.PreservesFiniteCoproducts.preserves, Equiv.symm, _private.0.CategoryTheory.Limits.instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite.match_1, CategoryTheory.Discrete
-- 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 : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
haveI := reflectsSmallestColimits_of_reflectsColimits 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 : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsColimitsOfShape J F

Tactic:
reflectsColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_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 : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsColimitsOfShape J F

Tactic:
exact reflectsColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_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 : ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsFiniteColimits F

Tactic:
ReflectsColimitsOfSize.reflectsFiniteColimits F

Premises used: CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits
-- 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 : ReflectsColimits F
⊢ ReflectsFiniteColimits F

Tactic:
ReflectsColimitsOfSize.reflectsFiniteColimits F

Premises used: CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits
-- 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 : ReflectsFiniteCoproducts F
J : Type u
inst_5 : Finite J
⊢ ReflectsColimitsOfShape.{u, u, v₁, v₂, u₁, u₂} (Discrete J) F

Tactic:
let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
  have := ReflectsFiniteCoproducts.reflects (F := F) n
  reflectsColimitsOfShape_of_equiv (Discrete.equivalence e.symm) _

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv, CategoryTheory.Limits.ReflectsColimitsOfShape, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.ReflectsFiniteCoproducts.reflects, Finite.exists_equiv_fin, Equiv.symm, _private.0.CategoryTheory.Limits.instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite.match_1, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
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
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))
⊢ IsColimit (F := K ⋙ obj prod.functor F) (mapCocone (obj prod.functor F) c)

Tactic:
apply evaluationJointlyReflectsColimits _ fun {k} => ?_

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsColimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
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
change : IsColimit ((obj prod.functor F ⋙ obj (evaluation C D) k).mapCocone 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:
change IsColimit ((prod.functor.obj F ⋙ (evaluation _ _).obj k).mapCocone c)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.prod.functor, CategoryTheory.Functor.comp, CategoryTheory.Limits.IsColimit, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
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 : obj (evaluation C D) k ⋙ obj prod.functor (F.obj k) ≅ obj prod.functor F ⋙ obj (evaluation C D) k
⊢ IsColimit ((obj prod.functor F ⋙ obj (evaluation C D) k).mapCocone c)

Tactic:
apply IsColimit.mapCoconeEquiv _ this

Premises used: CategoryTheory.Limits.IsColimit.mapCoconeEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
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
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)
⊢ obj (evaluation C D) k ⋙ obj prod.functor (F.obj k) ≅ obj prod.functor F ⋙ obj (evaluation C D) k

Tactic:
apply (NatIso.ofComponents _ _).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
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
G : Functor.{v₁, u, u, u₂} C D
⊢ (obj prod.functor F ⋙ obj (evaluation C D) k).obj G ≅ obj (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) G

Tactic:
apply asIso (prodComparison ((evaluation C D).obj k) F G)

Premises used: CategoryTheory.evaluation, CategoryTheory.Limits.prodComparison, CategoryTheory.Functor.obj, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
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
G G' : Functor.{v₁, u, u, u₂} C D
⊢ ∀ (f : G ⟶ G'),
    Eq (α :=
      (obj prod.functor F ⋙ obj (evaluation C D) k).obj G ⟶
        obj (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) G')
      ((obj prod.functor F ⋙ obj (evaluation C D) k).map f ≫
        Iso.hom (asIso (prodComparison (obj (evaluation C D) k) F G')))
      (Iso.hom (asIso (prodComparison (obj (evaluation C D) k) F G)) ≫
        map (obj (evaluation C D) k ⋙ obj prod.functor (F.obj k)) f)

Tactic:
apply prodComparison_natural ((evaluation C D).obj k) (𝟙 F)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.prodComparison_natural, CategoryTheory.evaluation, CategoryTheory.Functor.obj