mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : MonoidalRightAction C D
c₁ c₂ c₃ : C
⊢ { app := fun x ↦ (αᵣ x c₁ c₂).inv, naturality := ⋯ } ▷ (curriedAction C D).obj c₃ ≫
      { app := fun x ↦ (αᵣ x (c₁ ⊗ c₂) c₃).inv, naturality := ⋯ } ≫ (curriedAction C D).map (α_ c₁ c₂ c₃).hom =
    (α_ ((curriedAction C D).obj c₁) ((curriedAction C D).obj c₂) ((curriedAction C D).obj c₃)).hom ≫
      (curriedAction C D).obj c₁ ◁ { app := fun x ↦ (αᵣ x c₂ c₃).inv, naturality := ⋯ } ≫
        { app := fun x ↦ (αᵣ x c₁ (c₂ ⊗ c₃)).inv, naturality := ⋯ }

Tactic:
by

Goal state after:
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
inst✝ : MonoidalRightAction C D
x : C
⊢ (λ_ ((curriedAction C D).obj x)).inv =
    (curriedAction C D).map (λ_ x).inv ≫
      { app := fun x_1 ↦ (αᵣ x_1 (𝟙_ C) x).hom, naturality := ⋯ } ≫
        (actionUnitNatIso C D).hom ▷ (curriedAction C D).obj x

Tactic:
by

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) = (αᵣ z x y).hom ≫ (f ⊵ᵣ x) ⊵ᵣ y ≫ (αᵣ z' x y).inv

Tactic:
by

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
w x y : D
f : w ⟶ x
g : x ⟶ y
z : C
⊢ (f ≫ g) ⊵ᵣ z = f ⊵ᵣ z ≫ g ⊵ᵣ z

Tactic:
by

Goal state after:
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
inst✝ : MonoidalRightAction C D
x : C
⊢ (ρ_ ((curriedAction C D).obj x)).inv =
    (curriedAction C D).map (ρ_ x).inv ≫
      { app := fun x_1 ↦ (αᵣ x_1 x (𝟙_ C)).hom, naturality := ⋯ } ≫
        (curriedAction C D).obj x ◁ (actionUnitNatIso C D).hom

Tactic:
by

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
y : D
z x x' : C
f : x ⟶ x'
⊢ (y ⊙ᵣ z) ⊴ᵣ f = (αᵣ y z x).inv ≫ y ⊴ᵣ z ◁ f ≫ (αᵣ y z x').hom

Tactic:
by

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
w x : D
y z : C
f : w ⟶ x
g : y ⟶ z
⊢ w ⊴ᵣ g ≫ f ⊵ᵣ z = f ⊵ᵣ y ≫ x ⊴ᵣ g

Tactic:
by

Goal state after:
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
c₁ c₁' : D
c₂ c₂' c₃ c₃' : C
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
⊢ ((fun {d d'} f c ↦ (F.obj c).map f) f (c₂ ⊗ c₃) ≫
        (fun d x x_1 f ↦ (F.map f).app d) c₁' (c₂ ⊗ c₃) (c₂' ⊗ c₃') (g ⊗ₘ h)) ≫
      ((Functor.Monoidal.μIso F c₂' c₃').app c₁').symm.hom =
    ((Functor.Monoidal.μIso F c₂ c₃).app c₁).symm.hom ≫
      (fun {d d'} f c ↦ (F.obj c).map f)
          ((fun {d d'} f c ↦ (F.obj c).map f) f c₂ ≫ (fun d x x_1 f ↦ (F.map f).app d) c₁' c₂ c₂' g) c₃ ≫
        (fun d x x_1 f ↦ (F.map f).app d) ((F.obj c₂').obj c₁') c₃ c₃' h

Tactic:
by

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
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ ((f ⊙ᵣₘ g) ⊙ᵣₘ h) ≫ (αᵣ d₂ c₂ c₄).inv = (αᵣ d₁ c₁ c₃).inv ≫ (f ⊙ᵣₘ g ⊗ₘ h)

Tactic:
by

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
d d' : D
f : d ⟶ d'
⊢ (ρᵣ d).inv ≫ f ⊵ᵣ 𝟙_ C = f ≫ (ρᵣ d').inv

Tactic:
by

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
⊢ x ⊴ᵣ f.hom ≫ x ⊴ᵣ f.inv = 𝟙 (x ⊙ᵣ y)

Tactic:
by

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
z : C
⊢ f.hom ⊵ᵣ z ≫ f.inv ⊵ᵣ z = 𝟙 (x ⊙ᵣ z)

Tactic:
by

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
⊢ x ⊴ᵣ f.inv ≫ x ⊴ᵣ f.hom = 𝟙 (x ⊙ᵣ z)

Tactic:
by

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
z : C
⊢ f.inv ⊵ᵣ z ≫ f.hom ⊵ᵣ z = 𝟙 (y ⊙ᵣ z)

Tactic:
by

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)

Tactic:
by

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)

Tactic:
by

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 ⊴ᵣ inv f ≫ x ⊴ᵣ f = 𝟙 (x ⊙ᵣ z)

Tactic:
by

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
⊢ inv f ⊵ᵣ z ≫ f ⊵ᵣ z = 𝟙 (y ⊙ᵣ z)

Tactic:
by

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
c₁ c₂ c₃ : C
d : D
⊢ d ⊴ᵣ (α_ c₁ c₂ c₃).hom.mop ≫
      (αᵣ d { unmop := c₂ ⊗ c₃ } { unmop := c₁ }).hom ≫ (αᵣ d { unmop := c₃ } { unmop := c₂ }).hom ⊵ᵣ { unmop := c₁ } =
    (αᵣ d { unmop := c₃ } { unmop := c₁ ⊗ c₂ }).hom ≫ (αᵣ (d ⊙ᵣ { unmop := c₃ }) { unmop := c₂ } { unmop := c₁ }).hom

Tactic:
by

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

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
c₁ c₂ c₃ : Cᴹᵒᵖ
d : D
⊢ d ⊴ᵣ (α_ c₁ c₂ c₃).hom.unmop ≫ (αᵣ d (c₂ ⊗ c₃).unmop c₁.unmop).hom ≫ (αᵣ d c₃.unmop c₂.unmop).hom ⊵ᵣ c₁.unmop =
    (αᵣ d c₃.unmop (c₁ ⊗ c₂).unmop).hom ≫ (αᵣ (d ⊙ᵣ c₃.unmop) c₂.unmop c₁.unmop).hom

Tactic:
by

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

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

Tactic:
by

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'✝ : Cᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop c'✝ ⟶ unop c✝
g : unop d'✝ ⟶ unop d✝
⊢ (Quiver.Hom.unop (op f) ⊙ₗₘ Quiver.Hom.unop (op g)).op =
    (Quiver.Hom.unop (op f) ⊵ₗ unop d✝).op ≫ (unop c'✝ ⊴ₗ Quiver.Hom.unop (op g)).op

Tactic:
by

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
x' y' : C
f : x ⟶ y
g : x' ⟶ y'
inst✝¹ : IsIso f
inst✝ : IsIso g
⊢ (f ⊙ᵣₘ g) ≫ (inv f ⊙ᵣₘ inv g) = 𝟙 (x ⊙ᵣ x')

Tactic:
by

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✝ : C
f : X✝ ⟶ Y✝
x✝² x✝¹ : D
x✝ : x✝² ⟶ x✝¹
⊢ { obj := fun y ↦ y ⊙ᵣ X✝, map := fun {X Y} f ↦ f ⊵ᵣ X✝, map_id := ⋯, map_comp := ⋯ }.map x✝ ≫ x✝¹ ⊴ᵣ f =
    x✝² ⊴ᵣ f ≫ { obj := fun y ↦ y ⊙ᵣ Y✝, map := fun {X Y} f ↦ f ⊵ᵣ Y✝, map_id := ⋯, map_comp := ⋯ }.map x✝

Tactic:
by

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₂✝ c₃✝ c₄✝ : Cᵒᵖ
d₁✝ d₂✝ : Dᵒᵖ
f : unop c₂✝ ⟶ unop c₁✝
g : unop c₄✝ ⟶ unop c₃✝
h : unop d₂✝ ⟶ unop d₁✝
⊢ ((op f ⊗ₘ op g).unop ⊙ₗₘ Quiver.Hom.unop (op h)).op ≫ (αₗ (unop c₂✝) (unop c₄✝) (unop d₂✝)).symm.op.hom =
    (αₗ (unop c₁✝) (unop c₃✝) (unop d₁✝)).symm.op.hom ≫
      (Quiver.Hom.unop (op f) ⊙ₗₘ (Quiver.Hom.unop (op g) ⊙ₗₘ Quiver.Hom.unop (op h)).op.unop).op

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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ᵒᵖ
⊢ ((α_ 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 (x✝³ ⊗ x✝²)) (unop x✝¹) (unop x✝)).symm.op.hom ≫
      (αₗ (unop x✝³) (unop x✝²) (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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'✝ : C
d✝ d'✝ : D
f : c✝ ⟶ c'✝
g : d✝ ⟶ d'✝
⊢ (f.op ⊙ₗₘ g.op).unop = (f.op ⊵ₗ op d✝).unop ≫ (op c'✝ ⊴ₗ g.op).unop

Tactic:
by

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₂✝ c₃✝ c₄✝ : C
d₁✝ d₂✝ : D
f : c₁✝ ⟶ c₂✝
g : c₃✝ ⟶ c₄✝
h : d₁✝ ⟶ d₂✝
⊢ ((f ⊗ₘ g).op ⊙ₗₘ h.op).unop ≫ (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).symm.unop.hom =
    (αₗ (op c₁✝) (op c₃✝) (op d₁✝)).symm.unop.hom ≫ (f.op ⊙ₗₘ (g.op ⊙ₗₘ h.op).unop.op).unop

Tactic:
by

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 (𝟙_ C) ⊴ₗ x✝.op).unop ≫ (λₗ (op d'✝)).symm.unop.hom

Tactic:
by

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

Tactic:
by

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
⊢ ((α_ 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 (x✝³ ⊗ x✝²)) (op x✝¹) (op x✝)).symm.unop.hom ≫
      (αₗ (op x✝³) (op x✝²) (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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₂ c₃ : C
d : D
⊢ (α_ c₁ c₂ c₃).hom.mop ⊵ₗ d ≫
      (αₗ { unmop := c₂ ⊗ c₃ } { unmop := c₁ } d).hom ≫
        (αₗ { unmop := c₃ } { unmop := c₂ } ({ unmop := c₁ } ⊙ₗ d)).hom =
    (αₗ { unmop := c₃ } { unmop := c₁ ⊗ c₂ } d).hom ≫ { unmop := c₃ } ⊴ₗ (αₗ { unmop := c₂ } { unmop := c₁ } d).hom

Tactic:
by

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₂ c₃ : Cᴹᵒᵖ
d : D
⊢ (α_ c₁ c₂ c₃).hom.unmop ⊵ₗ d ≫ (αₗ (c₂ ⊗ c₃).unmop c₁.unmop d).hom ≫ (αₗ c₃.unmop c₂.unmop (c₁.unmop ⊙ₗ d)).hom =
    (αₗ c₃.unmop (c₁ ⊗ c₂).unmop d).hom ≫ c₃.unmop ⊴ₗ (αₗ c₂.unmop c₁.unmop d).hom

Tactic:
by

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
c✝ c'✝ : Cᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop d'✝ ⟶ unop d✝
g : unop c'✝ ⟶ unop c✝
⊢ (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op =
    (Quiver.Hom.unop (op f) ⊵ᵣ unop c✝).op ≫ (unop d'✝ ⊴ᵣ Quiver.Hom.unop (op g)).op

Tactic:
by

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ᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : Cᵒᵖ
f : unop d₂✝ ⟶ unop d₁✝
g : unop c₂✝ ⟶ unop c₁✝
h : unop c₄✝ ⟶ unop c₃✝
⊢ (Quiver.Hom.unop (op f) ⊙ᵣₘ (op g ⊗ₘ op h).unop).op ≫ (αᵣ (unop d₂✝) (unop c₂✝) (unop c₄✝)).symm.op.hom =
    (αᵣ (unop d₁✝) (unop c₁✝) (unop c₃✝)).symm.op.hom ≫
      ((Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op.unop ⊙ᵣₘ Quiver.Hom.unop (op h)).op

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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ᵒᵖ
⊢ (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 x✝) (unop (x✝³ ⊗ x✝²)) (unop x✝¹)).symm.op.hom ≫
      ((αᵣ (unop x✝) (unop x✝³) (unop x✝²)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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ᵒᵖ
c✝ c'✝ : C
d✝ d'✝ : D
f : d✝ ⟶ d'✝
g : c✝ ⟶ c'✝
⊢ (f.op ⊙ᵣₘ g.op).unop = (f.op ⊵ᵣ op c✝).unop ≫ (op d'✝ ⊴ᵣ g.op).unop

Tactic:
by

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₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Arrow.Hom.right ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = Arrow.Hom.right (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
by

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
c₁✝ c₂✝ c₃✝ c₄✝ : C
f : d₁✝ ⟶ d₂✝
g : c₁✝ ⟶ c₂✝
h : c₃✝ ⟶ c₄✝
⊢ (f.op ⊙ᵣₘ (g ⊗ₘ h).op).unop ≫ (αᵣ (op d₂✝) (op c₂✝) (op c₄✝)).symm.unop.hom =
    (αᵣ (op d₁✝) (op c₁✝) (op c₃✝)).symm.unop.hom ≫ ((f.op ⊙ᵣₘ g.op).unop.op ⊙ᵣₘ h.op).unop

Tactic:
by

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✝ = (x✝.op ⊵ᵣ op (𝟙_ C)).unop ≫ (ρᵣ (op d'✝)).symm.unop.hom

Tactic:
by

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₁ 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

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

Tactic:
by

Goal state after: