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

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
        LaxMonoidal.μ L' X (Y ⊗ Z) ≫
          L'.map (α_ X Y Z).inv ≫ OplaxMonoidal.δ L' (X ⊗ Y) Z ≫ OplaxMonoidal.δ L' X Y ▷ L'.obj Z) ≫
      ((braidingNatIso L W ε).hom.app (L'.obj X ⊗ L'.obj Y)).app (L'.obj Z) ≫
        L'.obj Z ◁ LaxMonoidal.μ L' X Y ≫
          LaxMonoidal.μ L' Z (X ⊗ Y) ≫
            L'.map (α_ Z X Y).inv ≫ OplaxMonoidal.δ L' (Z ⊗ X) Y ≫ OplaxMonoidal.δ L' Z X ▷ L'.obj Y =
    ((((L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
              L'.obj X ◁ L'.map (β_ Y Z).hom ≫
                L'.obj X ◁ OplaxMonoidal.δ L' Z Y ≫ L'.obj X ◁ LaxMonoidal.μ L' Z Y ≫ LaxMonoidal.μ L' X (Z ⊗ Y)) ≫
            L'.map (α_ X Z Y).inv) ≫
          OplaxMonoidal.δ L' (X ⊗ Z) Y) ≫
        OplaxMonoidal.δ L' X Z ▷ L'.obj Y) ≫
      ((LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom) ≫ OplaxMonoidal.δ L' Z X) ▷ L'.obj Y

Tactic:
slice_lhs 6 7 =>
    rw [braidingNatIso_hom_app_naturality_μ_right, braidingNatIso_hom_app]

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
      LaxMonoidal.μ L' X (Y ⊗ Z) ≫
        L'.map (α_ X Y Z).inv ≫
          OplaxMonoidal.δ L' (X ⊗ Y) Z ≫
            OplaxMonoidal.δ L' X Y ▷ L'.obj Z ≫
              ((((LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫
                        LaxMonoidal.μ L' (X ⊗ Y) Z ≫ L'.map (β_ (X ⊗ Y) Z).hom ≫ OplaxMonoidal.δ L' Z (X ⊗ Y)) ≫
                      LaxMonoidal.μ L' Z (X ⊗ Y)) ≫
                    L'.map (α_ Z X Y).inv) ≫
                  OplaxMonoidal.δ L' (Z ⊗ X) Y) ≫
                OplaxMonoidal.δ L' Z X ▷ L'.obj Y =
    ((((L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
              L'.obj X ◁ L'.map (β_ Y Z).hom ≫
                L'.obj X ◁ OplaxMonoidal.δ L' Z Y ≫ L'.obj X ◁ LaxMonoidal.μ L' Z Y ≫ LaxMonoidal.μ L' X (Z ⊗ Y)) ≫
            L'.map (α_ X Z Y).inv) ≫
          OplaxMonoidal.δ L' (X ⊗ Z) Y) ≫
        OplaxMonoidal.δ L' X Z ▷ L'.obj Y) ≫
      ((LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom) ≫ OplaxMonoidal.δ L' Z X) ▷ L'.obj Y
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simpa using! map_hexagon_forward _ _ _

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
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
comm : toUnit A ≫ curry (ρ_ I).hom = v₂ ≫ (ihom I).map X.hom
w' : I ◁ toUnit A ≫ (ρ_ I).hom = ((ihom.adjunction I).homEquiv A X.left).symm v₂ ≫ X.hom
⊢ (β_ A I).hom ≫ SemiCartesianMonoidalCategory.fst I A = SemiCartesianMonoidalCategory.snd A I

Tactic:
braiding_hom_fst

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
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
comm : toUnit A ≫ curry (ρ_ I).hom = v₂ ≫ (ihom I).map X.hom
w' : I ◁ toUnit A ≫ (ρ_ I).hom = ((ihom.adjunction I).homEquiv A X.left).symm v₂ ≫ X.hom
⊢ SemiCartesianMonoidalCategory.snd A I = SemiCartesianMonoidalCategory.snd A I
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun x ↦ joinM (⇑(TypeCat.Hom.hom g.of) <$> (ConcreteCategory.hom f.of) x)) =
    (fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x

Tactic:
ext t

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : X✝.of
⊢ joinM (⇑(TypeCat.Hom.hom g.of) <$> (ConcreteCategory.hom f.of) t) =
    ((fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x) t
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { of := (f ≫ g) ≫ T.η.app Z } =
    { of := { of := f ≫ T.η.app Y }.of ≫ T.map { of := g ≫ T.η.app Z }.of ≫ T.μ.app { of := Z }.of }

Tactic:
simp [← T.η.naturality g]

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
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj A.A)

Tactic:
rw [adj.left_triangle_components]

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✝ : MonoidalLeftAction C D
x : C
⊢ (λ_ ((curriedActionMop C D).obj x)).inv.unmop =
    ((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

Tactic:
ext t

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
⊢ (λ_ ((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
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
⊢ (ρ_ ((curriedActionMop C D).obj x)).inv.unmop =
    ((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

Tactic:
ext t

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
⊢ (ρ_ ((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
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:
ext t

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
⊢ (λ_ ((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
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:
ext t

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
⊢ (ρ_ ((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
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetraction adj c d = 𝟙 ((𝟭 D).obj ((ihom d).obj (R.obj c)))

Tactic:
suffices (_ ◁ adj.unit.app _) ≫ adjRetractionAux adj c d = (ihom.ev _).app _ by
    simp only [id_obj, adjRetraction, ← curry_natural_left, this]
    simp [curry_eq]

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
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetractionAux adj c d = (ihom.ev d).app (R.obj c)
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) =
    (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
suffices ((α_ _ _ _).hom ≫ _ ◁ _ ◁ f₃.right ≫ (α_ _ _ _).inv ≫ f₁.left ▷ _ ▷ _ ≫
      (α_ _ _ _).hom ≫ _ ◁ f₂.right ▷ _ = f₁.left ▷ _ ▷ _ ≫ (α_ _ _ _).hom ≫
      _ ◁ f₂.right ▷ _ ≫ _ ◁ _ ◁ f₃.right) by
      simp [← whisker_exchange_assoc, reassoc_of% this]
    cat_disch

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

Goal state before:
pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ (tensorRight Y.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((α_ X (𝟙_ (Arrow C)) Y).hom ≫ X ◁ (λ_ Y).hom) =
    (tensorRight Y.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((ρ_ X).hom ▷ Y)

Tactic:
simp [← comp_whiskerRight_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry ((F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ F₃.map (Under.Hom.right φ)) =
    curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right) ≫ (pre (F₁.map (Under.Hom.right φ))).app (F₃.obj k₂.right)

Tactic:
curry_pre_app,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry ((F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ F₃.map (Under.Hom.right φ)) =
    curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right)
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        F₁.map (Under.Hom.right φ) ▷ F₂.obj k₁.right ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right) =
    curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map (k₁.hom ≫ Under.Hom.right φ) ≫ f.app k₂.right)

Tactic:
Functor.map_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        F₁.map (Under.Hom.right φ) ▷ F₂.obj k₁.right ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right) =
    curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫
        F₁.obj k₂.right ◁ (F₂.map k₁.hom ≫ F₂.map (Under.Hom.right φ)) ≫ f.app k₂.right)
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✝² : MonoidalClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
X : D
⊢ (i ⋙ ihom A).obj X ≅ (i ⋙ ihom A ⋙ reflector i ⋙ i).obj X

Tactic:
haveI := Functor.essImage.unit_isIso (ExponentialIdeal.exp_closed (i.obj_mem_essImage X) A)

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✝² : MonoidalClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
X : D
this : IsIso ((reflectorAdjunction i).unit.app (A ⟹ i.obj X))
⊢ (i ⋙ ihom A).obj X ≅ (i ⋙ ihom A ⋙ reflector i ⋙ i).obj X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
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.tensorBimod N₁).actRight ≫
      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) ⋯ ⋯) =
    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) ⋯ ⋯) ▷
        Z.X ≫
      (M.tensorBimod N₂).actRight

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
    dsimp
    slice_lhs 1 2 => rw [TensorBimod.π_tensor_id_actRight]
    slice_lhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
    slice_lhs 2 3 => rw [← whiskerLeft_comp, Hom.right_act_hom]
    slice_rhs 1 2 =>
      rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one, comp_whiskerRight]
    slice_rhs 2 3 => rw [TensorBimod.π_tensor_id_actRight]
    simp

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✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ i.essImage (A ⟹ i.obj B)

Tactic:
have : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B) := by
    dsimp
    rw [← curry_natural_left, curry_eq_iff, uncurry_id_eq_ev, ← ir.homEquiv_naturality_left,
      ir.homEquiv_apply_eq, Category.assoc, Category.assoc,
      prodComparison_natural_whiskerLeft_assoc, ← whiskerLeft_comp_assoc,
      ir.left_triangle_components, whiskerLeft_id, Category.id_comp]
    apply IsIso.hom_inv_id_assoc

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✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
this : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
⊢ i.essImage (A ⟹ i.obj B)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : MonoidalCategory V
inst✝² : BraidedCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
⊢ (corepresentableBy G F).homEquiv.symm (braidingInvCorepresenting F G) ≫
      (corepresentableBy F G).homEquiv.symm (braidingHomCorepresenting F G) =
    𝟙 (G ⊛ F)

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension (G ⊛ F) (unit G F)
    ext
    simp [-tensor_obj]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ihom (F.obj j')).map (f.app (j' ⊗ c)) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
⊢ ℌ.π c j ≫ (ihom (F.obj j)).map (G.map (φ ▷ c) ≫ f.app (j' ⊗ c)) =
    (ℌ.π c j' ≫ (ihom (F.obj j')).map (f.app (j' ⊗ c))) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))

Tactic:
Functor.map_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ihom (F.obj j')).map (f.app (j' ⊗ c)) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
⊢ ℌ.π c j ≫ (ihom (F.obj j)).map (G.map (φ ▷ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ℌ.π c j' ≫ (ihom (F.obj j')).map (f.app (j' ⊗ c))) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ Δ ≫ 𝒮 ▷ A ≫ μ
⊢ η ≫ 𝒮 = η

Tactic:
conv at this =>
    rhs
    rw [antipode_left]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ hom P Q L ≫ inv P Q L = 𝟙 ((P.tensorBimod Q).tensorBimod L).X

Tactic:
by
  dsimp [hom, homAux, inv, invAux]
  apply coequalizer.hom_ext
  slice_lhs 1 2 => rw [coequalizer.π_desc]
  refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
  simp only [Functor.flip_obj_map, curriedTensor_map_app]
  slice_lhs 1 3 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
  slice_lhs 3 4 => rw [coequalizer.π_desc]
  slice_lhs 2 4 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
  slice_lhs 1 3 => rw [Iso.hom_inv_id_assoc]
  dsimp only [TensorBimod.X]
  slice_rhs 2 3 => rw [Category.comp_id]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 X ⊗≫ X ◁ η_ X Y ⊗≫ (X ◁ (β_ Y X).inv ⊗≫ (β_ X Y).hom ▷ X) ⊗≫ ε_ X Y ▷ X ⊗≫ 𝟙 X =
    𝟙 X ⊗≫
      X ◁ η_ X Y ⊗≫
        (𝟙 (X ⊗ X ⊗ Y) ⊗≫
            (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)) ⊗≫
          ε_ X Y ▷ X ⊗≫ 𝟙 X

Tactic:
congr 3

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ X ◁ (β_ Y X).inv ⊗≫ (β_ X Y).hom ▷ X =
    𝟙 (X ⊗ X ⊗ Y) ⊗≫ (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)