awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
x : Action.{v_1, u_1, u_2} V G
h :
  Eq (α :=
    (obj (F.mapAction G) x).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))).V)
    (Hom.hom (Iso.inv (ρ_ (obj (F.mapAction G) x))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        (map (F.mapAction G) (Iso.inv (ρ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
            (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
          { hom := δ F x.V (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))),
            comm := ⋯ }
          (obj (F.mapAction G) x ◁ { hom := η F, comm := ⋯ }))))
⊢ Eq (α :=
    obj (F.mapAction G) x ⟶
      tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
    (Iso.inv (ρ_ (obj (F.mapAction G) x)))
    (CategoryStruct.comp (Y :=
      obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
      (map (F.mapAction G) (Iso.inv (ρ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
          (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        { hom := δ F x.V (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))),
          comm := ⋯ }
        (obj (F.mapAction G) x ◁ { hom := η F, comm := ⋯ })))

Tactic:
ext
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
x : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (obj (F.mapAction G) x).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))).V)
    (Hom.hom (Iso.inv (ρ_ (obj (F.mapAction G) x))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        (map (F.mapAction G) (Iso.inv (ρ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
            (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
          { hom := δ F x.V (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))),
            comm := ⋯ }
          (obj (F.mapAction G) x ◁ { hom := η F, comm := ⋯ }))))

Tactic:
simp
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
⊢ Eq (α :=
    Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) ⟶
      Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
    (Hom.hom (η (F.mapAction G))) (η F)

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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
X Y : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) X Y)).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) X) (obj (F.mapAction G) Y)).V)
    (Hom.hom (δ (F.mapAction G) X Y)) (δ F 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
h :
  Eq (α :=
    Quiver.Hom.{v_2, u_3} (V := W)
      (Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
      (Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))))
    (Hom.hom
      (CategoryStruct.comp (Y := obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
        (ε (F.mapAction G)) (η (F.mapAction G))))
    (Hom.hom (𝟙 ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))))
⊢ Eq (α :=
    Quiver.Hom (V := Action.{v_2, u_3, u_2} W G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))
      ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
    (CategoryStruct.comp (Y := obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
      (ε (F.mapAction G)) (η (F.mapAction G)))
    (𝟙 ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))

Tactic:
ext
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
h :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F) (η F) =
    𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
⊢ Eq (α :=
    Quiver.Hom.{v_2, u_3} (V := W)
      (Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
      (Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))))
    (Hom.hom
      (CategoryStruct.comp (Y := obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
        (ε (F.mapAction G)) (η (F.mapAction G))))
    (Hom.hom (𝟙 ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))))

Tactic:
dsimp
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
h h₁ :
  Eq.{v_2 + 1} (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
    (𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))) (𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)))
⊢ CategoryStruct.comp (Y := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F) (η F) =
    𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))

Tactic:
rw [ε_η]

Premises used: CategoryTheory.Functor.Monoidal.ε_η
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
h :
  Eq (α :=
    Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) ⟶
      Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
    (Hom.hom
      (CategoryStruct.comp (Y := (𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (η (F.mapAction G))
        (ε (F.mapAction G))))
    (Hom.hom (𝟙 (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))))
⊢ Eq (α :=
    Quiver.Hom (V := Action.{v_2, u_3, u_2} W G)
      (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
      (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
    (CategoryStruct.comp (Y := (𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (η (F.mapAction G))
      (ε (F.mapAction G)))
    (𝟙 (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))

Tactic:
ext
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
h :
  CategoryStruct.comp (Y := tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) (η F) (ε F) =
    𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
⊢ Eq (α :=
    Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) ⟶
      Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
    (Hom.hom
      (CategoryStruct.comp (Y := (𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (η (F.mapAction G))
        (ε (F.mapAction G))))
    (Hom.hom (𝟙 (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))))

Tactic:
dsimp
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
h h₁ :
  Eq.{v_2 + 1} (α := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
    (𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)))) (𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
⊢ CategoryStruct.comp (Y := tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) (η F) (ε F) =
    𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)))

Tactic:
rw [η_ε]

Premises used: CategoryTheory.Functor.Monoidal.η_ε
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
h :
  Hom.hom
      (CategoryStruct.comp (Y := obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)) (μ (F.mapAction G) x x_1)
        (δ (F.mapAction G) x x_1)) =
    Hom.hom (𝟙 (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1)))
⊢ CategoryStruct.comp (Y := obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)) (μ (F.mapAction G) x x_1)
      (δ (F.mapAction G) x x_1) =
    𝟙 (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))

Tactic:
ext
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
h :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V)) (μ F x.V x_1.V) (δ F x.V x_1.V) =
    𝟙 (tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V))
⊢ Hom.hom
      (CategoryStruct.comp (Y := obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)) (μ (F.mapAction G) x x_1)
        (δ (F.mapAction G) x x_1)) =
    Hom.hom (𝟙 (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1)))

Tactic:
dsimp
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
h h₁ :
  Eq.{v_2 + 1} (α :=
    tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V) ⟶
      tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V))
    (𝟙 (tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V)))
    (𝟙 (tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V)))
⊢ CategoryStruct.comp (Y := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V)) (μ F x.V x_1.V) (δ F x.V x_1.V) =
    𝟙 (tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V))

Tactic:
rw [μ_δ]

Premises used: CategoryTheory.Functor.Monoidal.μ_δ
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
h :
  Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))
        (δ (F.mapAction G) x x_1) (μ (F.mapAction G) x x_1)) =
    Hom.hom (𝟙 (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)))
⊢ CategoryStruct.comp (Y := tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))
      (δ (F.mapAction G) x x_1) (μ (F.mapAction G) x x_1) =
    𝟙 (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1))

Tactic:
ext
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
h :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V)) (δ F x.V x_1.V)
      (μ F x.V x_1.V) =
    𝟙 (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V))
⊢ Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))
        (δ (F.mapAction G) x x_1) (μ (F.mapAction G) x x_1)) =
    Hom.hom (𝟙 (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1)))

Tactic:
dsimp
-- 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
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.Monoidal
x x_1 : Action.{v_1, u_1, u_2} V G
h h₁ :
  Eq.{v_2 + 1} (α :=
    F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V))
    (𝟙 (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V))) (𝟙 (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V)))
⊢ CategoryStruct.comp (Y := tensorObj.{v_2, u_3} (𝒞 := inst_2) (F.obj x.V) (F.obj x_1.V)) (δ F x.V x_1.V)
      (μ F x.V x_1.V) =
    𝟙 (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x.V x_1.V))

Tactic:
rw [δ_μ]

Premises used: CategoryTheory.Functor.Monoidal.δ_μ
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : SingleObj M
h :
  ∀ (x_1 : X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x_2 : X) ↦ HSMul.hSMul.{u_1, u, u} (α := x ⟶ x) (𝟙 x) x_2))
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x_1
⊢ (↾fun (x_1 : X) ↦ HSMul.hSMul.{u_1, u, u} (α := x ⟶ x) (𝟙 x) x_1) = 𝟙 X

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : SingleObj M
x_1 : X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x_2 : X) ↦ HSMul.hSMul.{u_1, u, u} (α := x ⟶ x) (𝟙 x) x_2)) x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x_1

Tactic:
MulAction.one_smul _

Premises used: MulAction.one_smul
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : SingleObj M
x_1 : X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x_2 : X) ↦ HSMul.hSMul.{u_1, u, u} (α := x ⟶ x) (𝟙 x) x_2)) x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x_1

Tactic:
exact MulAction.one_smul _

Premises used: MulAction.one_smul
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
X_1 Y Z : SingleObj M
f : X_1 ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : X),
    Eq (α := X) (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : X) ↦ f ≫ g • x)) x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := X) (↾fun (x : X) ↦ f • x) (↾fun (x : X) ↦ g • x)))
        x)
⊢ Eq.{u + 1} (α := X ⟶ X) (↾fun (x : X) ↦ f ≫ g • x)
    (CategoryStruct.comp (Y := X) (↾fun (x : X) ↦ f • x) (↾fun (x : X) ↦ g • x))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
X_1 Y Z : SingleObj M
f : X_1 ⟶ Y
g : Y ⟶ Z
x : X
⊢ Eq (α := X) (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : X) ↦ f ≫ g • x)) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := X) (↾fun (x : X) ↦ f • x) (↾fun (x : X) ↦ g • x)))
      x)

Tactic:
(smul_smul g f x).symm

Premises used: smul_smul, Eq.symm
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
X_1 Y Z : SingleObj M
f : X_1 ⟶ Y
g : Y ⟶ Z
x : X
⊢ Eq (α := X) (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x : X) ↦ f ≫ g • x)) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := X) (↾fun (x : X) ↦ f • x) (↾fun (x : X) ↦ g • x)))
      x)

Tactic:
exact (smul_smul g f x).symm

Premises used: smul_smul, Eq.symm
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
p q : ActionCategory M X
f : p ⟶ q
⊢ Functor.map (π M X) f = (↑f : p.fst ⟶ q.fst)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
p : ActionCategory M X
⊢ Functor.obj (π M X) p = SingleObj.star M

Tactic:
Unit.ext _ _

Premises used: Quiver.SingleObj, Unit.ext
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
⊢ ActionCategory.back.{u, u_1} (M := M)
      (Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) () x) =
    x

Tactic:
rfl

Premises used: CategoryTheory.ActionCategory.back, rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : ActionCategory M X
mk :
  ∀ (fst : SingleObj M) (snd : Functor.obj (actionAsFunctor M X) fst),
    Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) ()
        (ActionCategory.back (Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) fst snd)) =
      Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) fst snd
⊢ Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) () x.back = x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
fst : SingleObj M
snd : Functor.obj (actionAsFunctor M X) fst
⊢ Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) ()
      (ActionCategory.back (Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) fst snd)) =
    Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) fst snd

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
p q : ActionCategory M X
⊢ (p ⟶ q) = { m : M // m • p.back = q.back }

Tactic:
rfl

Premises used: CategoryTheory.ActionCategory.back, rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
inst_2 : Nonempty X
⊢ Nonempty.{u + 1} (ActionCategory M X)

Tactic:
Nonempty.map (objEquiv M X) inferInstance

Premises used: CategoryTheory.ActionCategory.objEquiv, inferInstance, Nonempty.map, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
f : ↥(stabilizerSubmonoid M x)
⊢ (stabilizerIsoEnd M x : (a : ↥(stabilizerSubmonoid M x)) → End ⟨(), x⟩) f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
f :
  End.{u_1, u} (C := ActionCategory M X)
    (Sigma.mk (β := fun (c : SingleObj M) ↦ Functor.obj (actionAsFunctor M X) c) () x)
⊢ (MulEquiv.symm (stabilizerIsoEnd M x) : (a : End ⟨(), x⟩) → ↥(stabilizerSubmonoid M x)) f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : ActionCategory M X
⊢ (↑(𝟙 x) : x.fst ⟶ x.fst) = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x y z : ActionCategory M X
f : x ⟶ y
g : y ⟶ z
⊢ (↑(f ≫ g) : x.fst ⟶ z.fst) = (↑g : y.fst ⟶ z.fst) * (↑f : x.fst ⟶ y.fst)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
inst_2 : IsPretransitive M X
inst_3 : Nonempty X
⊢ IsConnected.{u_1, u} (ActionCategory M X)

Tactic:
zigzag_isConnected fun x y =>
    Relation.ReflTransGen.single <|
      Or.inl <| nonempty_subtype.mpr (show _ from exists_smul_eq M x.back y.back)

Premises used: Iff.mpr, nonempty_subtype, Relation.ReflTransGen.single, Or.inl, CategoryTheory.zigzag_isConnected, MulAction.exists_smul_eq, CategoryTheory.ActionCategory.back
-- Module: Mathlib.CategoryTheory.Action
Goal:
X : Type u
G : Type u_2
inst : Group G
inst_1 : MulAction G X
t : X
g : G
⊢ (↑(homOfPair t g) : ⟨(), g⁻¹ • t⟩.fst ⟶ ⟨(), t⟩.fst) = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
G : Type u_2
inst_2 : Group G
inst_3 : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : ActionCategory G X
f : a ⟶ b
refine : P (homOfPair b.back (↑f : a.fst ⟶ b.fst)) = P f
⊢ P f

Tactic:
refine cast ?_ (hyp b.back f.val)

Premises used: cast, Subtype.val, CategoryTheory.ActionCategory.back
-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
G : Type u_2
inst_2 : Group G
inst_3 : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : ActionCategory G X
f : a ⟶ b
rcases :
  ∀ (a : X) (f : Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a ⟶ b),
    P (homOfPair b.back (↑f : ⟨PUnit.unit, a⟩.fst ⟶ b.fst)) = P f
⊢ P (homOfPair b.back (↑f : a.fst ⟶ b.fst)) = P f

Tactic:
rcases a with ⟨⟨⟩, a : X⟩