mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapᵣ F =
    LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapᵣ F

Tactic:
· refine natTrans_ext L W (fun X₁ ↦ ?_)
    have := ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).naturality (εIso L).inv
    dsimp [e] at this ⊢
    monoidal_simps
    simp [reassoc_of% this, curriedTensorPreIsoPost_hom_app_app, tensorHom_def,
      whisker_exchange_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, ← map_comp]

Goal state after:
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₈
Z : Type u₉
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
V : Y ⥤ Z
⊢ (CatCommSq.iso ((precompose F G).obj (U ⋙ V)) ((transform Z).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj (U ⋙ V))).hom ≫
      ((transform Z).obj ψ).whiskerLeft (precomposeObjComp F₁ G₁ U V).hom =
    whiskerRight (precomposeObjComp F G U V).hom ((transform X).obj ψ) ≫
      (((precompose F G).obj V).associator ((precompose F G).obj U) ((transform X).obj ψ)).hom ≫
        ((precompose F G).obj V).whiskerLeft
            (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ)
                ((precompose F₁ G₁).obj U)).hom ≫
          (((precompose F G).obj V).associator ((transform Y).obj ψ) ((precompose F₁ G₁).obj U)).inv ≫
            whiskerRight
                (CatCommSq.iso ((precompose F G).obj V) ((transform Z).obj ψ) ((transform Y).obj ψ)
                    ((precompose F₁ G₁).obj V)).hom
                ((precompose F₁ G₁).obj U) ≫
              (((transform Z).obj ψ).associator ((precompose F₁ G₁).obj V) ((precompose F₁ G₁).obj U)).hom

Tactic:
ext <;> simp

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

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

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

Goal state after:
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₁
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₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
⊢ (CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
          ((transform X).obj (ψ.comp ψ'))).hom ≫
      ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom =
    whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
      (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
        ((transform Y).obj ψ).whiskerLeft
            (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                ((transform X).obj ψ')).hom ≫
          (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
            whiskerRight
                (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                    ((transform X).obj ψ)).hom
                ((transform X).obj ψ') ≫
              (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).hom

Tactic:
ext <;> simp

Goal state after:
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 [-IsMonHom.one_hom] using congrArg (fun t ↦ t.app X) (IsMonHom.one_hom f.hom)

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 =
    ((αₗ (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:
apply IsIso.inv_eq_inv.mp

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

Tactic:
apply IsIso.inv_eq_inv.mp

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

Tactic:
apply IsIso.inv_eq_inv.mp

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ᵒᵖ
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
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 =
    ((αₗ (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:
apply IsIso.inv_eq_inv.mp

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

Tactic:
apply IsIso.inv_eq_inv.mp

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

Tactic:
apply IsIso.inv_eq_inv.mp

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
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
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 =
    ((αᵣ (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:
apply IsIso.inv_eq_inv.mp

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

Tactic:
apply IsIso.inv_eq_inv.mp

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

Tactic:
apply IsIso.inv_eq_inv.mp

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ᵒᵖ
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
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
⊢ ((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 =
    ((αᵣ (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:
apply IsIso.inv_eq_inv.mp

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

Tactic:
apply IsIso.inv_eq_inv.mp

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

Tactic:
apply IsIso.inv_eq_inv.mp

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
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
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c
⊢ R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ

Tactic:
replace h := h (fst R (R ⊗ R)) (snd _ _ ≫ fst _ _) (snd _ _ ≫ snd _ _)

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h :
  fst R (R ⊗ R) * (snd R (R ⊗ R) ≫ fst R R + snd R (R ⊗ R) ≫ snd R R) =
    fst R (R ⊗ R) * snd R (R ⊗ R) ≫ fst R R + fst R (R ⊗ R) * snd R (R ⊗ R) ≫ snd R R
⊢ R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫
    colimMap
      (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
        ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| (α_ X.X M.X N₁.X).inv

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| M.actLeft ▷ N₁.X

Tactic:
ι_colimMap,

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
          ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯).app
      WalkingParallelPair.one ≫
    colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| (α_ X.X M.X N₁.X).inv

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| M.actLeft ▷ N₁.X