mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

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

Tactic:
dsimp only [projectMapAux]

Goal state after:
case tensorHom_comp_tensorHom
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₁✝ X₂✝ Y₂✝ Z₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₁✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g₁✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (projectMapAux f✝ f₁✝ ⊗ₘ projectMapAux f✝ f₂✝) ≫ (projectMapAux f✝ g₁✝ ⊗ₘ projectMapAux f✝ g₂✝) =
    projectMapAux f✝ f₁✝ ≫ projectMapAux f✝ g₁✝ ⊗ₘ projectMapAux f✝ f₂✝ ≫ projectMapAux f✝ g₂✝
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]

Goal state after:
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)
⊢ (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).hom ≫
      (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).inv =
    𝟙 (projectObj f✝ ((X✝.tensor Y✝).tensor Z✝))
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case α_inv_hom
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✝ ((α_inv X✝ Y✝ Z✝).comp (α_hom X✝ Y✝ Z✝)) = projectMapAux f✝ (Hom.id (X✝.tensor (Y✝.tensor Z✝)))

Tactic:
dsimp only [projectMapAux]

Goal state after:
case α_inv_hom
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)
⊢ (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).inv ≫
      (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).hom =
    𝟙 (projectObj f✝ (X✝.tensor (Y✝.tensor Z✝)))
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

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

Tactic:
dsimp only [projectMapAux]

Goal state after:
case associator_naturality
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₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₁✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₃✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((projectMapAux f✝ f₁✝ ⊗ₘ projectMapAux f✝ f₂✝) ⊗ₘ projectMapAux f✝ f₃✝) ≫
      (α_ (projectObj f✝ Y₁✝) (projectObj f✝ Y₂✝) (projectObj f✝ Y₃✝)).hom =
    (α_ (projectObj f✝ X₁✝) (projectObj f✝ X₂✝) (projectObj f✝ X₃✝)).hom ≫
      (projectMapAux f✝ f₁✝ ⊗ₘ projectMapAux f✝ f₂✝ ⊗ₘ projectMapAux f✝ f₃✝)
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]

Goal state after:
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)
⊢ (ρ_ (projectObj f✝ X✝)).hom ≫ (ρ_ (projectObj f✝ X✝)).inv = 𝟙 (projectObj f✝ (X✝.tensor unit))
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case ρ_inv_hom
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✝ ((ρ_inv X✝).comp (ρ_hom X✝)) = projectMapAux f✝ (Hom.id X✝)

Tactic:
dsimp only [projectMapAux]

Goal state after:
case ρ_inv_hom
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)
⊢ (ρ_ (projectObj f✝ X✝)).inv ≫ (ρ_ (projectObj f✝ X✝)).hom = 𝟙 (projectObj f✝ X✝)
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]

Goal state after:
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)
⊢ (λ_ (projectObj f✝ X✝)).hom ≫ (λ_ (projectObj f✝ X✝)).inv = 𝟙 (projectObj f✝ (unit.tensor X✝))
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case l_inv_hom
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_inv X✝).comp (l_hom X✝)) = projectMapAux f✝ (Hom.id X✝)

Tactic:
dsimp only [projectMapAux]

Goal state after:
case l_inv_hom
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)
⊢ (λ_ (projectObj f✝ X✝)).inv ≫ (λ_ (projectObj f✝ X✝)).hom = 𝟙 (projectObj f✝ 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
⊢ ∃ ψ, ψ ≫ η = G ◁ η ≫ conj G

Tactic:
use toUnit _
    simp [conj, comp_mul, comp_inv, toUnit_unique _ (toUnit _), ← Hom.one_def]

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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ uncurry
      (g.app j ≫
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
            eHomWhiskerRight C ((Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₁)).inv.app (Under.mk (𝟙 j')))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))) ≫
              eHomWhiskerLeft C ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
                ((Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₃)).hom.app (Under.mk (𝟙 j')))) ≫
          (pre (F₁.map φ)).app (F₃.obj j')) =
    uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ))

Tactic:
enrichedOrdinaryCategorySelf_eHomWhiskerRight

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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ uncurry
      (g.app j ≫
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
            (pre ((Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₁)).inv.app (Under.mk (𝟙 j')))).app
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))) ≫
              eHomWhiskerLeft C ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
                ((Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₃)).hom.app (Under.mk (𝟙 j')))) ≫
          (pre (F₁.map φ)).app (F₃.obj j')) =
    uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ))
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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ uncurry
      (g.app j ≫
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
            (𝟙 (ihom (F₁.obj j'))).app (F₃.obj j') ≫ eHomWhiskerLeft C (F₁.obj j') (𝟙 (F₃.obj j'))) ≫
          (pre (F₁.map φ)).app (F₃.obj j')) =
    uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ))

Tactic:
NatTrans.id_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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ uncurry
      (g.app j ≫
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
            𝟙 ((ihom (F₁.obj j')).obj (F₃.obj j')) ≫ eHomWhiskerLeft C (F₁.obj j') (𝟙 (F₃.obj j'))) ≫
          (pre (F₁.map φ)).app (F₃.obj j')) =
    uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ))
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
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
          (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁
              ((Enriched.FunctorCategory.homEquiv C) f₃ ≫
                enrichedHomπ C F₃ F₃' k.right ≫
                  (𝟙 (ihom (F₃.obj k.right))).app (F₃'.obj k.right) ≫
                    (ihom (F₃.obj k.right)).map (𝟙 (F₃'.obj k.right))) ≫
            eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)

Tactic:
NatTrans.id_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₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
          (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁
              ((Enriched.FunctorCategory.homEquiv C) f₃ ≫
                enrichedHomπ C F₃ F₃' k.right ≫
                  𝟙 ((ihom (F₃.obj k.right)).obj (F₃'.obj k.right)) ≫
                    (ihom (F₃.obj k.right)).map (𝟙 (F₃'.obj k.right))) ≫
            eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)
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
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫ F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2))
⊢ F.map f.1 ▷ H.obj x.2 ≫
      F.obj y.1 ◁ (ℌ.π x.2 y.1 ≫ (ihom (F.obj y.1)).map (G.map (y.1 ◁ f.2))) ≫
        (ihom.ev (F.obj y.1)).app (G.obj (y.1 ⊗ y.2)) =
    F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ (ihom.ev (F.obj x.1)).app (G.obj (x.1 ⊗ x.2)) ≫ G.map (f.1 ⊗ₘ f.2)

Tactic:
simp only [whiskerLeft_comp, Category.assoc, ihom.ev_naturality,
          Functor.comp_obj, curriedTensor_obj_obj, Functor.id_obj,
          ← whisker_exchange_assoc, tensorHom_def, Functor.map_comp,
          ← ihom.ev_naturality_assoc]

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
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫ F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2))
⊢ F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.map f.1 ▷ (ihom (F.obj y.1)).obj (G.obj (y.1 ⊗ x.2)) ≫
        (ihom.ev (F.obj y.1)).app (G.obj (y.1 ⊗ x.2)) ≫ G.map (y.1 ◁ f.2) =
    F.obj x.1 ◁ ℌ.π x.2 x.1 ≫
      F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) ≫
        (ihom.ev (F.obj x.1)).app (G.obj (y.1 ⊗ x.2)) ≫ G.map (y.1 ◁ f.2)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (Δ ≫ A ◁ Δ)

pp: case a.a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮 ▷ A

pp: case a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (α_ A A A).inv

pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ ▷ A

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

Tactic:
rw [ComonObj.comul_assoc]

Goal state after:
case a.a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (Δ ≫ Δ ▷ A ≫ (α_ A A A).hom)

case a.a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮 ▷ A

case a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (α_ A A A).inv

case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ ▷ A

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
r : R
a : ↑A
h₁ :
  (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ)) (r ⊗ₜ[R] a) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor A).hom) (r ⊗ₜ[R] a)
h₂ :
  (Hom.hom (MonoidalCategoryStruct.whiskerLeft A η ≫ μ)) (a ⊗ₜ[R] r) =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor A).hom) (a ⊗ₜ[R] r)
⊢ (Hom.hom η) r * a = a * (Hom.hom η) r

Tactic:
exact h₁.trans h₂.symm

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

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
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
x y z : C
⊢ F.obj x ◁ (unit G H).app (y, z) ≫ (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ (associator F G H).inv.app (x ⊗ y ⊗ z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
      (unit F G).app (x, y) ▷ H.obj z ≫ (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ ((F ⊛ G) ⊛ H).map (α_ x y z).hom

Tactic:
by
  have := congrArg (fun t ↦ t.app (x, y, z)) <|
      (corepresentableBy₂ F G H).homEquiv.rightInverse_symm <|
        (corepresentableBy₂' F G H |>.ofIso
          (associatorCorepresentingIso F G H) |>.homEquiv (𝟙 _))
  dsimp [associator, Coyoneda.fullyFaithful, corepresentableBy₂,
    corepresentableBy₂', Functor.CorepresentableBy.ofIso, corepresentableBy₂,
    Functor.corepresentableByEquiv, associatorCorepresentingIso] at this ⊢
  simp only [whiskerRight_tensor, id_whiskerRight, Category.id_comp, Iso.inv_hom_id] at this
  simp only [this]
  dsimp [Functor.FullyFaithful.homEquiv, Equivalence.fullyFaithfulFunctor, prod.associativity]
  erw [id_apply] -- TODO: remove this `erw` (introduced in #36613)
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
M : Cᴹᵒᵖ
inst✝² : MonObj M
N : Cᴹᵒᵖ
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ MonObj.mul ≫ f.unmop = (f.unmop ⊗ₘ f.unmop) ≫ MonObj.mul

Tactic:
by
    apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
    simpa [-IsMonHom.mul_hom] using! IsMonHom.mul_hom f

Goal state after: