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

Goal state before:
pp: case h₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U V : X ⥤ Y
α : U ⟶ V
W : Y ⥤ Z
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((precompose F G).map (whiskerRight α W)).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G U W).hom ≫
                ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).inv).app
            x✝¹).fst.app
      x✝

pp: case h₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U V : X ⥤ Y
α : U ⟶ V
W : Y ⥤ Z
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((precompose F G).map (whiskerRight α W)).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G U W).hom ≫
                ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).inv).app
            x✝¹).snd.app
      x✝

Tactic:
<;>

Goal state after:
case h₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U V : X ⥤ Y
α : U ⟶ V
W : Y ⥤ Z
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((precompose F G).map (whiskerRight α W)).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G U W).hom ≫
                ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).inv).app
            x✝¹).fst.app
      x✝

case h₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U V : X ⥤ Y
α : U ⟶ V
W : Y ⥤ Z
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((precompose F G).map (whiskerRight α W)).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G U W).hom ≫
                ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).inv).app
            x✝¹).snd.app
      x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.leftUnitor.hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G (𝟭 X) U).hom ≫
                ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫
                  ((precompose F G).obj U).rightUnitor.hom).app
            x✝¹).fst.app
      x✝

pp: case h₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.leftUnitor.hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G (𝟭 X) U).hom ≫
                ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫
                  ((precompose F G).obj U).rightUnitor.hom).app
            x✝¹).snd.app
      x✝

Tactic:
<;>

Goal state after:
case h₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.leftUnitor.hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G (𝟭 X) U).hom ≫
                ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫
                  ((precompose F G).obj U).rightUnitor.hom).app
            x✝¹).fst.app
      x✝

case h₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.leftUnitor.hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G (𝟭 X) U).hom ≫
                ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫
                  ((precompose F G).obj U).rightUnitor.hom).app
            x✝¹).snd.app
      x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.rightUnitor.hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫
                  ((precompose F G).obj U).leftUnitor.hom).app
            x✝¹).fst.app
      x✝

pp: case h₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.rightUnitor.hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫
                  ((precompose F G).obj U).leftUnitor.hom).app
            x✝¹).snd.app
      x✝

Tactic:
<;>

Goal state after:
case h₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.rightUnitor.hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫
                  ((precompose F G).obj U).leftUnitor.hom).app
            x✝¹).fst.app
      x✝

case h₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.rightUnitor.hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫
                  ((precompose F G).obj U).leftUnitor.hom).app
            x✝¹).snd.app
      x✝
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: 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
⊢ F.CoreMonoidal

Tactic:
by
  letI e := Lifting.iso L W G F
  refine Functor.CoreMonoidal.ofBifunctor
    (εIso G ≪≫ e.symm.app _ ≪≫ F.mapIso (εIso L).symm) (curriedTensorPreIsoPost L W F G) ?_ ?_ ?_
  · refine natTrans₃_ext L L L W W W (fun X₁ X₂ X₃ ↦ ?_)
    dsimp [e]
    rw [curriedTensorPreIsoPost_hom_app_app, curriedTensorPreIsoPost_hom_app_app,
      curriedTensorPreIsoPost_hom_app_app' L W F G (μIso L _ _) (Iso.refl _),
      curriedTensorPreIsoPost_hom_app_app' L W F G (Iso.refl _) (μIso L _ _)]
    monoidal_simps
    /-
    The following `simp only` block was generated by:
    ```
    simp? [← comp_whiskerRight_assoc, -comp_whiskerRight, whisker_exchange_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc, -MonoidalCategory.whiskerLeft_comp]
    ```
    -/
    simp only [comp_obj, μIso_hom, Iso.refl_hom, map_id, Category.id_comp, μIso_inv, Iso.refl_inv,
      MonoidalCategory.whiskerLeft_id, Category.comp_id, map_comp, Category.assoc,
      ← comp_whiskerRight_assoc, map_δ_μ_assoc, Iso.inv_hom_id_app, id_whiskerRight,
      whisker_exchange_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, whiskerRight_tensor]
    simp [← whisker_exchange_assoc, tensor_whiskerLeft_symm, -tensor_whiskerLeft,
      ← LaxMonoidal.associativity_assoc G, ← Functor.map_comp]
  · refine natTrans_ext L W (fun X₂ ↦ ?_)
    have := NatTrans.congr_app ((curriedTensorPreIsoPost L W F G).hom.naturality (εIso L).inv)
      (L.obj X₂)
    dsimp [e] at this ⊢
    monoidal_simps
    simp [reassoc_of% this, curriedTensorPreIsoPost_hom_app_app, ← comp_whiskerRight_assoc,
      -comp_whiskerRight, tensorHom_def, ← whisker_exchange_assoc, ← map_comp]
  · refine natTrans_ext L W (fun X₁ ↦ ?_)
    have := ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).naturality (εIso L).inv
    dsimp [e] at this ⊢
    monoidal_simps
    simp [reassoc_of% this, curriedTensorPreIsoPost_hom_app_app, tensorHom_def,
      whisker_exchange_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, ← map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.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₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) =
    pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

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₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) =
    pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
<;>

Goal state after:
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₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) =
    pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

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₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) =
    pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
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₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)

Tactic:
by
  refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp [whisker_exchange_assoc]) ?_) (by simp)
  apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
  · suffices _ ◁ _ ◁ f₃.right ≫ (α_ _ _ _).inv ≫ f₁.right ▷ _ ▷ _ ≫ (α_ _ _ _).hom ≫
      _ ◁ f₂.left ▷ _ ≫ _ ◁ pushout.inr _ _ = _ ◁ f₂.left ▷ _ ≫ _ ◁ _ ◁ f₃.right ≫
      _ ◁ pushout.inr _ _ ≫ f₁.right ▷ pushout (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) by
      simp [← whisker_exchange_assoc, reassoc_of% this]
    rw [← MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange, whisker_exchange_assoc,
      ← whisker_exchange, associator_inv_naturality_right_assoc, whisker_exchange_assoc,
      ← associator_inv_naturality_left_assoc, associator_naturality_right_assoc,
      Iso.inv_hom_id_assoc, MonoidalCategory.whiskerLeft_comp_assoc]
  · 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: 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
⊢ IsInitial (((curriedTensor C).obj X.right).obj (𝟙_ (Arrow C)).left)

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 : Arrow C
⊢ IsInitial (((curriedTensor C).obj X.right).obj (𝟙_ (Arrow C)).left)

Tactic:
<;>

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 : Arrow C
⊢ IsInitial (((curriedTensor C).obj X.right).obj (𝟙_ (Arrow C)).left)

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
⊢ IsInitial (((curriedTensor C).obj X.right).obj (𝟙_ (Arrow C)).left)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: case h_fst
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
Z : C
x : Z ⟶ X
m : Z ⟶ M
⊢ (lift m x ≫ leftSMul M X) ≫ fst X X = lift (m • x) x ≫ fst X X

pp: case h_snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
Z : C
x : Z ⟶ X
m : Z ⟶ M
⊢ (lift m x ≫ leftSMul M X) ≫ snd X X = lift (m • x) x ≫ snd X X

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
Z : C
x : Z ⟶ X
m : Z ⟶ M
⊢ (lift m x ≫ leftSMul M X) ≫ fst X X = lift (m • x) x ≫ fst X X

case h_snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
Z : C
x : Z ⟶ X
m : Z ⟶ M
⊢ (lift m x ≫ leftSMul M X) ≫ snd X X = lift (m • x) x ≫ snd X X
Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ eHomWhiskerLeft C X g = (ihom X).map g

Tactic:
change (ρ_ _).inv ≫ _ ◁ curry' g ≫ comp X Y₁ Y₂ = _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (ρ_ ((ihom X).obj Y₁)).inv ≫ (ihom X).obj Y₁ ◁ curry' g ≫ comp X Y₁ Y₂ = (ihom X).map g
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'
⊢ (F₁ ⊗ F₂).map φ ≫
      uncurry (g.app j' ≫ enrichedHomπ C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃) (Under.mk (𝟙 j'))) =
    uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))) ≫ F₃.map φ

Tactic:
by
        dsimp
        rw [← uncurry_natural_right, tensorHom_def'_assoc, ← uncurry_pre_app,
          ← uncurry_natural_left, Category.assoc, Category.assoc,
          NatTrans.naturality_assoc, functorEnrichedHom_map,
          end_.lift_π_assoc, enrichedOrdinaryCategorySelf_eHomWhiskerRight]
        dsimp
        rw [pre_id, NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerLeft,
          Functor.map_id, Category.comp_id, Category.comp_id]
        congr 2
        rw [← enrichedOrdinaryCategorySelf_eHomWhiskerRight,
          ← enrichedOrdinaryCategorySelf_eHomWhiskerLeft]
        let α : Under.mk (𝟙 j) ⟶ (Under.map φ).obj (Under.mk (𝟙 j')) := Under.homMk φ
        exact (enrichedHom_condition C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) α).symm

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ default ≫ default ≫ default = 𝟙 (⊥_ C)

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ (default ≫ default) ≫ default = 𝟙 (𝟙_ C)

Tactic:
<;>

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ default ≫ default ≫ default = 𝟙 (⊥_ C)

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ (default ≫ default) ≫ default = 𝟙 (𝟙_ C)
Module: Mathlib.CategoryTheory.Monoidal.Conv

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
M N : C
inst✝¹ : ComonObj M
inst✝ : MonObj N
f g h : Conv M N
⊢ Δ ≫ Δ ▷ M ≫ f ▷ M ▷ M ≫ (α_ N M M).hom ≫ N ◁ g ▷ M ≫ (α_ N N M).inv ≫ ((N ⊗ N) ◁ h ≫ μ ▷ N) ≫ μ =
    Δ ≫ f ▷ M ≫ N ◁ Δ ≫ N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ

Tactic:
slice_rhs 2 3 =>
      rw [← whisker_exchange]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
M N : C
inst✝¹ : ComonObj M
inst✝ : MonObj N
f g h : Conv M N
⊢ Δ ≫ Δ ▷ M ≫ f ▷ M ▷ M ≫ (α_ N M M).hom ≫ N ◁ g ▷ M ≫ (α_ N N M).inv ≫ ((N ⊗ N) ◁ h ≫ μ ▷ N) ≫ μ =
    Δ ≫ ((((M ◁ Δ ≫ f ▷ (M ⊗ M)) ≫ N ◁ g ▷ M) ≫ N ◁ N ◁ h) ≫ N ◁ μ) ≫ μ
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
⊢ (DayConvolution.unit F H).app (x, y) ≫ ℌ.ev_app.app (x ⊗ y) = MonoidalClosed.uncurry (ℌ.π y x)

Tactic:
by
  have := Functor.descOfIsLeftKanExtension_fac_app (F ⊛ H)
    (DayConvolution.unit F H) G
  dsimp at this
  simp [this, ev_app]

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

Goal state before:
pp: case mk.comp.h₁
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n ↦ X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n ↦ Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ (fun n ↦ X✝.normalizeObj n) = ?mk.comp.b

pp: case mk.comp.h₂
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n ↦ X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n ↦ Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ ?mk.comp.b = Z✝.normalizeObj

pp: case mk.comp.b
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n ↦ X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n ↦ Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ NormalMonoidalObject C → NormalMonoidalObject C

Tactic:
<;>

Goal state after:
case mk.comp.h₁
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n ↦ X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n ↦ Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ (fun n ↦ X✝.normalizeObj n) = ?mk.comp.b

case mk.comp.h₂
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n ↦ X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n ↦ Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ ?mk.comp.b = Z✝.normalizeObj

case mk.comp.b
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n ↦ X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n ↦ Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ NormalMonoidalObject C → NormalMonoidalObject C
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
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
| R.X ◁
    (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫
        coequalizer.desc
          ((α_ P.X Q.X L.X).hom ≫
            P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
              coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
                ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
                  P.X ◁ TensorBimod.actLeft Q L))
          ⋯)

pp: case a
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
| TensorBimod.actLeft P (Q.tensorBimod L)

Tactic:
π_tensor_id_preserves_coequalizer_inv_desc,

Goal state after:
case a
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
| R.X ◁
    ((α_ P.X Q.X L.X).hom ≫
      P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
        coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
          ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
            P.X ◁ TensorBimod.actLeft Q L))

case a
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
| TensorBimod.actLeft P (Q.tensorBimod L)