mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Multifunctor

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalCategory D
F₁ F₂ : C ⥤ D
f : F₁ ⟶ F₂
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ (curriedTensorPre F₁).map x✝ ≫ { app := fun X₂ ↦ f.app x✝¹ ⊗ₘ f.app X₂, naturality := ⋯ } =
    { app := fun X₂ ↦ f.app x✝² ⊗ₘ f.app X₂, naturality := ⋯ } ≫ (curriedTensorPre F₂).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MarkovCategory C
X : C
f : X ⟶ 𝟙_ C
⊢ f ≫ ε = ε

Tactic:
discard_natural

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MarkovCategory C
X : C
f : X ⟶ 𝟙_ C
⊢ ε = ε
Module: Mathlib.CategoryTheory.MarkovCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MarkovCategory C
X : C
f : X ⟶ 𝟙_ C
⊢ f = ε

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ f ≫ Δ = f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y) = (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Deterministic (f ≫ inv f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) = Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y) = Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝⁴ : Category.{v₄, u₄} A₁
inst✝³ : Category.{v₅, u₅} B₁
inst✝² : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
⊢ whiskerRight ((transform Y).map η) ((precompose F₁ G₁).obj U) ≫
      (CatCommSq.iso ((transform Y).obj ψ') ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
          ((transform X).obj ψ')).hom =
    (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
          ((transform X).obj ψ)).hom ≫
      ((precompose F G).obj U).whiskerLeft ((transform X).map η)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y) = Δ ≫ (f ⊗ₘ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ f ≫ Δ = Δ ≫ (f ⊗ₘ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
⊢ ((β_ A I).hom ≫ uncurry v₂) ≫ X.hom = ((toOver I).obj A).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
⊢ sectionsCurry (sectionsUncurry v) = v

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
F : A ⥤ B
G : C ⥤ B
⊢ (CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U)
          ((transform X).obj (CatCospanTransform.id F G))).hom ≫
      ((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom =
    whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U) ≫
      ((precompose F G).obj U).leftUnitor.hom ≫ ((precompose F G).obj U).rightUnitor.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ sectionsUncurry (sectionsCurry u) = u

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
⊢ ∀ {X' X : C} {Y : Over I} (f : X' ⟶ X) (g : X ⟶ (sections I).obj Y),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
      (toOver I).map f ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝¹⁰ : Category.{v₁, u₁} A
inst✝⁹ : Category.{v₂, u₂} B
inst✝⁸ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝⁷ : Category.{v₄, u₄} A₁
inst✝⁶ : Category.{v₅, u₅} B₁
inst✝⁵ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
A₂ : Type u₇
B₂ : Type u₈
C₂ : Type u₉
inst✝⁴ : Category.{v₇, u₇} A₂
inst✝³ : Category.{v₈, u₈} B₂
inst✝² : Category.{v₉, u₉} C₂
F₂ : A₂ ⥤ B₂
G₂ : C₂ ⥤ B₂
X : Type u₁₀
Y : Type u₁₁
inst✝¹ : Category.{v₁₀, u₁₀} X
inst✝ : Category.{v₁₁, u₁₁} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
⊢ (CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
          ((transform X).obj (ψ.comp ψ'))).hom ≫
      ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom =
    whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
      (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
        ((transform Y).obj ψ).whiskerLeft
            (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                ((transform X).obj ψ')).hom ≫
          (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
            whiskerRight
                (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                    ((transform X).obj ψ)).hom
                ((transform X).obj ψ') ≫
              (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
⊢ ∀ {X : C} {Y Y' : Over I} (f : (toOver I).obj X ⟶ Y) (g : Y ⟶ Y'),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
u : T✝ ⟶ Y
v : T✝ ⟶ Z
⊢ Over.Hom.left u ≫ Y.hom = Over.Hom.left v ≫ Z.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
u : T✝ ⟶ Y
v : T✝ ⟶ Z
⊢ lift (Over.Hom.left u) (Over.Hom.left v) ⋯ ≫ (binaryFan Y Z).pt.hom = T✝.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
⊢ ∀ {T : Over X} (f : T ⟶ Y) (g : T ⟶ Z),
    Over.homMk (lift (Over.Hom.left f) (Over.Hom.left g) ⋯) ⋯ ≫ (binaryFan Y Z).fst = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
⊢ ∀ {T : Over X} (f : T ⟶ Y) (g : T ⟶ Z),
    Over.homMk (lift (Over.Hom.left f) (Over.Hom.left g) ⋯) ⋯ ≫ (binaryFan Y Z).snd = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
a : T✝ ⟶ Y
b : T✝ ⟶ Z
m : T✝ ⟶ (binaryFan Y Z).pt
h₁ : m ≫ (binaryFan Y Z).fst = a
h₂ : m ≫ (binaryFan Y Z).snd = b
⊢ m = Over.homMk (lift (Over.Hom.left a) (Over.Hom.left b) ⋯) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenPullbacks C
X : C
Y : Over X
m : Y ⟶ Over.mk (𝟙 X)
⊢ Over.Hom.left m = Over.Hom.left (Over.homMk Y.hom ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X A A' : C
f : A ⟶ A'
⊢ (toOver X).map f = Over.homMk (f ▷ X) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ ((forgetAdjToOver X).homEquiv Z A).symm f = Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ { of := { of := T.η.app X.of }.of ≫ T.map f.of ≫ T.μ.app Y.of } = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝¹ x✝ : Type u
f : x✝¹ ⟶ x✝
⊢ (𝟭 (Type u)).map f ≫ ↾pure = ↾pure ≫ __Functor✝.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝² x✝¹ : Type u
x✝ : x✝² ⟶ x✝¹
⊢ (__Functor✝ ⋙ __Functor✝).map x✝ ≫ ↾joinM = ↾joinM ≫ __Functor✝.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝ : Type u
⊢ (ofTypeFunctor m).map ({ app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝ =
    { app := fun X ↦ ↾joinM, naturality := ⋯ }.app ((ofTypeFunctor m).obj x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝ : Type u
⊢ { app := fun X ↦ ↾pure, naturality := ⋯ }.app ((ofTypeFunctor m).obj x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝ =
    𝟙 ((𝟭 (Type u)).obj ((ofTypeFunctor m).obj x✝))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝ : Type u
⊢ (ofTypeFunctor m).map ({ app := fun X ↦ ↾pure, naturality := ⋯ }.app x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝ =
    𝟙 ((ofTypeFunctor m).obj ((𝟭 (Type u)).obj x✝))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : { of := X✝ }.of
⊢ (ConcreteCategory.hom { of := ↾(f ≫ g) }.of).toFun x✝ =
    (ConcreteCategory.hom ({ of := ↾f } ≫ { of := ↾g }).of).toFun x✝

Tactic:
simp [joinM]

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : { of := X✝ }.of
⊢ (f ≫ g) x✝ = do
    let a ← f x✝
    g a
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { of := ↾(f ≫ g) } = { of := ↾f } ≫ { of := ↾g }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
W✝ X✝ Y✝ Z✝ : Kleisli T
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ { of := { of := f.of ≫ T.map g.of ≫ T.μ.app Y✝.of }.of ≫ T.map h.of ≫ T.μ.app Z✝.of } =
    { of := f.of ≫ T.map { of := g.of ≫ T.map h.of ≫ T.μ.app Z✝.of }.of ≫ T.μ.app Z✝.of }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : Monad C
⊢ MonoidalCategoryStruct.whiskerRight M.μ M.toFunctor ≫ M.μ =
    (MonoidalCategoryStruct.associator M.toFunctor M.toFunctor M.toFunctor).hom ≫
      MonoidalCategoryStruct.whiskerLeft M.toFunctor M.μ ≫ M.μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : Mon (C ⥤ C)
X : C
⊢ M.X.map (μ.app X) ≫ μ.app X = μ.app (M.X.obj X) ≫ μ.app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : X✝.of
⊢ joinM (⇑(TypeCat.Hom.hom g.of) <$> (ConcreteCategory.hom f.of) t) =
    ((fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x) t

Tactic:
simp [joinM]

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : X✝.of
⊢ (do
      let a ← (ConcreteCategory.hom f.of) t
      (TypeCat.Hom.hom g.of) a) =
    ((fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x) t
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : Mon (C ⥤ C)
X : C
⊢ η.app (M.X.obj X) ≫ μ.app X = 𝟙 ((𝟭 C).obj (M.X.obj X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun x ↦ (ConcreteCategory.hom (f ≫ g).of) x) =
    (fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : Mon (C ⥤ C)
X : C
⊢ M.X.map (η.app X) ≫ μ.app X = 𝟙 (M.X.obj ((𝟭 C).obj X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : Mon (C ⥤ C)
f : X✝ ⟶ Y
X : C
⊢ (ofMon X✝).η.app X ≫ f.hom.app X = (ofMon Y).η.app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
⊢ 𝟭 (KleisliCat m) ≅
    { obj := fun X ↦ { of := X }, map := fun {X Y} f ↦ { of := ↾f }, map_id := ⋯, map_comp := ⋯ } ⋙
      { obj := fun X ↦ X.of, map := fun {X Y} f x ↦ (ConcreteCategory.hom f.of) x, map_id := ⋯, map_comp := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Mon (C ⥤ C)
f : X ⟶ Y
Z : C
⊢ (ofMon X).μ.app Z ≫ f.hom.app Z = ((ofMon X).map (f.hom.app Z) ≫ f.hom.app ((ofMon Y).obj Z)) ≫ (ofMon Y).μ.app Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { of := (f ≫ g) ≫ T.η.app Z } = { of := f ≫ T.η.app Y } ≫ { of := g ≫ T.η.app Z }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ Z
⊢ T.map (f ≫ g).of ≫ T.μ.app Z.of = (T.map f.of ≫ T.μ.app Y.of) ≫ T.map g.of ≫ T.μ.app Z.of

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
⊢ { toFun := fun f ↦ f.of, invFun := fun f ↦ { of := f }, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
    (toKleisli T).map f ≫ { toFun := fun f ↦ f.of, invFun := fun f ↦ { of := f }, left_inv := ⋯, right_inv := ⋯ }.symm g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X : Cokleisli U
Y x✝ : C
f : (fromCokleisli U).obj X ⟶ Y
g : Y ⟶ x✝
⊢ { toFun := fun f ↦ { of := f }, invFun := fun f ↦ f.of, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
    { toFun := fun f ↦ { of := f }, invFun := fun f ↦ f.of, left_inv := ⋯, right_inv := ⋯ } f ≫ (toCokleisli U).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalLeftAction C D
inst✝¹ : MonoidalLeftAction C D'
inst✝ : F.LaxLeftLinear C
c c' : C
d : D
⊢ c ⊴ₗ μₗ F c' d ≫ μₗ F c (c' ⊙ₗ d) ≫ F.map (αₗ c c' d).inv = (αₗ c c' (F.obj d)).inv ≫ μₗ F (c ⊗ c') d

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalLeftAction C D
inst✝¹ : MonoidalLeftAction C D'
inst✝ : F.LaxLeftLinear C
d : D
⊢ (λₗ (F.obj d)).inv ≫ μₗ F (𝟙_ C) d = F.map (λₗ d).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalLeftAction C D
inst✝¹ : MonoidalLeftAction C D'
inst✝ : F.OplaxLeftLinear C
c c' : C
d : D
⊢ δₗ F c (c' ⊙ₗ d) ≫ c ⊴ₗ δₗ F c' d ≫ (αₗ c c' (F.obj d)).inv = F.map (αₗ c c' d).inv ≫ δₗ F (c ⊗ c') d

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalLeftAction C D
inst✝¹ : MonoidalLeftAction C D'
inst✝ : F.OplaxLeftLinear C
d : D
⊢ δₗ F (𝟙_ C) d ≫ (λₗ (F.obj d)).hom = F.map (λₗ d).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalRightAction C D
inst✝¹ : MonoidalRightAction C D'
inst✝ : F.LaxRightLinear C
d : D
c c' : C
⊢ μᵣ F d c ⊵ᵣ c' ≫ μᵣ F (d ⊙ᵣ c) c' ≫ F.map (αᵣ d c c').inv = (αᵣ (F.obj d) c c').inv ≫ μᵣ F d (c ⊗ c')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalRightAction C D
inst✝¹ : MonoidalRightAction C D'
inst✝ : F.LaxRightLinear C
d : D
⊢ (ρᵣ (F.obj d)).inv ≫ μᵣ F d (𝟙_ C) = F.map (ρᵣ d).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalRightAction C D
inst✝¹ : MonoidalRightAction C D'
inst✝ : F.OplaxRightLinear C
d : D
c c' : C
⊢ δᵣ F (d ⊙ᵣ c) c' ≫ δᵣ F d c ⊵ᵣ c' ≫ (αᵣ (F.obj d) c c').inv = F.map (αᵣ d c c').inv ≫ δᵣ F d (c ⊗ c')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalRightAction C D
inst✝¹ : MonoidalRightAction C D'
inst✝ : F.OplaxRightLinear C
d : D
⊢ δᵣ F d (𝟙_ C) ≫ (ρᵣ (F.obj d)).hom = F.map (ρᵣ d).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ { f // F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f } ≃
    { g // G.map (F.map g) ≫ G.map (adj.counit.app B) = A.a ≫ g }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ adj.toMonad.Algebra ⥤ D

Tactic:
by

Goal state after: