awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
x_1 : Functor.obj (𝟭 (Type u)) ((ofTypeFunctor m).obj x)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
          (NatTrans.app { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ : NatTrans (𝟭 (Type u)) (ofTypeFunctor m) }
            ((ofTypeFunctor m).obj x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
              NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
            x)))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Functor.obj (𝟭 (Type u)) ((ofTypeFunctor m).obj x)))).toFun x_1

Tactic:
joinM_pure _

Premises used: joinM_pure, joinM
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
x_1 : Functor.obj (𝟭 (Type u)) ((ofTypeFunctor m).obj x)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
          (NatTrans.app { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ : NatTrans (𝟭 (Type u)) (ofTypeFunctor m) }
            ((ofTypeFunctor m).obj x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
              NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
            x)))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Functor.obj (𝟭 (Type u)) ((ofTypeFunctor m).obj x)))).toFun x_1

Tactic:
exact joinM_pure _

Premises used: joinM_pure
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
h :
  ∀ (x_1 : (ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x)),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
            ((ofTypeFunctor m).map
              (NatTrans.app
                { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ : NatTrans (𝟭 (Type u)) (ofTypeFunctor m) } x))
            (NatTrans.app
              { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
                NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
              x)))
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x)))).toFun x_1
⊢ CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
      ((ofTypeFunctor m).map (NatTrans.app { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ } x))
      (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x) =
    𝟙 ((ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
x_1 : (ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
          ((ofTypeFunctor m).map
            (NatTrans.app { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ : NatTrans (𝟭 (Type u)) (ofTypeFunctor m) }
              x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
              NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
            x)))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x)))).toFun x_1

Tactic:
joinM_map_pure _

Premises used: joinM_map_pure, joinM
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
x_1 : (ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
          ((ofTypeFunctor m).map
            (NatTrans.app { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ : NatTrans (𝟭 (Type u)) (ofTypeFunctor m) }
              x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
              NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
            x)))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x)))).toFun x_1

Tactic:
exact joinM_map_pure _

Premises used: joinM_map_pure
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : KleisliCat m
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : { of := X : Kleisli (ofTypeMonad m) }.of),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            { of := ↾(f ≫ g) :
                { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } }.of).toFun
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Kleisli.Hom.of
            ({ of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } } ≫
              { of := ↾g : { of := Y : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } })))
        x
⊢ { of := ↾(f ≫ g) : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } } =
    { of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } } ≫ { of := ↾g }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : KleisliCat m
f : X ⟶ Y
g : Y ⟶ Z
x : { of := X : Kleisli (ofTypeMonad m) }.of
h :
  (f ≫ g) x = do
    let a ← f x
    g a
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          { of := ↾(f ≫ g) : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } }.of).toFun
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Kleisli.Hom.of
          ({ of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } } ≫
            { of := ↾g : { of := Y : Kleisli (ofTypeMonad m) }.Hom { of := Z : Kleisli (ofTypeMonad m) } })))
      x

Tactic:
simp [joinM]

Premises used: joinM
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : KleisliCat m
f : X ⟶ Y
g : Y ⟶ Z
x : { of := X : Kleisli (ofTypeMonad m) }.of
⊢ (f ≫ g) x = do
    let a ← f x
    g a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : Kleisli (ofTypeMonad m)
f : X ⟶ Y
g : Y ⟶ Z
dsimp :
  Eq.{u + 1} (α := X.of ⟶ Z.of)
    (fun (x : X.of) ↦
      joinM
        (_root_.Functor.map (α := Y.of) (⇑(TypeCat.Hom.hom g.of) : (a : Y.of) → m Z.of)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)))
    (CategoryStruct.comp (Y := Y.of)
      (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x) fun (x : Y.of) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x)
⊢ Eq.{u + 1} (α := X.of ⟶ Z.of)
    (fun (x : X.of) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g).of :
          (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Z.of))
        x)
    (CategoryStruct.comp (Y := Y.of)
      (fun (x : X.of) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
            (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
          x)
      fun (x : Y.of) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) g.of :
          (a : (fun (X : Type u) ↦ X) Y.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Z.of))
        x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : Kleisli (ofTypeMonad m)
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (t : X.of),
    Eq (α := m Z.of)
      (joinM
          (_root_.Functor.map (α := Y.of) (⇑(TypeCat.Hom.hom g.of) : (a : Y.of) → m Z.of)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) t)) :
        m Z.of)
      (CategoryStruct.comp (Y := Y.of)
          (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)
          (fun (x : Y.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x) t :
        m Z.of)
⊢ Eq.{u + 1} (α := X.of ⟶ Z.of)
    (fun (x : X.of) ↦
      joinM
        (_root_.Functor.map (α := Y.of) (⇑(TypeCat.Hom.hom g.of) : (a : Y.of) → m Z.of)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)))
    (CategoryStruct.comp (Y := Y.of)
      (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x) fun (x : Y.of) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x)

Tactic:
ext t
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : Kleisli (ofTypeMonad m)
f : X ⟶ Y
g : Y ⟶ Z
t : X.of
h :
  Eq.{u + 1} (α := m Z.of)
    (do
      let a ← (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) t
      (TypeCat.Hom.hom g.of : (a : Y.of) → m Z.of) a : m Z.of)
    (CategoryStruct.comp (Y := Y.of)
        (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)
        (fun (x : Y.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x) t :
      m Z.of)
⊢ Eq (α := m Z.of)
    (joinM
        (_root_.Functor.map (α := Y.of) (⇑(TypeCat.Hom.hom g.of) : (a : Y.of) → m Z.of)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) t)) :
      m Z.of)
    (CategoryStruct.comp (Y := Y.of)
        (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)
        (fun (x : Y.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x) t :
      m Z.of)

Tactic:
simp [joinM]

Premises used: joinM
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y Z : Kleisli (ofTypeMonad m)
f : X ⟶ Y
g : Y ⟶ Z
t : X.of
⊢ Eq.{u + 1} (α := m Z.of)
    (do
      let a ← (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) t
      (TypeCat.Hom.hom g.of : (a : Y.of) → m Z.of) a : m Z.of)
    (CategoryStruct.comp (Y := Y.of)
        (fun (x : X.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) f.of : (a : X.of) → m Y.of) x)
        (fun (x : Y.of) ↦ (ConcreteCategory.hom (FC := TypeCat.Fun) g.of : (a : Y.of) → m Z.of) x) t :
      m Z.of)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
refine :
  ∀ {X Y : KleisliCat m} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (𝟭 (KleisliCat m)) X ⟶
        Functor.obj
          (Functor.comp (D := Kleisli (ofTypeMonad m))
            { obj := fun (X : KleisliCat m) ↦ { of := X }, map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦ { of := ↾f },
              map_id := ⋯, map_comp := ⋯ }
            { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
              map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
                    (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
                  x,
              map_id := ⋯, map_comp := ⋯ })
          Y)
      (Functor.map (𝟭 (KleisliCat m)) f ≫ Iso.hom ((fun (X : KleisliCat m) ↦ (Iso.refl X : X ≅ X)) Y))
      (Iso.hom ((fun (X : KleisliCat m) ↦ (Iso.refl X : X ≅ X)) X) ≫
        Functor.map
          (Functor.comp (D := Kleisli (ofTypeMonad m))
            { obj := fun (X : KleisliCat m) ↦ { of := X : Kleisli (ofTypeMonad m) },
              map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦
                { of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } },
              map_id := ⋯, map_comp := ⋯ : KleisliCat m ⥤ Kleisli (ofTypeMonad m) }
            { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
              map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
                    (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
                  x,
              map_id := ⋯, map_comp := ⋯ : Kleisli (ofTypeMonad m) ⥤ KleisliCat m })
          f)
⊢ Iso (C := KleisliCat m ⥤ KleisliCat m) (𝟭 (KleisliCat m))
    (Functor.comp (D := Kleisli (ofTypeMonad m))
      { obj := fun (X : KleisliCat m) ↦ { of := X }, map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦ { of := ↾f },
        map_id := ⋯, map_comp := ⋯ }
      { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
        map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
              (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
            x,
        map_id := ⋯, map_comp := ⋯ })

Tactic:
refine NatIso.ofComponents (fun X => Iso.refl X) fun f => ?_

Premises used: CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
change : f >=> pure = pure >=> f
⊢ Eq (α :=
    Functor.obj (𝟭 (KleisliCat m)) X ⟶
      Functor.obj
        (Functor.comp (D := Kleisli (ofTypeMonad m))
          { obj := fun (X : KleisliCat m) ↦ { of := X }, map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦ { of := ↾f },
            map_id := ⋯, map_comp := ⋯ }
          { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
            map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
                  (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
                x,
            map_id := ⋯, map_comp := ⋯ })
        Y)
    (Functor.map (𝟭 (KleisliCat m)) f ≫ Iso.hom ((fun (X : KleisliCat m) ↦ (Iso.refl X : X ≅ X)) Y))
    (Iso.hom ((fun (X : KleisliCat m) ↦ (Iso.refl X : X ≅ X)) X) ≫
      Functor.map
        (Functor.comp (D := Kleisli (ofTypeMonad m))
          { obj := fun (X : KleisliCat m) ↦ { of := X : Kleisli (ofTypeMonad m) },
            map := fun {X Y : KleisliCat m} (f : X ⟶ Y) ↦
              { of := ↾f : { of := X : Kleisli (ofTypeMonad m) }.Hom { of := Y : Kleisli (ofTypeMonad m) } },
            map_id := ⋯, map_comp := ⋯ : KleisliCat m ⥤ Kleisli (ofTypeMonad m) }
          { obj := fun (X : Kleisli (ofTypeMonad m)) ↦ X.of,
            map := fun {X Y : Kleisli (ofTypeMonad m)} (f : X ⟶ Y) (x : X.of) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.of :
                  (a : (fun (X : Type u) ↦ X) X.of) → (fun (X : Type u) ↦ X) ((ofTypeMonad m).obj Y.of))
                x,
            map_id := ⋯, map_comp := ⋯ : Kleisli (ofTypeMonad m) ⥤ KleisliCat m })
        f)

Tactic:
change f >=> pure = pure >=> f

Premises used: Pure.pure
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
⊢ f >=> pure = pure >=> f

Tactic:
simp [functor_norm]
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
⊢ ∀ {c c' d d' : C} (f : c ⟶ c') (g : d ⟶ d'),
    Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) c d ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c' d') (f ⊗ₘ g) (f ▷ d ≫ c' ◁ g)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c : C
d d' : D
f : d ⟶ d'
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c d')
    (𝟙 c ⊙ₗₘ f) (c ⊴ₗ f)

Tactic:
simp [actionHom_def]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c c' : C
f : c ⟶ c'
d : D
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c' d)
    (f ⊙ₗₘ 𝟙 d) (f ⊵ₗ d)

Tactic:
simp [actionHom_def]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
w : C
x y z : D
f : x ⟶ y
g : y ⟶ z
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ w x ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ w z)
    (w ⊴ₗ (f ≫ g)) (w ⊴ₗ f ≫ w ⊴ₗ g)

Tactic:
simp [← id_actionHom, ← actionHom_comp]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHom, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        y)
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f)
    ((tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ y)) ≫ Iso.inv (λₗ y))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        y)
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (Iso.hom (λₗ x) ≫ f ≫ Iso.inv (λₗ y))

Tactic:
rw [← Category.assoc, actionUnitIso_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        y)
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f)
    ((tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ y)) ≫ Iso.inv (λₗ y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
z z' : D
f : z ⟶ z'
simp :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z')
    (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⊙ₗₘ f) (Iso.hom (αₗ x y z) ≫ (𝟙 x ⊙ₗₘ 𝟙 y ⊙ₗₘ f) ≫ Iso.inv (αₗ x y z'))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z')
    (tensorObj.{v_1, u_1} (𝒞 := inst) x y ⊴ₗ f) (Iso.hom (αₗ x y z) ≫ x ⊴ₗ y ⊴ₗ f ≫ Iso.inv (αₗ x y z'))

Tactic:
simp only [← id_actionHom]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHom
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
z z' : D
f : z ⟶ z'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z')
    (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⊙ₗₘ f)
    ((((𝟙 x ⊗ₘ 𝟙 y) ⊙ₗₘ f) ≫ Iso.hom (αₗ x y z')) ≫ Iso.inv (αₗ x y z'))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z')
    (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⊙ₗₘ f) (Iso.hom (αₗ x y z) ≫ (𝟙 x ⊙ₗₘ 𝟙 y ⊙ₗₘ f) ≫ Iso.inv (αₗ x y z'))

Tactic:
rw [← Category.assoc, ← actionAssocIso_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
z z' : D
f : z ⟶ z'
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) x y)
        z')
    (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⊙ₗₘ f)
    ((((𝟙 x ⊗ₘ 𝟙 y) ⊙ₗₘ f) ≫ Iso.hom (αₗ x y z')) ≫ Iso.inv (αₗ x y z'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
w x y : C
f : w ⟶ x
g : x ⟶ y
z : D
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ w z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
    ((f ≫ g) ⊵ₗ z) (f ⊵ₗ z ≫ g ⊵ₗ z)

Tactic:
simp only [← actionHom_id, ← actionHom_comp, Category.id_comp]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x x' : C
f : x ⟶ x'
y : C
z : D
⊢ f ⊵ₗ @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z =
    Iso.inv (αₗ x y z) ≫ (f ▷ y) ⊵ₗ z ≫ Iso.hom (αₗ x' y z)

Tactic:
simp [whiskerRight_actionHomLeft]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerRight_actionHomLeft