awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesLimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
preservesLimit :
  autoParam (∀ {K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C}, PreservesLimit K F)
    PreservesLimitsOfShape.preservesLimit._autoParam
⊢ PreservesLimitsOfShape J F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesLimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
preservesLimit : PreservesLimit K (F ⋙ forget V G)
⊢ PreservesLimit K F

Tactic:
apply Action.preservesLimit_of_preserves

Premises used: Action.preservesLimit_of_preserves
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesLimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
⊢ PreservesLimit K (F ⋙ forget V G)

Tactic:
PreservesLimitsOfShape.preservesLimit

Premises used: CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesLimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
⊢ PreservesLimit K (F ⋙ forget V G)

Tactic:
exact PreservesLimitsOfShape.preservesLimit

Premises used: CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
preservesLimitsOfShape :
  autoParam (∀ {J : Type w₁} [inst_3 : Category.{w₂, w₁} J], PreservesLimitsOfShape J F)
    PreservesLimitsOfSize.preservesLimitsOfShape._autoParam
⊢ PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
preservesLimitsOfShape : ∀ [inst_3 : Category.{w₂, w₁} J], PreservesLimitsOfShape J F
⊢ ∀ [inst_3 : Category.{w₂, w₁} J], PreservesLimitsOfShape J F

Tactic:
_
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst_3 : Category.{w₂, w₁} J
preservesLimitsOfShape : PreservesLimitsOfShape.{w₂, w₁, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
⊢ PreservesLimitsOfShape J F

Tactic:
apply Action.preservesLimitsOfShape_of_preserves

Premises used: Action.preservesLimitsOfShape_of_preserves
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst_3 : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape.{w₂, w₁, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)

Tactic:
PreservesLimitsOfSize.preservesLimitsOfShape

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst_3 : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape.{w₂, w₁, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)

Tactic:
exact PreservesLimitsOfSize.preservesLimitsOfShape

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V
J : Type u_4
inst_3 : Category.{v_3, u_4} J
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesColimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
H : ∀ (k : SingleObj G), PreservesColimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) k)
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_evaluation

Premises used: CategoryTheory.Limits.preservesColimit_of_evaluation
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V
J : Type u_4
inst_3 : Category.{v_3, u_4} J
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesColimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
k : SingleObj G
⊢ PreservesColimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) k)

Tactic:
h

Premises used: Quiver.SingleObj, Quiver.SingleObj.star
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V
J : Type u_4
inst_3 : Category.{v_3, u_4} J
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesColimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
k : SingleObj G
⊢ PreservesColimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) k)

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesColimit K (F ⋙ forget V G)
F' : C ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V :=
  F ⋙ Equivalence.functor (functorCategoryEquivalence V G)
⊢ PreservesColimit K F'

Tactic:
have : PreservesColimit K F' := SingleObj.preservesColimit _ _ h
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesColimit K (F ⋙ forget V G)
F' : C ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V :=
  F ⋙ Equivalence.functor (functorCategoryEquivalence V G)
this : PreservesColimit K F'
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor

Premises used: CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesColimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
preservesColimit :
  autoParam (∀ {K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C}, PreservesColimit K F)
    PreservesColimitsOfShape.preservesColimit._autoParam
⊢ PreservesColimitsOfShape J F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesColimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
preservesColimit : PreservesColimit K (F ⋙ forget V G)
⊢ PreservesColimit K F

Tactic:
apply Action.preservesColimit_of_preserves

Premises used: Action.preservesColimit_of_preserves
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesColimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
⊢ PreservesColimit K (F ⋙ forget V G)

Tactic:
PreservesColimitsOfShape.preservesColimit

Premises used: CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesColimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
⊢ PreservesColimit K (F ⋙ forget V G)

Tactic:
exact PreservesColimitsOfShape.preservesColimit

Premises used: CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
preservesColimitsOfShape :
  autoParam (∀ {J : Type w₁} [inst_3 : Category.{w₂, w₁} J], PreservesColimitsOfShape J F)
    PreservesColimitsOfSize.preservesColimitsOfShape._autoParam
⊢ PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
preservesColimitsOfShape : ∀ [inst_3 : Category.{w₂, w₁} J], PreservesColimitsOfShape J F
⊢ ∀ [inst_3 : Category.{w₂, w₁} J], PreservesColimitsOfShape J F

Tactic:
_
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst_3 : Category.{w₂, w₁} J
preservesColimitsOfShape : PreservesColimitsOfShape.{w₂, w₁, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
⊢ PreservesColimitsOfShape J F

Tactic:
apply Action.preservesColimitsOfShape_of_preserves

Premises used: Action.preservesColimitsOfShape_of_preserves
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst_3 : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape.{w₂, w₁, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)

Tactic:
PreservesColimitsOfSize.preservesColimitsOfShape

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst_3 : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape.{w₂, w₁, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)

Tactic:
exact PreservesColimitsOfSize.preservesColimitsOfShape

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasLimit (K ⋙ forget V G)
change :
  PreservesLimit K
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ PreservesLimit K (forget V G)

Tactic:
change PreservesLimit K ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))

Premises used: CategoryTheory.Limits.PreservesLimit, CategoryTheory.Functor.comp, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor, CategoryTheory.SingleObj.star, CategoryTheory.SingleObj, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasLimit (K ⋙ forget V G)
⊢ ∀ (k : SingleObj G), HasLimit ((K ⋙ Equivalence.functor (functorCategoryEquivalence V G)).flip.obj k)

Tactic:
have (k : SingleObj G) :
      HasLimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
    inferInstanceAs (HasLimit (K ⋙ forget V G))
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasLimit (K ⋙ forget V G)
this : ∀ (k : SingleObj G), HasLimit ((K ⋙ Equivalence.functor (functorCategoryEquivalence V G)).flip.obj k)
⊢ PreservesLimit K
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasColimit (K ⋙ forget V G)
change :
  PreservesColimit K
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ PreservesColimit K (forget V G)

Tactic:
change PreservesColimit K ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))

Premises used: CategoryTheory.Functor.comp, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor, CategoryTheory.SingleObj.star, CategoryTheory.SingleObj, CategoryTheory.evaluation, CategoryTheory.Limits.PreservesColimit, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasColimit (K ⋙ forget V G)
⊢ ∀ (k : SingleObj G), HasColimit ((K ⋙ Equivalence.functor (functorCategoryEquivalence V G)).flip.obj k)

Tactic:
have (k : SingleObj G) :
      HasColimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
    inferInstanceAs (HasColimit (K ⋙ forget V G))
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasColimit (K ⋙ forget V G)
this : ∀ (k : SingleObj G), HasColimit ((K ⋙ Equivalence.functor (functorCategoryEquivalence V G)).flip.obj k)
⊢ PreservesColimit K
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
change :
  PreservesFiniteLimits (C := Action.{v_1, u_1, u_2} V G)
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ PreservesFiniteLimits (C := Action.{v_1, u_1, u_2} V G) (forget V G)

Tactic:
change PreservesFiniteLimits ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))

Premises used: CategoryTheory.Limits.PreservesFiniteLimits, CategoryTheory.Functor.comp, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor, CategoryTheory.SingleObj.star, CategoryTheory.SingleObj, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
preservesFiniteLimits :
  autoParam
    (∀ (J : Type) [inst_3 : SmallCategory J] [FinCategory J],
      PreservesLimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
        (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G)))
    PreservesFiniteLimits.preservesFiniteLimits._autoParam
⊢ PreservesFiniteLimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
J : Type
preservesFiniteLimits :
  ∀ [inst_3 : SmallCategory J] [FinCategory J],
    PreservesLimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ ∀ [inst_3 : SmallCategory J] [FinCategory J],
    PreservesLimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
J : Type
inst_3 : SmallCategory J
preservesFiniteLimits :
  ∀ [FinCategory J],
    PreservesLimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ ∀ [FinCategory J],
    PreservesLimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
J : Type
inst_3 : SmallCategory J
inst_4 : FinCategory J
⊢ PreservesLimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
⊢ PreservesFiniteLimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
have : PreservesFiniteLimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) := by
    constructor
    intro _ _ _
    infer_instance
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
this :
  PreservesFiniteLimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ PreservesFiniteLimits (C := Action.{v_1, u_1, u_2} V G)
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
apply comp_preservesFiniteLimits

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
change :
  PreservesFiniteColimits (C := Action.{v_1, u_1, u_2} V G)
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ PreservesFiniteColimits (C := Action.{v_1, u_1, u_2} V G) (forget V G)

Tactic:
change PreservesFiniteColimits ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))

Premises used: CategoryTheory.Functor.comp, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor, CategoryTheory.SingleObj.star, CategoryTheory.Limits.PreservesFiniteColimits, CategoryTheory.SingleObj, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
preservesFiniteColimits :
  autoParam
    (∀ (J : Type) [inst_3 : SmallCategory J] [FinCategory J],
      PreservesColimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
        (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G)))
    PreservesFiniteColimits.preservesFiniteColimits._autoParam
⊢ PreservesFiniteColimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
J : Type
preservesFiniteColimits :
  ∀ [inst_3 : SmallCategory J] [FinCategory J],
    PreservesColimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ ∀ [inst_3 : SmallCategory J] [FinCategory J],
    PreservesColimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
J : Type
inst_3 : SmallCategory J
preservesFiniteColimits :
  ∀ [FinCategory J],
    PreservesColimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ ∀ [FinCategory J],
    PreservesColimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
J : Type
inst_3 : SmallCategory J
inst_4 : FinCategory J
⊢ PreservesColimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
⊢ PreservesFiniteColimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))

Tactic:
have : PreservesFiniteColimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) := by
    constructor
    intro _ _ _
    infer_instance