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

Goal state before:
pp: case refine_1
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
X₁ X₂ X₃ : C
⊢ (((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂)) ▷
        F.obj (L.obj X₃) ≫
      ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁ ⊗ L.obj X₂)).app (L.obj X₃) ≫
        F.map (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)).hom =
    (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))).hom ≫
      F.obj (L.obj X₁) ◁ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₂)).app (L.obj X₃) ≫
        ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂ ⊗ L.obj X₃)

Tactic:
curriedTensorPreIsoPost_hom_app_app,

Goal state after:
case refine_1
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
X₁ X₂ X₃ : C
⊢ (((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂)) ▷
        F.obj (L.obj X₃) ≫
      ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁ ⊗ L.obj X₂)).app (L.obj X₃) ≫
        F.map (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)).hom =
    (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))).hom ≫
      F.obj (L.obj X₁) ◁
          (((Lifting.iso L W G F).hom.app X₂ ⊗ₘ (Lifting.iso L W G F).hom.app X₃) ≫
            μ G X₂ X₃ ≫ (Lifting.iso L W G F).inv.app (X₂ ⊗ X₃) ≫ F.map (δ L X₂ X₃)) ≫
        ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂ ⊗ L.obj X₃)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ ((forgetAdjToOver X).homEquiv Z A).symm f = Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X

Tactic:
Adjunction.homEquiv_counit,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ (Over.forget X).map f ≫ (forgetAdjToOver X).counit.app A = Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
refine Arrow.hom_ext _ _ ?_ (by simp [whisker_exchange_assoc])

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
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)
| R.X ◁ (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q)

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)
| actLeft 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)
| (α_ R.X R.X (P.X ⊗ Q.X)).hom

Tactic:
whiskerLeft_π_actLeft,

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)
| R.X ◁
    ((α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))

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)
| actLeft P Q

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)
| (α_ R.X R.X (P.X ⊗ Q.X)).hom
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'))
| ∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c))

Tactic:
intro c d

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

Tactic:
have w₁ : ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c) =
        (adj.homEquiv _ _).symm ∘
          (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) ∘
            (adj.homEquiv _ _) := by ext; simp

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' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d')) ↔
    IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)
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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
d d' : D
this :
  δ L ((𝟭 D).obj d) ((𝟭 D).obj d') ≫
      (L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d') =
    L.map (adj.unit.app d ⊗ₘ adj.unit.app d')
⊢ IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
← this

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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
d d' : D
this :
  δ L ((𝟭 D).obj d) ((𝟭 D).obj d') ≫
      (L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d') =
    L.map (adj.unit.app d ⊗ₘ adj.unit.app d')
⊢ IsIso
    (δ L ((𝟭 D).obj d) ((𝟭 D).obj d') ≫
      (L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d'))
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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
⊢ ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))

Tactic:
rw [((isIso_tfae adj).out 0 3 :)]

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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
⊢ ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q) ▷ T.X

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)
| actRight P Q

Tactic:
whiskerLeft_π_actLeft,

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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| ((α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ▷
    T.X

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)
| actRight P Q
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X : C
a b c : X ⟶ R
⊢ (a + b) * c = a * c + b * c

Tactic:
revert X a b c
  rw [← add_mul_iff, RingObj.add_mul R]

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₃ : J ⥤ C
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
⊢ homEquiv.symm (f₂ ≫ g) = F₁ ◁ f₂ ≫ homEquiv.symm g

Tactic:
by
  dsimp [homEquiv]
  ext j
  simp [← uncurry_natural_left]

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
X : MonoOver (⊤_ C)
Z : C
f g : Z ⟶ X.obj.left
⊢ f = g

Tactic:
by
          rw [← cancel_mono X.arrow]
          subsingleton

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

Goal state before:
pp: case h
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
X Y : D
this : HasFiniteProducts D
⊢ i.obj (X ⨯ Y) ≅ i.obj X ⊗ i.obj Y

Tactic:
apply Limits.PreservesLimitPair.iso i _ _ |>.trans

Goal state after:
case h
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
X Y : D
this : HasFiniteProducts D
⊢ i.obj X ⨯ i.obj Y ≅ i.obj X ⊗ i.obj Y
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
x✝ : C × C
⊢ (unit F G ≫
          (tensor C).whiskerLeft
            ((corepresentableBy F G).homEquiv.symm (braidingHomCorepresenting F G) ≫
              (corepresentableBy G F).homEquiv.symm (braidingInvCorepresenting F G))).app
      x✝ =
    (unit F G ≫ (tensor C).whiskerLeft (𝟙 (F ⊛ G))).app x✝

Tactic:
simp [-tensor_obj]

Goal state after:
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
x✝ : C × C
⊢ (unit G F ≫
          (tensor C).whiskerLeft
            ((corepresentableBy G F).homEquiv.symm (braidingInvCorepresenting F G) ≫
              (corepresentableBy F G).homEquiv.symm (braidingHomCorepresenting F G))).app
      x✝ =
    (unit G F ≫ (tensor C).whiskerLeft (𝟙 (G ⊛ F))).app x✝

Tactic:
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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  MonoidalClosed.curry (F.map f ▷ G.obj c) ≫ (ihom (F.obj c')).map ((DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫ (ihom (F.obj c')).map ((F ⊛ G).map (f ▷ c))
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫ (ihom (F.obj c')).map ((F ⊛ G).map (f ▷ c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      (MonoidalClosed.pre (F.map f)).app ((F ⊛ G).obj (c'' ⊗ c))

Tactic:
← this

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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  MonoidalClosed.curry (F.map f ▷ G.obj c) ≫ (ihom (F.obj c')).map ((DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫ (ihom (F.obj c')).map ((F ⊛ G).map (f ▷ c))
⊢ MonoidalClosed.curry (F.map f ▷ G.obj c) ≫ (ihom (F.obj c')).map ((DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      (MonoidalClosed.pre (F.map f)).app ((F ⊛ G).obj (c'' ⊗ c))
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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
this :
  MonoidalClosed.curry (F.obj j ◁ G.map f) ≫ (ihom (F.obj j)).map ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
⊢ G.map f ≫ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))

Tactic:
← this

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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
this :
  MonoidalClosed.curry (F.obj j ◁ G.map f) ≫ (ihom (F.obj j)).map ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
⊢ G.map f ≫ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry (F.obj j ◁ G.map f) ≫ (ihom (F.obj j)).map ((DayConvolution.unit F G).app (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).inv ≫ 𝒮 ▷ 𝟙_ C ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
simpa

Goal state after:
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
⊢ η ≫ 𝒮 = η

Tactic:
have := (rfl : η[A] ≫ Δ[A] ≫ (𝒮[A] ▷ A) ≫ μ[A] = _)
  conv at this =>
    rhs
    rw [antipode_left]
  rw [Bimon.one_comul_assoc, tensorHom_def_assoc, unitors_inv_equal,
    ← rightUnitor_inv_naturality_assoc, whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc,
    rightUnitor_inv_naturality_assoc] at this
  simpa

Goal state after:
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
⊢ Δ ≫
      Δ ▷ A ≫
        (α_ A A A).hom ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ (β_ A A).hom ≫
              A ◁ A ◁ A ◁ 𝒮 ≫
                A ◁ (α_ A A A).inv ≫
                  A ◁ (β_ A A).hom ▷ A ≫ ((A ◁ (α_ A A A).hom ≫ A ◁ 𝒮 ▷ (A ⊗ A)) ≫ (α_ A A (A ⊗ A)).inv) ≫ (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 5 6 =>
    rw [← whiskerLeft_comp, ← whiskerLeft_comp, ← BraidedCategory.braiding_naturality_left,
      whiskerLeft_comp, whiskerLeft_comp]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      Δ ▷ A ≫
        (α_ A A A).hom ≫
          A ◁ A ◁ Δ ≫
            ((((((A ◁ A ◁ 𝒮 ▷ A ≫ A ◁ A ◁ (β_ A A).hom) ≫ A ◁ (α_ A A A).inv) ≫ A ◁ (β_ A A).hom ▷ A) ≫
                    A ◁ (α_ A A A).hom) ≫
                  A ◁ 𝒮 ▷ (A ⊗ A)) ≫
                (α_ A A (A ⊗ A)).inv) ≫
              (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A)) =
    Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom

Tactic:
refine TensorProduct.ext <| LinearMap.ext fun x => LinearMap.ext_ring ?_

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (((TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))).compr₂ₛₗ
          (Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A))))
        x)
      1 =
    (((TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))).compr₂ₛₗ
          (Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom))
        x)
      1
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ hom P ≫ inv P = 𝟙 (TensorBimod.X (regular R) P)

Tactic:
dsimp only [hom, inv, TensorBimod.X]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ coequalizer.desc P.actLeft ⋯ ≫
      (λ_ P.X).inv ≫
        η ▷ P.X ≫
          coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) =
    𝟙 (coequalizer ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft))