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₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
x y : CatCommSqOver F G Y
f : x ⟶ y
⊢ ((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).map f ≫
      (mkIso (U.associator y.fst ψ.left).symm (U.associator y.snd ψ.right).symm ⋯).hom =
    (mkIso (U.associator x.fst ψ.left).symm (U.associator x.snd ψ.right).symm ⋯).hom ≫
      ((precompose F G).obj U ⋙ (transform X).obj ψ).map f

Tactic:
ext

Goal state after:
case h₁
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₁
x y : CatCommSqOver F G Y
f : x ⟶ y
x✝ : X
⊢ (((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).map f ≫
            (mkIso (U.associator y.fst ψ.left).symm (U.associator y.snd ψ.right).symm ⋯).hom).fst.app
      x✝ =
    ((mkIso (U.associator x.fst ψ.left).symm (U.associator x.snd ψ.right).symm ⋯).hom ≫
            ((precompose F G).obj U ⋙ (transform X).obj ψ).map f).fst.app
      x✝

case h₂
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₁
x y : CatCommSqOver F G Y
f : x ⟶ y
x✝ : X
⊢ (((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).map f ≫
            (mkIso (U.associator y.fst ψ.left).symm (U.associator y.snd ψ.right).symm ⋯).hom).snd.app
      x✝ =
    ((mkIso (U.associator x.fst ψ.left).symm (U.associator x.snd ψ.right).symm ⋯).hom ≫
            ((precompose F G).obj U ⋙ (transform X).obj ψ).map f).snd.app
      x✝
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:
ext

Goal state after:
case h₁
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₁
η : ψ ⟶ ψ'
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ((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).app
            x✝¹).fst.app
      x✝ =
    (((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 η)).app
            x✝¹).fst.app
      x✝

case h₂
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₁
η : ψ ⟶ ψ'
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ((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).app
            x✝¹).snd.app
      x✝ =
    (((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 η)).app
            x✝¹).snd.app
      x✝
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:
ext

Goal state after:
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✝²
x✝ : C
⊢ ((curriedTensorPre F₁).map x✝¹ ≫ { app := fun X₂ ↦ f.app x✝² ⊗ₘ f.app X₂, naturality := ⋯ }).app x✝ =
    ({ app := fun X₂ ↦ f.app x✝³ ⊗ₘ f.app X₂, naturality := ⋯ } ≫ (curriedTensorPre F₂).map x✝¹).app x✝
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:
ext

Goal state after:
case h₁
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
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((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).app
            x✝¹).fst.app
      x✝ =
    ((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).app
            x✝¹).fst.app
      x✝

case h₂
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
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((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).app
            x✝¹).snd.app
      x✝ =
    ((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).app
            x✝¹).snd.app
      x✝
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
⊢ homMk
      ((β_ A I).hom ≫
        uncurry
          (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫
            ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)))
      ⋯ =
    u

Tactic:
ext

Goal state after:
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
⊢ Hom.left
      (homMk
        ((β_ A I).hom ≫
          uncurry
            (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫
              ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)))
        ⋯) =
    Hom.left u
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:
ext

Goal state after:
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
⊢ Over.Hom.left m = Over.Hom.left (Over.homMk (lift (Over.Hom.left a) (Over.Hom.left b) ⋯) ⋯)
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:
ext

Goal state after:
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 }.of = f.of
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:
ext

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
⊢ { 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:
ext

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
⊢ (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:
ext

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.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:
ext

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
⊢ (ConcreteCategory.hom { of := ↾(f ≫ g) }.of).toFun x✝ =
    (ConcreteCategory.hom ({ of := ↾f } ≫ { of := ↾g }).of).toFun x✝
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:
ext

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.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:
ext

Goal state after:
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)).of =
    ((toKleisli T).map f ≫
        { toFun := fun f ↦ f.of, invFun := fun f ↦ { of := f }, left_inv := ⋯, right_inv := ⋯ }.symm g).of
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
x y c : C
f : x ⟶ y
d : D
⊢ (F.map (f ▷ c)).unmop.app d =
    ((Functor.Monoidal.μIso F x c).unmop.app d).symm.hom ≫
      (F.map f).unmop.app ((F.obj c).unmop.obj d) ≫ ((Functor.Monoidal.μIso F y c).unmop.app d).symm.inv

Tactic:
have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.LaxMonoidal.μ_natural_left F f c

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
x y c : C
f : x ⟶ y
d : D
e :
  (F.map f ▷ F.obj c ≫ Functor.LaxMonoidal.μ F y c).unmop.app d =
    (Functor.LaxMonoidal.μ F x c ≫ F.map (f ▷ c)).unmop.app d
⊢ (F.map (f ▷ c)).unmop.app d =
    ((Functor.Monoidal.μIso F x c).unmop.app d).symm.hom ≫
      (F.map f).unmop.app ((F.obj c).unmop.obj d) ≫ ((Functor.Monoidal.μIso F y c).unmop.app d).symm.inv
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
by
  refine Arrow.hom_ext _ _ ?_ (by simp [whisker_exchange_assoc])
  apply pushout.hom_ext <;> simp [whisker_exchange_assoc]

Goal state after:
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
⊢ ⇑(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)

Tactic:
ext

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.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)
⊢ (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((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

Tactic:
ext

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 = s.π.app h

Tactic:
ext

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 := ⋯ } =
    𝟙 P

Tactic:
ext

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
⊢ { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ } ≫ { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ } =
    𝟙 P

Tactic:
ext; dsimp; rw [Iso.hom_inv_id]

Goal state after: