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
inst_2 : HasFiniteColimits.{v_1, u_1} V
this :
  PreservesFiniteColimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ 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))

Tactic:
apply comp_preservesFiniteColimits

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits
-- 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
F : J ⥤ Action.{v_1, u_1, u_2} V G
c : Cone F
h : IsLimit (F := F ⋙ forget V G) (Functor.mapCone (forget V G) c)
t :
  IsLimit (F := F ⋙ Equivalence.functor (functorCategoryEquivalence V G))
    (Functor.mapCone (Equivalence.functor (functorCategoryEquivalence V G)) c)
⊢ IsLimit c

Tactic:
apply isLimitOfReflects ((Action.functorCategoryEquivalence V G).functor)

Premises used: CategoryTheory.Limits.isLimitOfReflects, 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
J : Type u_3
inst_2 : Category.{v_2, u_3} J
F : J ⥤ Action.{v_1, u_1, u_2} V G
c : Cone F
h : IsLimit (F := F ⋙ forget V G) (Functor.mapCone (forget V G) c)
⊢ IsLimit (F := F ⋙ Equivalence.functor (functorCategoryEquivalence V G))
    (Functor.mapCone (Equivalence.functor (functorCategoryEquivalence V G)) c)

Tactic:
exact evaluationJointlyReflectsLimits _ (fun _ => 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
J : Type u_3
inst_2 : Category.{v_2, u_3} J
F : J ⥤ Action.{v_1, u_1, u_2} V G
c : Cocone F
h : IsColimit (F := F ⋙ forget V G) (Functor.mapCocone (forget V G) c)
t :
  IsColimit (F := F ⋙ Equivalence.functor (functorCategoryEquivalence V G))
    (Functor.mapCocone (Equivalence.functor (functorCategoryEquivalence V G)) c)
⊢ IsColimit c

Tactic:
apply isColimitOfReflects ((Action.functorCategoryEquivalence V G).functor)

Premises used: Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Limits.isColimitOfReflects
-- 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
F : J ⥤ Action.{v_1, u_1, u_2} V G
c : Cocone F
h : IsColimit (F := F ⋙ forget V G) (Functor.mapCocone (forget V G) c)
⊢ IsColimit (F := F ⋙ Equivalence.functor (functorCategoryEquivalence V G))
    (Functor.mapCocone (Equivalence.functor (functorCategoryEquivalence V G)) c)

Tactic:
exact evaluationJointlyReflectsColimits _ (fun _ => h)
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
W : Type u_3
inst_2 : Category.{v_2, u_3} W
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_3} V W
G : Type u_4
inst_3 : Monoid G
J : Type u_5
inst_4 : Category.{v_3, u_5} J
K : J ⥤ Action.{v_1, u_1, u_4} V G
inst_5 : HasLimit (K ⋙ forget V G)
inst_6 : PreservesLimit (K ⋙ forget V G) F
⊢ PreservesLimit K (F.mapAction G)

Tactic:
Action.preservesLimit_of_preserves (F.mapAction G) K <|
    inferInstanceAs (PreservesLimit K (forget V G ⋙ F))

Premises used: _private.0.Action.Functor.mapActionPreservesLimit_of_preserves._proof_1, CategoryTheory.Functor.mapAction, Action.preservesLimit_of_preserves
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
W : Type u_3
inst_2 : Category.{v_2, u_3} W
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_3} V W
G : Type u_4
inst_3 : Monoid G
J : Type u_5
inst_4 : Category.{v_3, u_5} J
K : J ⥤ Action.{v_1, u_1, u_4} V G
inst_5 : HasColimit (K ⋙ forget V G)
inst_6 : PreservesColimit (K ⋙ forget V G) F
⊢ PreservesColimit K (F.mapAction G)

Tactic:
Action.preservesColimit_of_preserves (F.mapAction G) K <|
    inferInstanceAs (PreservesColimit K (forget V G ⋙ F))

Premises used: CategoryTheory.Functor.mapAction, Action.preservesColimit_of_preserves, _private.0.Action.Functor.mapActionPreservesColimit_of_preserves._proof_1
-- 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 : HasZeroMorphisms.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
⊢ ∀ (g : G),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) (CategoryStruct.comp (Y := X.V) ((X.ρ : (a : G) → End X.V) g) 0 : X.V ⟶ Y.V)
      (CategoryStruct.comp (Y := Y.V) 0 ((Y.ρ : (a : G) → End Y.V) g) : X.V ⟶ Y.V)

Tactic:
simp
-- 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 : HasZeroMorphisms.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
⊢ Eq.{v_1 + 1} (α := X.V ⟶ Y.V) (Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
f g : X ⟶ Y
⊢ ∀ (g_1 : G),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : G) → End X.V) g_1 ≫ (f.hom + g.hom) : X.V ⟶ Y.V)
      ((f.hom + g.hom) ≫ (Y.ρ : (a : G) → End Y.V) g_1 : X.V ⟶ Y.V)

Tactic:
simp [f.comm, g.comm]

Premises used: Action.Hom.comm
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
f : X ⟶ Y
⊢ ∀ (g : G),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : G) → End X.V) g ≫ (-f.hom) : X.V ⟶ Y.V)
      ((-f.hom) ≫ (Y.ρ : (a : G) → End Y.V) g : X.V ⟶ Y.V)

Tactic:
simp [f.comm]

Premises used: Action.Hom.comm
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
f g : X ⟶ Y
⊢ ∀ (g_1 : G),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : G) → End X.V) g_1 ≫ (f.hom - g.hom) : X.V ⟶ Y.V)
      ((f.hom - g.hom) ≫ (Y.ρ : (a : G) → End Y.V) g_1 : X.V ⟶ Y.V)

Tactic:
simp [f.comm, g.comm]

Premises used: Action.Hom.comm
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
n : ℕ
f : X ⟶ Y
⊢ ∀ (g : G),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : G) → End X.V) g ≫ (n • f.hom) : X.V ⟶ Y.V)
      ((n • f.hom) ≫ (Y.ρ : (a : G) → End Y.V) g : X.V ⟶ Y.V)

Tactic:
simp [f.comm]

Premises used: Action.Hom.comm
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
n : ℤ
f : X ⟶ Y
⊢ ∀ (g : G),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : G) → End X.V) g ≫ (n • f.hom) : X.V ⟶ Y.V)
      ((n • f.hom) ≫ (Y.ρ : (a : G) → End Y.V) g : X.V ⟶ Y.V)

Tactic:
simp [f.comm]

Premises used: Action.Hom.comm
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
f g : X ⟶ Y
⊢ (f + g).hom = f.hom + g.hom

Tactic:
rfl

Premises used: rfl
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
f : X ⟶ Y
⊢ (-f).hom = -f.hom

Tactic:
rfl

Premises used: rfl
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
f g : X ⟶ Y
⊢ (f - g).hom = f.hom - g.hom

Tactic:
rfl

Premises used: rfl
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
n : ℕ
f : X ⟶ Y
⊢ (n • f).hom = n • f.hom

Tactic:
rfl

Premises used: rfl
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
n : ℤ
f : X ⟶ Y
⊢ (n • f).hom = n • f.hom

Tactic:
rfl

Premises used: rfl
-- 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 : Preadditive.{v_1, u_1} V
X Y P Q R : Action.{v_1, u_1, u_2} V G
f f' : P ⟶ Q
g : Q ⟶ R
h : ((f + f') ≫ g).hom = (f ≫ g + f' ≫ g).hom
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
X Y P Q R : Action.{v_1, u_1, u_2} V G
f f' : P ⟶ Q
g : Q ⟶ R
⊢ ((f + f') ≫ g).hom = (f ≫ g + f' ≫ g).hom

Tactic:
Preadditive.add_comp _ _ _ _ _ _

Premises used: CategoryTheory.Preadditive.add_comp
-- 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 : Preadditive.{v_1, u_1} V
X Y P Q R : Action.{v_1, u_1, u_2} V G
f f' : P ⟶ Q
g : Q ⟶ R
⊢ ((f + f') ≫ g).hom = (f ≫ g + f' ≫ g).hom

Tactic:
exact Preadditive.add_comp _ _ _ _ _ _

Premises used: CategoryTheory.Preadditive.add_comp
-- 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 : Preadditive.{v_1, u_1} V
X Y P Q R : Action.{v_1, u_1, u_2} V G
f : P ⟶ Q
g g' : Q ⟶ R
h : (f ≫ (g + g')).hom = (f ≫ g + f ≫ g').hom
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
X Y P Q R : Action.{v_1, u_1, u_2} V G
f : P ⟶ Q
g g' : Q ⟶ R
⊢ (f ≫ (g + g')).hom = (f ≫ g + f ≫ g').hom

Tactic:
Preadditive.comp_add _ _ _ _ _ _

Premises used: CategoryTheory.Preadditive.comp_add
-- 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 : Preadditive.{v_1, u_1} V
X Y P Q R : Action.{v_1, u_1, u_2} V G
f : P ⟶ Q
g g' : Q ⟶ R
⊢ (f ≫ (g + g')).hom = (f ≫ g + f ≫ g').hom

Tactic:
exact Preadditive.comp_add _ _ _ _ _ _

Premises used: CategoryTheory.Preadditive.comp_add
-- 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 : Preadditive.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
ι : Type u_3
f : ι → (X ⟶ Y)
s : Finset ι
⊢ (s.sum f).hom = ∑ i ∈ s, (f i).hom

Tactic:
(forget V G).map_sum f s

Premises used: Action.forget, CategoryTheory.Functor.map_sum
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
r : R
f : X ⟶ Y
⊢ ∀ (g : G),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : G) → End X.V) g ≫ (r • f.hom) : X.V ⟶ Y.V)
      ((r • f.hom) ≫ (Y.ρ : (a : G) → End Y.V) g : X.V ⟶ Y.V)

Tactic:
simp [f.comm]

Premises used: Action.Hom.comm
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
x y : R
b : X ⟶ Y
h : ((x * y) • b).hom = (x • y • b).hom
⊢ (x * y) • b = x • y • b

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
x y : R
b : X ⟶ Y
⊢ ((x * y) • b).hom = (x • y • b).hom

Tactic:
mul_smul _ _ _

Premises used: SemigroupAction.mul_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
x y : R
b : X ⟶ Y
⊢ ((x * y) • b).hom = (x • y • b).hom

Tactic:
exact mul_smul _ _ _

Premises used: SemigroupAction.mul_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
b : X ⟶ Y
h : (HSMul.hSMul.{u_3, v_1, v_1} (α := R) 1 b).hom = b.hom
⊢ HSMul.hSMul.{u_3, v_1, v_1} (α := R) 1 b = b

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
b : X ⟶ Y
⊢ (HSMul.hSMul.{u_3, v_1, v_1} (α := R) 1 b).hom = b.hom

Tactic:
one_smul _ _

Premises used: one_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
b : X ⟶ Y
⊢ (HSMul.hSMul.{u_3, v_1, v_1} (α := R) 1 b).hom = b.hom

Tactic:
exact one_smul _ _

Premises used: one_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
a : R
h : (HSMul.hSMul (β := X ⟶ Y) a 0).hom = Hom.hom 0
⊢ HSMul.hSMul (β := X ⟶ Y) a 0 = 0

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
a : R
⊢ (HSMul.hSMul (β := X ⟶ Y) a 0).hom = Hom.hom 0

Tactic:
smul_zero _

Premises used: smul_zero
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
a : R
⊢ (HSMul.hSMul (β := X ⟶ Y) a 0).hom = Hom.hom 0

Tactic:
exact smul_zero _

Premises used: smul_zero
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
a : R
x y : X ⟶ Y
h : (a • (x + y)).hom = (a • x + a • y).hom
⊢ a • (x + y) = a • x + a • y

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
a : R
x y : X ⟶ Y
⊢ (a • (x + y)).hom = (a • x + a • y).hom

Tactic:
smul_add _ _ _

Premises used: smul_add
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
a : R
x y : X ⟶ Y
⊢ (a • (x + y)).hom = (a • x + a • y).hom

Tactic:
exact smul_add _ _ _

Premises used: smul_add
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
r s : R
x : X ⟶ Y
h : ((r + s) • x).hom = (r • x + s • x).hom
⊢ (r + s) • x = r • x + s • x

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
r s : R
x : X ⟶ Y
⊢ ((r + s) • x).hom = (r • x + s • x).hom

Tactic:
add_smul _ _ _

Premises used: add_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
r s : R
x : X ⟶ Y
⊢ ((r + s) • x).hom = (r • x + s • x).hom

Tactic:
exact add_smul _ _ _

Premises used: add_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
h : (HSMul.hSMul.{u_3, v_1, v_1} (α := R) 0 x).hom = Hom.hom 0
⊢ HSMul.hSMul.{u_3, v_1, v_1} (α := R) 0 x = 0

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
⊢ (HSMul.hSMul.{u_3, v_1, v_1} (α := R) 0 x).hom = Hom.hom 0

Tactic:
zero_smul _ _

Premises used: zero_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
⊢ (HSMul.hSMul.{u_3, v_1, v_1} (α := R) 0 x).hom = Hom.hom 0

Tactic:
exact zero_smul _ _

Premises used: zero_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y Z : Action.{v_1, u_1, u_2} V G
r : R
f : X ⟶ Y
g : Y ⟶ Z
h : ((r • f) ≫ g).hom = (r • f ≫ g).hom
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y Z : Action.{v_1, u_1, u_2} V G
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((r • f) ≫ g).hom = (r • f ≫ g).hom

Tactic:
Linear.smul_comp _ _ _ _ _ _

Premises used: CategoryTheory.Linear.smul_comp
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y Z : Action.{v_1, u_1, u_2} V G
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((r • f) ≫ g).hom = (r • f ≫ g).hom

Tactic:
exact Linear.smul_comp _ _ _ _ _ _

Premises used: CategoryTheory.Linear.smul_comp
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y Z : Action.{v_1, u_1, u_2} V G
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : (f ≫ (r • g)).hom = (r • f ≫ g).hom
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
ext
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y Z : Action.{v_1, u_1, u_2} V G
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (f ≫ (r • g)).hom = (r • f ≫ g).hom

Tactic:
Linear.comp_smul _ _ _ _ _ _

Premises used: CategoryTheory.Linear.comp_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y Z : Action.{v_1, u_1, u_2} V G
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (f ≫ (r • g)).hom = (r • f ≫ g).hom

Tactic:
exact Linear.comp_smul _ _ _ _ _ _

Premises used: CategoryTheory.Linear.comp_smul
-- 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 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
r : R
f : X ⟶ Y
⊢ (r • f).hom = r • f.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
g : G
⊢ Eq.{v_1 + 1} (α := End (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
    (((ρ ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)) :
            MonoidHom.{u_2, v_1} G
              (End.{v_1, u_1} (C := V)
                (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))) :
          (a : G) → End (𝟙_ V))
        g :
      End (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
    (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst)) :
      tensorUnit.{v_1, u_1} V (𝒞 := inst) ⟶ tensorUnit.{v_1, u_1} V (𝒞 := inst))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
g : G
⊢ Eq.{v_1 + 1} (α := End (tensorObj.{v_1, u_1} (𝒞 := inst) X.V Y.V))
    (((tensorObj (𝒞 := instCategory) X Y).ρ : (a : G) → End (X.V ⊗ Y.V)) g :
      End (tensorObj.{v_1, u_1} (𝒞 := inst) X.V Y.V))
    ((X.ρ : (a : G) → End X.V) g ⊗ₘ (Y.ρ : (a : G) → End Y.V) g :
      tensorObj.{v_1, u_1} (𝒞 := inst) X.V Y.V ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X.V Y.V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
⊢ Eq.{v_1 + 1} (α :=
    tensorUnit.{v_1, u_1} V (𝒞 := inst) ⟶
      Functor.obj (C := Action.{v_1, u_1, u_2} V G) (forget V G)
        ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
    (ε (forget V G)) (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
⊢ η (forget V G) =
    𝟙
      (Functor.obj (C := Action.{v_1, u_1, u_2} V G) (forget V G)
        ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (Functor.obj (forget V G) X) (Functor.obj (forget V G) Y) ⟶
      Functor.obj (forget V G) (tensorObj (𝒞 := instCategory) X Y))
    (μ (forget V G) X Y)
    (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) (Functor.obj (forget V G) X) (Functor.obj (forget V G) Y)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
⊢ δ (forget V G) X Y = 𝟙 (Functor.obj (forget V G) (tensorObj (𝒞 := instCategory) X Y))

Tactic:
rfl

Premises used: rfl