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

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 C
inst✝ : MonoidalRightAction C D
x y : D
f : x ⟶ y
⊢ f ⊵ᵣ 𝟙_ C = (f ⊵ᵣ 𝟙_ C ≫ (ρᵣ y).hom) ≫ (ρᵣ y).inv

Tactic:
simp

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

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 C
inst✝ : MonoidalRightAction C D
z z' : D
f : z ⟶ z'
x y : C
⊢ f ⊙ᵣₘ 𝟙 (x ⊗ y) = ((f ⊙ᵣₘ 𝟙 x ⊗ₘ 𝟙 y) ≫ (αᵣ z' x y).hom) ≫ (αᵣ z' x y).inv

Tactic:
simp

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

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 C
inst✝¹ : MonoidalRightAction C D
x y : D
f : x ⟶ y
inst✝ : IsIso f
z : C
⊢ f ⊵ᵣ z ≫ inv f ⊵ᵣ z = 𝟙 (x ⊙ᵣ z) ∧ inv f ⊵ᵣ z ≫ f ⊵ᵣ z = 𝟙 (y ⊙ᵣ z)

Tactic:
simp

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

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 C
inst✝¹ : MonoidalRightAction C D
x : D
y z : C
f : y ⟶ z
inst✝ : IsIso f
⊢ x ⊴ᵣ f ≫ x ⊴ᵣ inv f = 𝟙 (x ⊙ᵣ y) ∧ x ⊴ᵣ inv f ≫ x ⊴ᵣ f = 𝟙 (x ⊙ᵣ z)

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction C D
d✝ d'✝ : Dᵒᵖ
x✝ : d✝ ⟶ d'✝
⊢ ((λₗ (unop d✝)).symm.op.hom ≫ x✝).unop = ((unop (𝟙_ Cᵒᵖ) ⊴ₗ x✝.unop).op ≫ (λₗ (unop d'✝)).symm.op.hom).unop

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction C D
c✝ c'✝ x✝² : Cᵒᵖ
x✝¹ : c✝ ⟶ c'✝
x✝ : Dᵒᵖ
⊢ ((x✝¹ ▷ x✝²).unop ⊵ₗ unop x✝).op.unop =
    ((αₗ (unop c✝) (unop x✝²) (unop x✝)).symm.op.hom ≫
        (x✝¹.unop ⊵ₗ unop (op (unop x✝² ⊙ₗ unop x✝))).op ≫ (αₗ (unop c'✝) (unop x✝²) (unop x✝)).symm.op.inv).unop

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction C D
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ inv
      (((α_ x✝³ x✝² x✝¹).hom.unop ⊵ₗ unop x✝).op ≫
          (αₗ (unop x✝³) (unop (x✝² ⊗ x✝¹)) (unop x✝)).symm.op.hom ≫
            (unop x✝³ ⊴ₗ (αₗ (unop x✝²) (unop x✝¹) (unop x✝)).symm.op.hom.unop).op).unop =
    inv
      ((αₗ (unop (x✝³ ⊗ x✝²)) (unop x✝¹) (unop x✝)).symm.op.hom ≫
          (αₗ (unop x✝³) (unop x✝²) (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom).unop

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ inv ((λ_ x✝¹).hom.unop ⊵ₗ unop x✝).op.unop =
    inv
      ((αₗ (unop (𝟙_ Cᵒᵖ)) (unop x✝¹) (unop x✝)).symm.op.hom ≫ (λₗ (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom).unop

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ inv ((ρ_ x✝¹).hom.unop ⊵ₗ unop x✝).op.unop =
    inv ((αₗ (unop x✝¹) (unop (𝟙_ Cᵒᵖ)) (unop x✝)).symm.op.hom ≫ (unop x✝¹ ⊴ₗ (λₗ (unop x✝)).symm.op.hom.unop).op).unop

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
d✝ d'✝ : D
x✝ : d✝ ⟶ d'✝
⊢ ((λₗ (op d✝)).symm.unop.hom ≫ x✝).op = ((op (𝟙_ C) ⊴ₗ x✝.op).unop ≫ (λₗ (op d'✝)).symm.unop.hom).op

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
c✝ c'✝ x✝² : C
x✝¹ : c✝ ⟶ c'✝
x✝ : D
⊢ ((x✝¹ ▷ x✝²).op ⊵ₗ op x✝).unop.op =
    ((αₗ (op c✝) (op x✝²) (op x✝)).symm.unop.hom ≫
        (x✝¹.op ⊵ₗ op (unop (op x✝² ⊙ₗ op x✝))).unop ≫ (αₗ (op c'✝) (op x✝²) (op x✝)).symm.unop.inv).op

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ inv
      (((α_ x✝³ x✝² x✝¹).hom.op ⊵ₗ op x✝).unop ≫
          (αₗ (op x✝³) (op (x✝² ⊗ x✝¹)) (op x✝)).symm.unop.hom ≫
            (op x✝³ ⊴ₗ (αₗ (op x✝²) (op x✝¹) (op x✝)).symm.unop.hom.op).unop).op =
    inv
      ((αₗ (op (x✝³ ⊗ x✝²)) (op x✝¹) (op x✝)).symm.unop.hom ≫
          (αₗ (op x✝³) (op x✝²) (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom).op

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ inv ((λ_ x✝¹).hom.op ⊵ₗ op x✝).unop.op =
    inv ((αₗ (op (𝟙_ C)) (op x✝¹) (op x✝)).symm.unop.hom ≫ (λₗ (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom).op

Tactic:
simp

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

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ inv ((ρ_ x✝¹).hom.op ⊵ₗ op x✝).unop.op =
    inv ((αₗ (op x✝¹) (op (𝟙_ C)) (op x✝)).symm.unop.hom ≫ (op x✝¹ ⊴ₗ (λₗ (op x✝)).symm.unop.hom.op).unop).op

Tactic:
simp

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

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
inst✝ : MonoidalRightAction C D
d✝ d'✝ : Dᵒᵖ
x✝ : d✝ ⟶ d'✝
⊢ ((ρᵣ (unop d✝)).symm.op.hom ≫ x✝).unop = ((x✝.unop ⊵ᵣ unop (𝟙_ Cᵒᵖ)).op ≫ (ρᵣ (unop d'✝)).symm.op.hom).unop

Tactic:
simp

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

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
inst✝ : MonoidalRightAction C D
x✝⁴ x✝³ x✝² : Cᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (x✝⁴ ◁ x✝¹).unop).op.unop =
    ((αᵣ (unop x✝) (unop x✝⁴) (unop x✝³)).symm.op.hom ≫
        (unop (op (unop x✝ ⊙ᵣ unop x✝⁴)) ⊴ᵣ x✝¹.unop).op ≫ (αᵣ (unop x✝) (unop x✝⁴) (unop x✝²)).symm.op.inv).unop

Tactic:
simp

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

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
inst✝ : MonoidalRightAction C D
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ inv
      ((unop x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.unop).op ≫
          (αᵣ (unop x✝) (unop x✝³) (unop (x✝² ⊗ x✝¹))).symm.op.hom ≫
            (αᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝³))) (unop x✝²) (unop x✝¹)).symm.op.hom).unop =
    inv
      ((αᵣ (unop x✝) (unop (x✝³ ⊗ x✝²)) (unop x✝¹)).symm.op.hom ≫
          ((αᵣ (unop x✝) (unop x✝³) (unop x✝²)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op).unop

Tactic:
simp

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

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
inst✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ inv (unop x✝ ⊴ᵣ (λ_ x✝¹).hom.unop).op.unop =
    inv ((αᵣ (unop x✝) (unop (𝟙_ Cᵒᵖ)) (unop x✝¹)).symm.op.hom ≫ ((ρᵣ (unop x✝)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op).unop

Tactic:
simp

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

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
inst✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ inv (unop x✝ ⊴ᵣ (ρ_ x✝¹).hom.unop).op.unop =
    inv
      ((αᵣ (unop x✝) (unop x✝¹) (unop (𝟙_ Cᵒᵖ))).symm.op.hom ≫ (ρᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝¹)))).symm.op.hom).unop

Tactic:
simp

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

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
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
d✝ d'✝ : D
x✝ : d✝ ⟶ d'✝
⊢ ((ρᵣ (op d✝)).symm.unop.hom ≫ x✝).op = ((x✝.op ⊵ᵣ op (𝟙_ C)).unop ≫ (ρᵣ (op d'✝)).symm.unop.hom).op

Tactic:
simp

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

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
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝⁴ x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : D
⊢ (op x✝ ⊴ᵣ (x✝⁴ ◁ x✝¹).op).unop.op =
    ((αᵣ (op x✝) (op x✝⁴) (op x✝³)).symm.unop.hom ≫
        (op (unop (op x✝ ⊙ᵣ op x✝⁴)) ⊴ᵣ x✝¹.op).unop ≫ (αᵣ (op x✝) (op x✝⁴) (op x✝²)).symm.unop.inv).op

Tactic:
simp

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

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
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ inv
      ((op x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.op).unop ≫
          (αᵣ (op x✝) (op x✝³) (op (x✝² ⊗ x✝¹))).symm.unop.hom ≫
            (αᵣ (op (unop (op x✝ ⊙ᵣ op x✝³))) (op x✝²) (op x✝¹)).symm.unop.hom).op =
    inv
      ((αᵣ (op x✝) (op (x✝³ ⊗ x✝²)) (op x✝¹)).symm.unop.hom ≫
          ((αᵣ (op x✝) (op x✝³) (op x✝²)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop).op

Tactic:
simp

Goal state after:
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₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Arrow.Hom.right (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) = Arrow.Hom.right ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
simp

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

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
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ inv (op x✝ ⊴ᵣ (λ_ x✝¹).hom.op).unop.op =
    inv ((αᵣ (op x✝) (op (𝟙_ C)) (op x✝¹)).symm.unop.hom ≫ ((ρᵣ (op x✝)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop).op

Tactic:
simp

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

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
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ inv (op x✝ ⊴ᵣ (ρ_ x✝¹).hom.op).unop.op =
    inv ((αᵣ (op x✝) (op x✝¹) (op (𝟙_ C))).symm.unop.hom ≫ (ρᵣ (op (unop (op x✝ ⊙ᵣ op x✝¹)))).symm.unop.hom).op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ μ ≫ Δ = Δ ≫ (μ ⊗ₘ μ)

Tactic:
simp

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
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      (((adj.unit.app ((ihom d).obj (R.obj c) ⊗ d) ≫
              R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d)) ≫
                inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d)))) ≫
            R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)) ≫
          R.map (L.map ((ihom.ev d).app (R.obj c)))) ≫
        inv (adj.unit.app (R.1 c)) =
    (ihom.ev d).app (R.obj c)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : BimonObj M
⊢ η ≫ Δ = (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : BimonObj M
⊢ μ ≫ ε = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom

Tactic:
simp

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
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:
simp

Goal state after:
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
⊢ ∀ (j : J),
    ((forget C).mapCone (limitCone F c hc)).π.app j =
      (Iso.refl ((forget C).mapCone (limitCone F c hc)).pt).hom ≫ c.π.app j

Tactic:
simp

Goal state after:
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
⊢ ∀ (j : J), (η ≫ hc.lift ((forget C).mapCone s)) ≫ c.π.app j = η ≫ c.π.app j

Tactic:
simp

Goal state after:
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
⊢ ∀ (j : J),
    (μ ≫ hc.lift ((forget C).mapCone s)) ≫ c.π.app j =
      ((hc.lift ((forget C).mapCone s) ⊗ₘ hc.lift ((forget C).mapCone s)) ≫ μ) ≫ c.π.app j

Tactic:
simp

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
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:
simp

Goal state after:
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:
simp

Goal state after:
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 : Arrow C
f : X ⟶ Y
⊢ pushout.inl (((curriedTensor C).map (𝟙_ (Arrow C)).hom).app X.left)
        (((curriedTensor C).obj (𝟙_ (Arrow C)).left).map X.hom) ≫
      Arrow.Hom.left (𝟙_ (Arrow C) ◁ f ≫ (λ_ Y).hom) =
    pushout.inl (((curriedTensor C).map (𝟙_ (Arrow C)).hom).app X.left)
        (((curriedTensor C).obj (𝟙_ (Arrow C)).left).map X.hom) ≫
      Arrow.Hom.left ((λ_ X).hom ≫ f)

Tactic:
simp

Goal state after:
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 : Arrow C
f : X ⟶ Y
⊢ Arrow.Hom.right (𝟙_ (Arrow C) ◁ f ≫ (λ_ Y).hom) = Arrow.Hom.right ((λ_ X).hom ≫ f)

Tactic:
simp

Goal state after:
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 : Arrow C
f : X ⟶ Y
⊢ pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
        (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom) ≫
      Arrow.Hom.left (f ▷ 𝟙_ (Arrow C) ≫ (ρ_ Y).hom) =
    pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
        (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom) ≫
      Arrow.Hom.left ((ρ_ X).hom ≫ f)

Tactic:
simp

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
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)
w₂ :
  (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
x✝ : (fun X ↦ X) ((coyoneda.obj (Opposite.op (d' ⊗ (L ⋙ R).obj d))).obj (R.obj c))
⊢ (ConcreteCategory.hom ((yoneda.obj (R.obj c)).map (d' ◁ adj.unit.app d).op)) x✝ =
    (tensorLeft d').map
        ((ConcreteCategory.hom ((yoneda.obj ((ihom d').obj (R.obj c))).map (adj.unit.app d).op))
          ((ihom.adjunction d').unit.app (R.obj (L.obj d)) ≫ (ihom d').map x✝)) ≫
      (ihom.adjunction d').counit.app (R.obj c)

Tactic:
simp

Goal state after:
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 : Arrow C
f : X ⟶ Y
⊢ Arrow.Hom.right (f ▷ 𝟙_ (Arrow C) ≫ (ρ_ Y).hom) = Arrow.Hom.right ((ρ_ X).hom ≫ f)

Tactic:
simp

Goal state after:
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
W X Y Z : Arrow C
⊢ pushout.inl (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
        (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    pushout.inl (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
        (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
simp

Goal state after:
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
W X Y Z : Arrow C
⊢ Arrow.Hom.right ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    Arrow.Hom.right ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
simp

Goal state after:
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
W X Y Z : Arrow C
⊢ (tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
          (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
          (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    (tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
          (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
          (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
simp

Goal state after:
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
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ ((α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (R.X ◁ P.actRight) ▷ Q.X) ≫ P.actLeft ▷ Q.X =
    (α_ R.X (P.X ⊗ S.X) Q.X).inv ≫
      (α_ R.X P.X S.X).inv ▷ Q.X ≫ (α_ R.X P.X S.X).hom ▷ Q.X ≫ (R.X ◁ P.actRight ≫ P.actLeft) ▷ Q.X

Tactic:
simp

Goal state after: