mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ (ObjectProperty.op fun f ↦ Coequifibered f.hom).IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
← isClosedUnderLimitsOfShape_inverseImage_iff _ _ e

Goal state after:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ ((ObjectProperty.op fun f ↦ Coequifibered f.hom).inverseImage e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case α_hom_inv
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 g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((α_hom X✝ Y✝ Z✝).comp (α_inv X✝ Y✝ Z✝)) = projectMapAux f✝ (Hom.id ((X✝.tensor Y✝).tensor Z✝))

Tactic:
dsimp only [projectMapAux]; rw [Iso.hom_inv_id]

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

Goal state before:
pp: case ρ_hom_inv
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 g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((ρ_hom X✝).comp (ρ_inv X✝)) = projectMapAux f✝ (Hom.id (X✝.tensor unit))

Tactic:
dsimp only [projectMapAux]; rw [Iso.hom_inv_id]

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

Goal state before:
pp: case l_hom_inv
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 g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((l_hom X✝).comp (l_inv X✝)) = projectMapAux f✝ (Hom.id (unit.tensor X✝))

Tactic:
dsimp only [projectMapAux]; rw [Iso.hom_inv_id]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ curry ((β_ I A).hom ≫ Hom.left u) ≫ (ihom I).map X.hom = toUnit A ≫ curryRightUnitorHom I

Tactic:
curry_natural_right,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ (curry (β_ I A).hom ≫ (ihom I).map (Hom.left u)) ≫ (ihom I).map X.hom = toUnit A ≫ curryRightUnitorHom I
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X A A' : C
f : A ⟶ A'
⊢ (toOver X).map f = Over.homMk (f ▷ X) ⋯

Tactic:
by
  simp [toOver]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝ : Type u
⊢ (ofTypeFunctor m).map ({ app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝ =
    { app := fun X ↦ ↾joinM, naturality := ⋯ }.app ((ofTypeFunctor m).obj x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝

Tactic:
by ext; exact joinM_map_joinM _

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasCoequalizerOfIsSplitPair G
inst✝ : PreservesColimitOfIsSplitPair G
⊢ MonadicRightAdjoint G

Tactic:
have : ReflectsColimitOfIsSplitPair G := ⟨fun f g _ => by
    have := HasCoequalizerOfIsSplitPair.out G f g
    apply reflectsColimit_of_reflectsIsomorphisms⟩
  apply monadicOfHasPreservesReflectsGSplitCoequalizers adj

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✝ : MonoidalLeftAction C D
d d' : D
f : d ⟶ d'
⊢ (λₗ d).inv ≫ 𝟙_ C ⊴ₗ f = f ≫ (λₗ d').inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]

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

Tactic:
by
  rw [← comp_actionHomLeft, IsIso.hom_inv_id, id_actionHomLeft]

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:
rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]

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
  rw [← comp_actionHomLeft, IsIso.hom_inv_id, id_actionHomLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Grp C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ M.X
⊢ (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.obj M).map g)) (shrinkYonedaGrpObjObjEquiv.symm f) =
    shrinkYonedaGrpObjObjEquiv.symm (g.unop ≫ f)

Tactic:
simp [shrinkYonedaGrp, shrinkYonedaGrpObjObjEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M M' : Grp C
Y : Cᵒᵖ
f : unop Y ⟶ M.X
g : M ⟶ M'
⊢ (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.map g).app Y)) (shrinkYonedaGrpObjObjEquiv.symm f) =
    shrinkYonedaGrpObjObjEquiv.symm (f ≫ g.hom.hom)

Tactic:
simp [shrinkYonedaGrp, shrinkYonedaGrpObjObjEquiv]

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

Goal state before:
pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (P.X ⊗ Q.X) ◁ η

Tactic:
π_tensor_id_actRight

Goal state after:
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (P.X ⊗ Q.X) ◁ η
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : CartesianMonoidalCategory C
G H K : C
inst✝⁶ : GrpObj G
inst✝⁵ : GrpObj H
inst✝⁴ : GrpObj K
φ : H ⟶ G
inst✝³ : BraidedCategory C
inst✝² : IsCommMonObj G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
⊢ Normal φ

Tactic:
simp [isNormalHom_iff, conj_eq_snd_of_isCommMonObj]

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)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d : D
⊢ (∀ (b : D) (a : C), IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj a))).app (Opposite.op b))) ↔
    ∀ (d' : D) (c : C), IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

Tactic:
apply forall₂_congr

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d : D
⊢ ∀ (a : D) (b : C),
    IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj b))).app (Opposite.op a)) ↔
      IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ a)).op).app b)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (P.X ⊗ Q.X) ◁ μ

Tactic:
π_tensor_id_actRight

Goal state after:
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (P.X ⊗ Q.X) ◁ μ
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (α_ (P.X ⊗ Q.X) T.X T.X).inv

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (α_ P.X Q.X T.X).hom ▷ T.X

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (P.X ◁ Q.actRight) ▷ T.X

Tactic:
π_tensor_id_actRight

Goal state after:
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (α_ (P.X ⊗ Q.X) T.X T.X).inv

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (α_ P.X Q.X T.X).hom ▷ T.X

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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₁} (tensorRight X)
| (P.X ◁ Q.actRight) ▷ T.X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X P.X Q.X).inv ▷ T.X

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actLeft ▷ Q.X ▷ T.X

Tactic:
π_tensor_id_actRight

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X P.X Q.X).inv ▷ T.X

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actLeft ▷ Q.X ▷ T.X
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 * c + b * c
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ

Tactic:
replace h := h (fst (R ⊗ R) R ≫ fst _ _) (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 ≫ fst R R + fst (R ⊗ R) R ≫ snd R R) * snd (R ⊗ R) R =
    fst (R ⊗ R) R ≫ fst R R * snd (R ⊗ R) R + fst (R ⊗ R) R ≫ snd R R * snd (R ⊗ R) R
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_fst
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map ((reflector i).map (fst A B))

Tactic:
apply (reflectorAdjunction i).unit.naturality

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_snd
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map ((reflector i).map (snd A B))

Tactic:
apply (reflectorAdjunction i).unit.naturality

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            (((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ?hB)
                    (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f)))) ≫
              i.map g))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

pp: case hB
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.essImage (B ⟹ i.obj X)

Tactic:
curry_natural_right,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ?hB)
                    (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f)))) ≫
            (ihom (i.obj ((reflector i).obj A))).map (i.map g))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

case hB
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.essImage (B ⟹ i.obj X)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk
C : Type u
X Y : F C
f' : X ⟶ᵐ Y
⊢ (fun n ↦ X.normalizeObj n) = Y.normalizeObj

Tactic:
induction f' with
  | comp _ _ _ _ => apply Eq.trans <;> assumption
  | whiskerLeft _ _ ih => funext; apply congr_fun ih
  | whiskerRight _ _ ih => funext; apply congr_arg₂ _ rfl (congr_fun ih _)
  | @tensor W X Y Z _ _ ih₁ ih₂ =>
      funext n
      simp [congr_fun ih₁ n, congr_fun ih₂ (normalizeObj Y n)]
  | _ => funext; rfl

Goal state after: