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
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  autoParam
    (whiskerRight e₁.hom F ≫
        (K.associator (π₁ F G) F).hom ≫
          K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
      (J.associator (π₁ F G) F).hom ≫
        J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G)
    toCatCommSqOver_mapIso_mkNatIso_eq_mkIso._auto_1
⊢ whiskerRight e₁.hom F ≫ ((toCatCommSqOver F G X).obj K).iso.hom =
    ((toCatCommSqOver F G X).obj J).iso.hom ≫ whiskerRight e₂.hom G

Tactic:
simpa using

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₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  autoParam
    (whiskerRight e₁.hom F ≫
        (K.associator (π₁ F G) F).hom ≫
          K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
      (J.associator (π₁ F G) F).hom ≫
        J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G)
    toCatCommSqOver_mapIso_mkNatIso_eq_mkIso._auto_1
⊢ whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
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₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  autoParam
    (whiskerRight e₁.hom F ≫
        (K.associator (π₁ F G) F).hom ≫
          K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
      (J.associator (π₁ F G) F).hom ≫
        J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G)
    mkNatIso_eq._auto_1
⊢ whiskerRight e₁.hom F ≫ ((functorEquiv F G X).functor.obj K).iso.hom =
    ((functorEquiv F G X).functor.obj J).iso.hom ≫ whiskerRight e₂.hom G

Tactic:
simpa using

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₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  autoParam
    (whiskerRight e₁.hom F ≫
        (K.associator (π₁ F G) F).hom ≫
          K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
      (J.associator (π₁ F G) F).hom ≫
        J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G)
    mkNatIso_eq._auto_1
⊢ whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
Module: Mathlib.Tactic.CategoryTheory.Coherence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f ≫ 𝟙 Y = g
⊢ f = g

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f ≫ 𝟙 Y = g
⊢ f = g
Module: Mathlib.Tactic.CategoryTheory.Coherence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g ≫ 𝟙 Y
⊢ f = g

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g ≫ 𝟙 Y
⊢ f = g
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f).map ⟦a✝⟧ ▷ (project f).obj x✝ ≫ (Iso.refl ((project f).obj Y✝ ⊗ (project f).obj x✝)).hom =
    (Iso.refl ((project f).obj X✝ ⊗ (project f).obj x✝)).hom ≫ (project f).map (⟦a✝⟧ ▷ x✝)

pp: case h
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ b✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p✝ : a✝ ≈ b✝
⊢ ⋯ = ⋯

Tactic:
all_goals aesop

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

Goal state before:
pp: case f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f).obj x✝ ◁ (project f).map ⟦a✝⟧ ≫ (Iso.refl ((project f).obj x✝ ⊗ (project f).obj Y✝)).hom =
    (Iso.refl ((project f).obj x✝ ⊗ (project f).obj X✝)).hom ≫ (project f).map (x✝ ◁ ⟦a✝⟧)

pp: case h
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
a✝ b✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p✝ : a✝ ≈ b✝
⊢ ⋯ = ⋯

Tactic:
all_goals aesop

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

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

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenPullbacks C
X : C
Y : Over X
m : Y ⟶ Over.mk (𝟙 X)
⊢ Over.Hom.left m = Y.hom
Module: Mathlib.CategoryTheory.Monad.EquivMon

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : Mon (C ⥤ C)
f : X✝ ⟶ Y
X : C
⊢ η.app X ≫ f.hom.app X = η.app X
Module: Mathlib.CategoryTheory.Monad.EquivMon

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon (C ⥤ C)
f : X ⟶ Y
Z : C
⊢ μ.app Z ≫ f.hom.app Z = f.hom.app (X.X.obj Z) ≫ Y.X.map (f.hom.app Z) ≫ μ.app Z
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalRightAction C D
inst✝¹ : MonoidalRightAction C D'
inst✝ : F.OplaxRightLinear C
d : D
⊢ δᵣ F d (𝟙_ C) ≫ (ρᵣ (F.obj d)).hom = F.map (ρᵣ d).hom
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✝ : MonoidalLeftAction C D
c₁ c₂ c₃ : C
d : D
⊢ ((mopEquiv (D ⥤ D)).inverse.map
          (Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ c₂ x).inv, naturality := ⋯ } ▷ (curriedActionMop C D).obj c₃ ≫
            Quiver.Hom.mop { app := fun x ↦ (αₗ (c₁ ⊗ c₂) c₃ x).inv, naturality := ⋯ } ≫
              (curriedActionMop C D).map (α_ c₁ c₂ c₃).hom)).app
      d =
    ((mopEquiv (D ⥤ D)).inverse.map
          ((α_ ((curriedActionMop C D).obj c₁) ((curriedActionMop C D).obj c₂) ((curriedActionMop C D).obj c₃)).hom ≫
            (curriedActionMop C D).obj c₁ ◁ Quiver.Hom.mop { app := fun x ↦ (αₗ c₂ c₃ x).inv, naturality := ⋯ } ≫
              Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ (c₂ ⊗ c₃) x).inv, naturality := ⋯ })).app
      d

Tactic:
simpa using

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
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ : C
d : D
⊢ (αₗ c₁ c₂ (c₃ ⊙ₗ d)).inv ≫ (αₗ (c₁ ⊗ c₂) c₃ d).inv ≫ (α_ c₁ c₂ c₃).hom ⊵ₗ d =
    c₁ ⊴ₗ (αₗ c₂ c₃ d).inv ≫ (αₗ c₁ (c₂ ⊗ c₃) d).inv
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✝ : MonoidalLeftAction C D
x : C
t : D
⊢ (λ_ ((curriedActionMop C D).obj x)).inv.unmop.app t =
    ((curriedActionMop C D).map (λ_ x).inv ≫
            Quiver.Hom.mop { app := fun x_1 ↦ (αₗ (𝟙_ C) x x_1).hom, naturality := ⋯ } ≫
              (actionUnitNatIso C D).hom.mop ▷ (curriedActionMop C D).obj x).unmop.app
      t

Tactic:
simpa using

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
inst✝ : MonoidalLeftAction C D
x : C
t : D
⊢ 𝟙 (x ⊙ₗ t) = (λ_ x).inv ⊵ₗ t ≫ (αₗ (𝟙_ C) x t).hom ≫ (λₗ (x ⊙ₗ t)).hom
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✝ : MonoidalLeftAction C D
x : C
t : D
⊢ (ρ_ ((curriedActionMop C D).obj x)).inv.unmop.app t =
    ((curriedActionMop C D).map (ρ_ x).inv ≫
            Quiver.Hom.mop { app := fun x_1 ↦ (αₗ x (𝟙_ C) x_1).hom, naturality := ⋯ } ≫
              (curriedActionMop C D).obj x ◁ (actionUnitNatIso C D).hom.mop).unmop.app
      t

Tactic:
simpa using

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
inst✝ : MonoidalLeftAction C D
x : C
t : D
⊢ 𝟙 (x ⊙ₗ t) = (ρ_ x).inv ⊵ₗ t ≫ (αₗ x (𝟙_ C) t).hom ≫ x ⊴ₗ (λₗ t).hom
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✝ : MonoidalLeftAction C D
x y : C
f : x ≅ y
z : D
⊢ f.hom ⊵ₗ z ≫ f.inv ⊵ₗ z = 𝟙 (x ⊙ₗ z)

Tactic:
rw [← comp_actionHomLeft, Iso.hom_inv_id, id_actionHomLeft]

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
c₁ c₂ c₃ : C
d : D
⊢ ({ 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).app
      d =
    ((α_ ((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 := ⋯ }).app
      d

Tactic:
simpa using

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
inst✝ : MonoidalRightAction C D
c₁ c₂ c₃ : C
d : D
⊢ (αᵣ d c₁ c₂).inv ⊵ᵣ c₃ ≫ (αᵣ d (c₁ ⊗ c₂) c₃).inv ≫ d ⊴ᵣ (α_ c₁ c₂ c₃).hom =
    (αᵣ (d ⊙ᵣ c₁) c₂ c₃).inv ≫ (αᵣ d c₁ (c₂ ⊗ c₃)).inv
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
t : D
⊢ (λ_ ((curriedAction C D).obj x)).inv.app t =
    ((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).app
      t

Tactic:
simpa using

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
inst✝ : MonoidalRightAction C D
x : C
t : D
⊢ 𝟙 (t ⊙ᵣ x) = t ⊴ᵣ (λ_ x).inv ≫ (αᵣ t (𝟙_ C) x).hom ≫ (ρᵣ t).hom ⊵ᵣ x
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
t : D
⊢ (ρ_ ((curriedAction C D).obj x)).inv.app t =
    ((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).app
      t

Tactic:
simpa using

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
inst✝ : MonoidalRightAction C D
x : C
t : D
⊢ 𝟙 (t ⊙ᵣ x) = t ⊴ᵣ (ρ_ x).inv ≫ (αᵣ t x (𝟙_ C)).hom ≫ (ρᵣ (t ⊙ᵣ x)).hom
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:
rw [← comp_actionHomLeft, Iso.hom_inv_id, id_actionHomLeft]

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:
simpa using

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
inst✝ : MonoidalRightAction Cᴹᵒᵖ D
c₁ c₂ c₃ : C
d : D
⊢ d ⊴ᵣ (α_ { unmop := c₃ } { unmop := c₂ } { unmop := c₁ }).inv ≫
      (αᵣ d ({ unmop := c₃ } ⊗ { unmop := c₂ }) { unmop := c₁ }).hom ≫
        (αᵣ d { unmop := c₃ } { unmop := c₂ }).hom ⊵ᵣ { unmop := c₁ } =
    (αᵣ d { unmop := c₃ } ({ unmop := c₂ } ⊗ { unmop := c₁ })).hom ≫
      (αᵣ (d ⊙ᵣ { unmop := c₃ }) { unmop := c₂ } { unmop := c₁ }).hom
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.unop =
    ((Quiver.Hom.unop (op f) ⊵ₗ unop d✝).op ≫ (unop c'✝ ⊴ₗ Quiver.Hom.unop (op g)).op).unop

Tactic:
simpa using

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

Tactic:
simpa using

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
c✝ c'✝ : C
d✝ d'✝ : D
f : c✝ ⟶ c'✝
g : d✝ ⟶ d'✝
⊢ f.op ⊙ₗₘ g.op = f.op ⊵ₗ op d'✝ ≫ op c✝ ⊴ₗ g.op
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:
simpa using

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