mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
⊢ 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) =
    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:
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

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₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (tensorRight X₃.right).map
        (pushout.inl (((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.inl (((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₃))

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₃))
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
⊢ 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) =
    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:
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

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 : Arrow C
⊢ (tensorRight Y.right).map
        (pushout.inl (((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.inl (((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)

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)
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 : Arrow C
⊢ pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom)

Tactic:
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

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 : Arrow C
⊢ (tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map X.hom).app Y.left) (((curriedTensor C).obj X.left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    (tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map X.hom).app Y.left) (((curriedTensor C).obj X.left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom)

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 : Arrow C
⊢ (tensorRight Z.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app Y.left) (((curriedTensor C).obj X.left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    (tensorRight Z.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app Y.left) (((curriedTensor C).obj X.left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom)
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ η ▷ X P Q ≫ actLeft P Q = (λ_ (X P Q)).hom

Tactic:
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
  dsimp [X]
  slice_lhs 1 2 => rw [whisker_exchange]
  slice_lhs 2 3 => rw [whiskerLeft_π_actLeft]
  slice_lhs 1 2 => rw [associator_inv_naturality_left]
  slice_lhs 2 3 => rw [← comp_whiskerRight, one_actLeft]
  slice_rhs 1 2 => rw [leftUnitor_naturality]
  monoidal

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

Tactic:
slice_rhs 1 2 => rw [associator_naturality_right]

Goal state after:
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 ≫
      ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (((α_ R.X R.X (P.X ⊗ Q.X)).hom ≫
          R.X ◁ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
        R.X ◁ actLeft P Q) ≫
      actLeft P Q
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ μ ⊵ₗ M ≫ f ⊵ₗ M ≫ γ = (αₗ A A M).hom ≫ (f ⊵ₗ (A ⊙ₗ M) ≫ B ⊴ₗ (f ⊵ₗ M ≫ γ)) ≫ γ

Tactic:
simp only [actionHomLeft_action_assoc, Category.assoc, Iso.hom_inv_id_assoc,
      actionHomRight_comp]

Goal state after:
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ μ ⊵ₗ M ≫ f ⊵ₗ M ≫ γ = (f ▷ A) ⊵ₗ M ≫ (αₗ B A M).hom ≫ B ⊴ₗ f ⊵ₗ M ≫ B ⊴ₗ γ ≫ γ
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ X P Q ◁ μ ≫ actRight P Q = (α_ (X P Q) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
  dsimp [X]
  slice_lhs 1 2 => rw [← whisker_exchange]
  slice_lhs 2 3 => rw [π_tensor_id_actRight]
  slice_lhs 1 2 => rw [associator_naturality_right]
  slice_lhs 2 3 => rw [← whiskerLeft_comp, right_assoc,
    whiskerLeft_comp, whiskerLeft_comp]
  slice_rhs 1 2 => rw [associator_inv_naturality_left]
  slice_rhs 2 3 => rw [← comp_whiskerRight, π_tensor_id_actRight, comp_whiskerRight,
    comp_whiskerRight]
  slice_rhs 4 5 => rw [π_tensor_id_actRight]
  simp

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ F.obj A ◁ (expComparison F A).natTrans.app B ≫ (ihom.ev (F.obj A)).app (F.obj B) =
    inv (prodComparison F A ((ihom A).obj B)) ≫ F.map ((ihom.ev A).app B)

Tactic:
by
  convert! mateEquiv_counit _ _ (prodComparisonNatIso F A).inv B using 2
  apply IsIso.inv_eq_of_hom_inv_id -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): was `ext`
  simp only [prodComparisonNatTrans_app, prodComparisonNatIso_inv, NatIso.isIso_inv_app,
    IsIso.hom_inv_id]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
⊢ Unique (X ⟶ Y)

Tactic:
by
  haveI : HasInitial C := HasZeroObject.hasInitial
  apply uniqueHomsetOfInitialIsoUnit _ X Y
  refine ⟨default, (default : 𝟙_ C ⟶ 0) ≫ default, ?_, ?_⟩ <;> simp [eq_iff_true_of_subsingleton]

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 G' : C ⥤ V
η : G ⟶ G'
c c' : C
f : c ⟶ c'
j : Cᵒᵖ
k : C
⊢ (MonoidalClosed.internalHom.obj (op (F.obj (unop j)))).map (G.map (k ◁ f)) ≫
      (MonoidalClosed.internalHom.obj (op (F.obj (unop j)))).map (η.app (k ⊗ c')) =
    (MonoidalClosed.internalHom.obj (op (F.obj (unop j)))).map (η.app (k ⊗ c)) ≫
      (MonoidalClosed.internalHom.obj (op (F.obj (unop j)))).map (G'.map (k ◁ f))

Tactic:
simpa [-NatTrans.naturality] using!
          congr_arg (ihom <| F.obj <| unop j).map (η.naturality <| k ◁ f)

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

Tactic:
slice_lhs 3 5 =>
    rw [← associator_naturality_right, ← Category.assoc, ← tensorHom_def]

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 ⊗ A)).hom) ≫ A ◁ (α_ A A A).inv) ≫ A ◁ (β_ A A).hom ▷ A) ≫ A ◁ (α_ A A A).hom) ≫
            (α_ A A (A ⊗ A)).inv) ≫
          (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
⊢ map (map f g) h ≫ (associator F' G' H').hom = (associator F G H).hom ≫ map f (map g h)

Tactic:
by
  apply (corepresentableBy₂' F G H) |>.homEquiv.injective
  dsimp
  ext
  simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, Functor.prod_obj, tensor_obj,
    Functor.id_obj, Functor.homEquivOfIsLeftKanExtension_apply_app,
    externalProductBifunctor_map_app, Functor.leftUnitor_inv_app, whiskerLeft_id, Category.comp_id,
    corepresentableBy_homEquiv_apply_app, NatTrans.comp_app, unit_app_map_app_assoc]
  rw [associator_hom_unit_unit_assoc]
  simp only [tensorHom_def, Category.assoc, externalProductBifunctor_obj_obj, tensor_obj,
    NatTrans.naturality, unit_app_map_app_assoc]
  rw [← comp_whiskerRight_assoc, unit_app_map_app]
  simp only [Functor.comp_obj, tensor_obj, comp_whiskerRight, Category.assoc]
  rw [← whisker_exchange_assoc, associator_hom_unit_unit, whisker_exchange_assoc,
    ← MonoidalCategory.whiskerLeft_comp_assoc, unit_app_map_app]
  simp [tensorHom_def]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j : J
i i' : I j
u : i ⟶ i'
⊢ (Q j).diag.map u ≫ c.ι.app ⟨j, i'⟩ = c.ι.app ⟨j, i⟩ ≫ ((Functor.const (I j)).obj c.pt).map u

Tactic:
let v : Total.mk Q j i ⟶ .mk _ j i' := { base := 𝟙 _, hom := (Q _).diag.map u }
            simpa using c.ι.naturality v

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✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
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)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
x✝ y₁ y₂ : D
f : y₁ ⟶ y₂
x y : C
⊢ (unit ((ι C V D).obj x✝) ((ι C V D).obj y₁)).app (x, y) ≫ (map ((ι C V D).map (𝟙 x✝)) ((ι C V D).map f)).app (x ⊗ y) =
    (unit ((ι C V D).obj x✝) ((ι C V D).obj y₁)).app (x, y) ≫ ((ι C V D).map (x✝ ◁ f)).app (x ⊗ y)

Tactic:
simp only [Functor.map_id, unit_app_map_app, Functor.comp_obj, tensor_obj,
        NatTrans.id_app, id_tensorHom]

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✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
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)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
x✝ y₁ y₂ : D
f : y₁ ⟶ y₂
x y : C
⊢ ((ι C V D).obj x✝).obj x ◁ ((ι C V D).map f).app y ≫ (unit ((ι C V D).obj x✝) ((ι C V D).obj y₂)).app (x, y) =
    (unit ((ι C V D).obj x✝) ((ι C V D).obj y₁)).app (x, y) ≫ ((ι C V D).map (x✝ ◁ f)).app (x ⊗ y)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case of
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : P f
⊢ Q f

Tactic:
exact h _ hf

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case of_presieve
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f✝ : X ⟶ Z
X✝ Y✝ : C
f : X✝ ⟶ Y✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h✝ : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    R g →
      ∀ (W : C) (g_1 : Y ⟶ Y✝) (fst : W ⟶ U) (snd : W ⟶ Y), IsPullback fst snd (g ≫ f) g_1 → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ X✝
snd : W ⟶ Y
h : IsPullback fst snd f g
⊢ sourceLocalClosure K P snd

Tactic:
refine .of_presieve _ _ (K.pullbackArrows_mem fst hR) ?_
      intro U v ⟨Z, u, hu⟩
      exact ih _ _ hu _ g (pullback.fst _ _) _ (.paste_vert (.of_hasPullback _ _) h)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : comma F₁ F₂ P₁ P₂ f
⊢ (comma F₁ F₂ Q₁ Q₂).isoClosure f

Tactic:
simp only [comma_iff] at hf

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : P₁ f.left ∧ P₂ f.right
⊢ (comma F₁ F₂ Q₁ Q₂).isoClosure f
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := Int.negSucc x✝¹ • x✝.left, right := Int.negSucc x✝¹ • x✝.right, w := ⋯ } =
    -{ left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ }

Tactic:
ext <;> dsimp <;> simp [add_nsmul, add_zsmul]

Goal state after: