mathlib-initiative/mathlib-tactics huggingface dataset:
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₇
inst✝ : Category.{v₇, u₇} X
X✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ {
      app := fun S ↦
        { fst := { app := fun y ↦ (f✝ ≫ g✝).left.app (S.fst.obj y), naturality := ⋯ },
          snd := { app := fun y ↦ (f✝ ≫ g✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
      naturality := ⋯ } =
    {
        app := fun S ↦
          { fst := { app := fun y ↦ f✝.left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ f✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } ≫
      {
        app := fun S ↦
          { fst := { app := fun y ↦ g✝.left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ g✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ }

Tactic:
;

Goal state after:
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₇
inst✝ : Category.{v₇, u₇} X
X✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ {
      app := fun S ↦
        { fst := { app := fun y ↦ (f✝ ≫ g✝).left.app (S.fst.obj y), naturality := ⋯ },
          snd := { app := fun y ↦ (f✝ ≫ g✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
      naturality := ⋯ } =
    {
        app := fun S ↦
          { fst := { app := fun y ↦ f✝.left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ f✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } ≫
      {
        app := fun S ↦
          { fst := { app := fun y ↦ g✝.left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ g✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ }
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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
X✝ : CatCommSqOver F G Y
⊢ { fst := U.whiskerLeft (𝟙 X✝).fst, snd := U.whiskerLeft (𝟙 X✝).snd, w := ⋯ } =
    𝟙
      { fst := U ⋙ X✝.fst, snd := U ⋙ X✝.snd,
        iso := U.associator X✝.fst F ≪≫ U.isoWhiskerLeft X✝.iso ≪≫ (U.associator X✝.snd G).symm }

Tactic:
;

Goal state after:
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₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
X✝ : CatCommSqOver F G Y
⊢ { fst := U.whiskerLeft (𝟙 X✝).fst, snd := U.whiskerLeft (𝟙 X✝).snd, w := ⋯ } =
    𝟙
      { fst := U ⋙ X✝.fst, snd := U ⋙ X✝.snd,
        iso := U.associator X✝.fst F ≪≫ U.isoWhiskerLeft X✝.iso ≪≫ (U.associator X✝.snd G).symm }
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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
X✝ Y✝ Z✝ : CatCommSqOver F G Y
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := U.whiskerLeft (f✝ ≫ g✝).fst, snd := U.whiskerLeft (f✝ ≫ g✝).snd, w := ⋯ } =
    { fst := U.whiskerLeft f✝.fst, snd := U.whiskerLeft f✝.snd, w := ⋯ } ≫
      { fst := U.whiskerLeft g✝.fst, snd := U.whiskerLeft g✝.snd, w := ⋯ }

Tactic:
;

Goal state after:
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₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
X✝ Y✝ Z✝ : CatCommSqOver F G Y
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := U.whiskerLeft (f✝ ≫ g✝).fst, snd := U.whiskerLeft (f✝ ≫ g✝).snd, w := ⋯ } =
    { fst := U.whiskerLeft f✝.fst, snd := U.whiskerLeft f✝.snd, w := ⋯ } ≫
      { fst := U.whiskerLeft g✝.fst, snd := U.whiskerLeft g✝.snd, w := ⋯ }
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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ : X ⥤ Y
⊢ { app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ }, naturality := ⋯ } =
    𝟙
      {
        obj := fun S ↦
          { fst := X✝ ⋙ S.fst, snd := X✝ ⋙ S.snd,
            iso := X✝.associator S.fst F ≪≫ X✝.isoWhiskerLeft S.iso ≪≫ (X✝.associator S.snd G).symm },
        map := fun {S S'} φ ↦ { fst := X✝.whiskerLeft φ.fst, snd := X✝.whiskerLeft φ.snd, w := ⋯ }, map_id := ⋯,
        map_comp := ⋯ }

Tactic:
;

Goal state after:
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₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ : X ⥤ Y
⊢ { app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ }, naturality := ⋯ } =
    𝟙
      {
        obj := fun S ↦
          { fst := X✝ ⋙ S.fst, snd := X✝ ⋙ S.snd,
            iso := X✝.associator S.fst F ≪≫ X✝.isoWhiskerLeft S.iso ≪≫ (X✝.associator S.snd G).symm },
        map := fun {S S'} φ ↦ { fst := X✝.whiskerLeft φ.fst, snd := X✝.whiskerLeft φ.snd, w := ⋯ }, map_id := ⋯,
        map_comp := ⋯ }
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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ Y✝ Z✝ : X ⥤ Y
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ { fst := whiskerRight (f✝ ≫ g✝) x.fst, snd := whiskerRight (f✝ ≫ g✝) x.snd, w := ⋯ },
      naturality := ⋯ } =
    { app := fun x ↦ { fst := whiskerRight f✝ x.fst, snd := whiskerRight f✝ x.snd, w := ⋯ }, naturality := ⋯ } ≫
      { app := fun x ↦ { fst := whiskerRight g✝ x.fst, snd := whiskerRight g✝ x.snd, w := ⋯ }, naturality := ⋯ }

Tactic:
;

Goal state after:
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₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ Y✝ Z✝ : X ⥤ Y
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ { fst := whiskerRight (f✝ ≫ g✝) x.fst, snd := whiskerRight (f✝ ≫ g✝) x.snd, w := ⋯ },
      naturality := ⋯ } =
    { app := fun x ↦ { fst := whiskerRight f✝ x.fst, snd := whiskerRight f✝ x.snd, w := ⋯ }, naturality := ⋯ } ≫
      { app := fun x ↦ { fst := whiskerRight g✝ x.fst, snd := whiskerRight g✝ x.snd, w := ⋯ }, naturality := ⋯ }
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 (𝟙 X)

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Deterministic (𝟙 X)
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✝
x : (𝟭 (Type u)).obj x✝¹
⊢ (ConcreteCategory.hom ((𝟭 (Type u)).map f ≫ ↾pure)).toFun x =
    (ConcreteCategory.hom (↾pure ≫ __Functor✝.map f)).toFun x

Tactic:
;

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝¹ x✝ : Type u
f : x✝¹ ⟶ x✝
x : (𝟭 (Type u)).obj x✝¹
⊢ (ConcreteCategory.hom ((𝟭 (Type u)).map f ≫ ↾pure)).toFun x =
    (ConcreteCategory.hom (↾pure ≫ __Functor✝.map f)).toFun x
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✝²
x✝ : (__Functor✝ ⋙ __Functor✝).obj x✝³
⊢ (ConcreteCategory.hom ((__Functor✝ ⋙ __Functor✝).map x✝¹ ≫ ↾joinM)).toFun x✝ =
    (ConcreteCategory.hom (↾joinM ≫ __Functor✝.map x✝¹)).toFun x✝

Tactic:
;

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝³ x✝² : Type u
x✝¹ : x✝³ ⟶ x✝²
x✝ : (__Functor✝ ⋙ __Functor✝).obj x✝³
⊢ (ConcreteCategory.hom ((__Functor✝ ⋙ __Functor✝).map x✝¹ ≫ ↾joinM)).toFun x✝ =
    (ConcreteCategory.hom (↾joinM ≫ __Functor✝.map x✝¹)).toFun x✝
Module: Mathlib.CategoryTheory.Monad.Types

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

Tactic:
;

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝¹ : Type u
x✝ : (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj x✝¹)
⊢ (ConcreteCategory.hom
          ((ofTypeFunctor m).map ({ app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝¹) ≫
            { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          ({ app := fun X ↦ ↾joinM, naturality := ⋯ }.app ((ofTypeFunctor m).obj x✝¹) ≫
            { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝¹)).toFun
      x✝
Module: Mathlib.CategoryTheory.Monad.Types

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

Tactic:
;

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝¹ : Type u
x✝ : (𝟭 (Type u)).obj ((ofTypeFunctor m).obj x✝¹)
⊢ (ConcreteCategory.hom
          ({ app := fun X ↦ ↾pure, naturality := ⋯ }.app ((ofTypeFunctor m).obj x✝¹) ≫
            { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (𝟙 ((𝟭 (Type u)).obj ((ofTypeFunctor m).obj x✝¹)))).toFun x✝
Module: Mathlib.CategoryTheory.Monad.Types

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

Tactic:
;

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝¹ : Type u
x✝ : (ofTypeFunctor m).obj ((𝟭 (Type u)).obj x✝¹)
⊢ (ConcreteCategory.hom
          ((ofTypeFunctor m).map ({ app := fun X ↦ ↾pure, naturality := ⋯ }.app x✝¹) ≫
            { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (𝟙 ((ofTypeFunctor m).obj ((𝟭 (Type u)).obj x✝¹)))).toFun x✝
Module: Mathlib.CategoryTheory.Monad.EquivMon

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

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
M : Monad C
x✝ : C
⊢ (MonoidalCategoryStruct.whiskerRight M.μ M.toFunctor ≫ M.μ).app x✝ =
    ((MonoidalCategoryStruct.associator M.toFunctor M.toFunctor M.toFunctor).hom ≫
          MonoidalCategoryStruct.whiskerLeft M.toFunctor M.μ ≫ M.μ).app
      x✝
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:
simpa [-MonObj.one_mul] using! congrArg (fun t ↦ t.app X) (one_mul M.X)

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✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this : HasCoequalizerOfIsSplitPair G
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : G.IsSplitPair f✝ g✝
⊢ PreservesColimit (parallelPair f✝ g✝) G

Tactic:
;

Goal state after:
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✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this : HasCoequalizerOfIsSplitPair G
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : G.IsSplitPair f✝ g✝
⊢ PreservesColimit (parallelPair f✝ g✝) G
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✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this✝ : HasCoequalizerOfIsSplitPair G
this : PreservesColimitOfIsSplitPair G
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : G.IsSplitPair f✝ g✝
⊢ ReflectsColimit (parallelPair f✝ g✝) G

Tactic:
;

Goal state after:
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✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this✝ : HasCoequalizerOfIsSplitPair G
this : PreservesColimitOfIsSplitPair G
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : G.IsSplitPair f✝ g✝
⊢ ReflectsColimit (parallelPair f✝ g✝) G
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
x✝ : (fun X ↦ X) ((coyoneda.obj (Opposite.op (L.obj ((L ⋙ R).obj d ⊗ d')))).obj c)
⊢ (ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) x✝ =
    (⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
        ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
          ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c))
      x✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
x✝ : (fun X ↦ X) ((coyoneda.obj (Opposite.op (L.obj ((L ⋙ R).obj d ⊗ d')))).obj c)
⊢ (ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) x✝ =
    (⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
        ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
          ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c))
      x✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
i j : J
f : i ⟶ j
this : ((Functor.const J).obj c.pt).map f ≫ c.π.app j = c.π.app i ≫ (F ⋙ forget C).map f
⊢ ((Functor.const J).obj (c.1 ⊗ c.1)).map f ≫ (c.π.app j ⊗ₘ c.π.app j) ≫ μ =
    ((c.π.app i ⊗ₘ c.π.app i) ≫ μ) ≫ (F ⋙ forget C).map f

Tactic:
;

Goal state after:
J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
i j : J
f : i ⟶ j
this : ((Functor.const J).obj c.pt).map f ≫ c.π.app j = c.π.app i ≫ (F ⋙ forget C).map f
⊢ ((Functor.const J).obj (c.1 ⊗ c.1)).map f ≫ (c.π.app j ⊗ₘ c.π.app j) ≫ μ =
    ((c.π.app i ⊗ₘ c.π.app i) ≫ μ) ≫ (F ⋙ forget C).map f
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
x✝ : (coyoneda.obj (Opposite.op ((L ⋙ R).obj d ⊗ d'))).obj (R.obj c)
⊢ (ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))).toFun x✝ =
    (ConcreteCategory.hom
          (((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
            (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
              ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom)).toFun
      x✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
x✝ : (coyoneda.obj (Opposite.op ((L ⋙ R).obj d ⊗ d'))).obj (R.obj c)
⊢ (ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))).toFun x✝ =
    (ConcreteCategory.hom
          (((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
            (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
              ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom)).toFun
      x✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
h : J
⊢ ({ hom := hc.lift ((forget C).mapCone s), isMonHom_hom := ⋯ } ≫ (limitCone F c hc).π.app h).hom = (s.π.app h).hom

Tactic:
;

Goal state after:
J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
h : J
⊢ ({ hom := hc.lift ((forget C).mapCone s), isMonHom_hom := ⋯ } ≫ (limitCone F c hc).π.app h).hom = (s.π.app h).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ ({ hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ } ≫
        { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ }).hom =
    (𝟙 P).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ ({ hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ } ≫
        { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ }).hom =
    (𝟙 P).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ f.hom ≫ f.inv = 𝟙 P.X

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ f.hom ≫ f.inv = 𝟙 P.X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ ({ hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ } ≫
        { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ }).hom =
    (𝟙 Q).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ ({ hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ } ≫
        { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ }).hom =
    (𝟙 Q).hom