mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c x y : C
f : x ⟶ y
d : D
⊢ (F.map (c ◁ f)).unmop.app d =
    ((Functor.Monoidal.μIso F c x).unmop.app d).symm.hom ≫
      (F.obj c).unmop.map ((F.map f).unmop.app d) ≫ ((Functor.Monoidal.μIso F c y).unmop.app d).symm.inv

Tactic:
have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.LaxMonoidal.μ_natural_right F c f

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c x y : C
f : x ⟶ y
d : D
e :
  (F.obj c ◁ F.map f ≫ Functor.LaxMonoidal.μ F c y).unmop.app d =
    (Functor.LaxMonoidal.μ F c x ≫ F.map (c ◁ f)).unmop.app d
⊢ (F.map (c ◁ f)).unmop.app d =
    ((Functor.Monoidal.μIso F c x).unmop.app d).symm.hom ≫
      (F.obj c).unmop.map ((F.map f).unmop.app d) ≫ ((Functor.Monoidal.μIso F c y).unmop.app d).symm.inv
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝² : MonoidalLeftAction C D
x y : C
x' y' : D
f : x ⟶ y
g : x' ⟶ y'
inst✝¹ : IsIso f
inst✝ : IsIso g
⊢ (f ⊙ₗₘ g) ≫ (inv f ⊙ₗₘ inv g) = 𝟙 (x ⊙ₗ x') ∧ (inv f ⊙ₗₘ inv g) ≫ (f ⊙ₗₘ g) = 𝟙 (y ⊙ₗ y')

Tactic:
by simp [← actionHom_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝² : MonoidalLeftAction C D
x y : C
x' y' : D
f : x ⟶ y
g : x' ⟶ y'
inst✝¹ : IsIso f
inst✝ : IsIso g
⊢ (f ⊙ₗₘ g) ≫ (inv f ⊙ₗₘ inv g) = 𝟙 (x ⊙ₗ x')

Tactic:
by simp [← actionHom_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x : C
⊢ (λ_ ((curriedAction C D).obj x)).inv =
    (curriedAction C D).map (λ_ x).inv ≫
      { app := fun x_1 ↦ (αᵣ x_1 (𝟙_ C) x).hom, naturality := ⋯ } ≫
        (actionUnitNatIso C D).hom ▷ (curriedAction C D).obj x

Tactic:
ext t
    simpa [-actionHom_leftUnitor] using
      t ⊴ᵣ (λ_ x).inv ≫= actionHom_leftUnitor x t

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝² : MonoidalRightAction C D
x y : D
x' y' : C
f : x ⟶ y
g : x' ⟶ y'
inst✝¹ : IsIso f
inst✝ : IsIso g
⊢ (f ⊙ᵣₘ g) ≫ (inv f ⊙ᵣₘ inv g) = 𝟙 (x ⊙ᵣ x') ∧ (inv f ⊙ᵣₘ inv g) ≫ (f ⊙ᵣₘ g) = 𝟙 (y ⊙ᵣ y')

Tactic:
by simp [← actionHom_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝² : MonoidalRightAction C D
x y : D
x' y' : C
f : x ⟶ y
g : x' ⟶ y'
inst✝¹ : IsIso f
inst✝ : IsIso g
⊢ (f ⊙ᵣₘ g) ≫ (inv f ⊙ᵣₘ inv g) = 𝟙 (x ⊙ᵣ x')

Tactic:
by simp [← actionHom_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : C
d₁✝ d₂✝ : D
f : c₁✝ ⟶ c₂✝
g : c₃✝ ⟶ c₄✝
h : d₁✝ ⟶ d₂✝
⊢ ((f ⊗ₘ g).op ⊙ₗₘ h.op).unop ≫ (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).symm.unop.hom =
    (αₗ (op c₁✝) (op c₃✝) (op d₁✝)).symm.unop.hom ≫ (f.op ⊙ₗₘ (g.op ⊙ₗₘ h.op).unop.op).unop

Tactic:
by
    apply Quiver.Hom.op_inj
    have := (αₗ (op _) (op _) (op _)).inv ≫=
      MonoidalLeftAction.actionAssocIso_hom_naturality f.op g.op h.op
    simp only [Iso.inv_hom_id_assoc] at this
    simp [← this]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have : (β_ (((e' e).functor ⋙ (e' e).inverse).obj X)
        (((e' e).functor ⋙ (e' e).inverse).obj Y)).hom =
          Functor.LaxMonoidal.μ (((e' e).functor ⋙ (e' e).inverse)) X Y ≫
            ((e' e).functor ⋙ (e' e).inverse).map (β_ X Y).hom ≫
              Functor.OplaxMonoidal.δ ((e' e).functor ⋙ (e' e).inverse) Y X := by
      simp only [((e' e).functor ⋙ (e' e).inverse).map_braiding X Y,
        assoc, Functor.Monoidal.μ_δ, comp_id, Functor.Monoidal.μ_δ_assoc]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
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 ◁ ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
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 P.X Q.X).inv

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
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)
| P.actLeft ▷ Q.X

Tactic:
rw [whiskerLeft_comp]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
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 ◁ (α_ P.X S.X Q.X).hom ≫ R.X ◁ P.X ◁ Q.actLeft

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
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 P.X Q.X).inv

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
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)
| P.actLeft ▷ Q.X
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 = (α_ R.X R.X (X P Q)).hom ≫ R.X ◁ actLeft P Q ≫ actLeft P Q

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, left_assoc, comp_whiskerRight, comp_whiskerRight]
  slice_rhs 1 2 => rw [associator_naturality_right]
  slice_rhs 2 3 =>
    rw [← whiskerLeft_comp, whiskerLeft_π_actLeft,
      whiskerLeft_comp, whiskerLeft_comp]
  slice_rhs 4 5 => rw [whiskerLeft_π_actLeft]
  slice_rhs 3 4 => rw [associator_inv_naturality_middle]
  monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
⊢ (∀ (b : Z ⟶ X ⊗ X), ∃! a, ((fun x ↦ x ≫ leftSMul M X) ∘ ⇑liftEquiv) a = b) ↔ ∀ (x y : Z ⟶ X), ∃! m, m • x = y

Tactic:
simp only [liftEquiv.surjective.forall, liftEquiv_apply, Prod.forall, Function.comp_apply, h]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
⊢ (∀ (a b : Z ⟶ X), ∃! a_1, a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔ ∀ (x y : Z ⟶ X), ∃! m, m • x = y
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ ∃ ψ, ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
refine ⟨Yoneda.fullyFaithful.preimage ?_, ?_⟩

Goal state after:
case refine_2.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ yoneda.obj (G ⊗ H) ⟶ yoneda.obj H

case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ Yoneda.fullyFaithful.preimage ?refine_2.refine_1 ≫ φ = G ◁ φ ≫ conj G
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 ≫ γ = ((f ▷ A ≫ B ◁ f) ⊵ₗ M ≫ μ ⊵ₗ M) ≫ γ

Tactic:
rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]

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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
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 X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ L.map (R.obj c ◁ R.map x✝) ≫ δ L (R.obj c) (R.obj Y✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y✝) =
    δ L (R.obj c) (R.obj X✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X✝) ≫ c ◁ x✝

Tactic:
← δ_natural_right_assoc,

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
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 X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫ L.obj (R.obj c) ◁ L.map (R.map x✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y✝) =
    δ L (R.obj c) (R.obj X✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X✝) ≫ c ◁ x✝
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₁.map φ ⊗ₘ 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:
← uncurry_natural_right,

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'
⊢ (F₁.map φ ⊗ₘ 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))) ≫
        (ihom (F₁.obj j)).map (F₃.map φ))
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
x✝² : C
x✝¹ x✝ : x✝² ⟶ ⊤_ C
⊢ x✝¹ = x✝

Tactic:
subsingleton

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 ≫ X.arrow = g ≫ X.arrow

Tactic:
subsingleton

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 Y : Subterminals C} (f : X ⟶ Y),
    (𝟭 (Subterminals C)).map f ≫ (Iso.refl Y).hom =
      (Iso.refl X).hom ≫
        ({ obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun X ↦ { obj := X.obj.left, property := ⋯ },
                map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ }).map
          f

Tactic:
subsingleton

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 Y : MonoOver (⊤_ C)} (f : X ⟶ Y),
    ({ obj := fun X ↦ { obj := X.obj.left, property := ⋯ }, map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left,
                map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).map
          f ≫
        (MonoOver.isoMk
            (Iso.refl
              (({ obj := fun X ↦ { obj := X.obj.left, property := ⋯ },
                          map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                          map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).obj
                    Y).obj.left)
            ⋯).hom =
      (MonoOver.isoMk
            (Iso.refl
              (({ obj := fun X ↦ { obj := X.obj.left, property := ⋯ },
                          map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                          map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).obj
                    X).obj.left)
            ⋯).hom ≫
        (𝟭 (MonoOver (⊤_ C))).map f

Tactic:
subsingleton

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 : Subterminals C),
    { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
              map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }.map
          ((NatIso.ofComponents (fun X ↦ Iso.refl X) ⋯).hom.app X) ≫
        (NatIso.ofComponents
                (fun X ↦
                  MonoOver.isoMk
                    (Iso.refl
                      (({ obj := fun X ↦ { obj := X.obj.left, property := ⋯ },
                                  map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ } ⋙
                                { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                                  map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).obj
                            X).obj.left)
                    ⋯)
                ⋯).hom.app
          ({ obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }.obj
            X) =
      𝟙
        ({ obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
              map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }.obj
          X)

Tactic:
subsingleton

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✝¹² : ∀ (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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (β_ (F.obj x) (H.obj z)).hom ≫
          G.obj y ◁ (unit H F).app (z, x) ≫
            (unit G (H ⊛ F)).app (y, z ⊗ x) ≫ (G ⊛ H ⊛ F).map (y ◁ (β_ z x).hom ≫ (α_ y x z).inv ≫ (β_ y x).hom ▷ z) =
    (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (unit F H).app (x, z) ≫
          G.obj y ◁ (braiding F H).hom.app (x ⊗ z) ≫
            (unit G (H ⊛ F)).app (y, x ⊗ z) ≫ (G ⊛ H ⊛ F).map ((α_ y x z).inv ≫ (β_ y x).hom ▷ z)

Tactic:
← BraidedCategory.hexagon_reverse,

Goal state after:
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✝¹² : ∀ (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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (β_ (F.obj x) (H.obj z)).hom ≫
          G.obj y ◁ (unit H F).app (z, x) ≫
            (unit G (H ⊛ F)).app (y, z ⊗ x) ≫ (G ⊛ H ⊛ F).map ((α_ y z x).inv ≫ (β_ (y ⊗ z) x).hom ≫ (α_ x y z).inv) =
    (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (unit F H).app (x, z) ≫
          G.obj y ◁ (braiding F H).hom.app (x ⊗ z) ≫
            (unit G (H ⊛ F)).app (y, x ⊗ z) ≫ (G ⊛ H ⊛ F).map ((α_ y x z).inv ≫ (β_ y x).hom ▷ z)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

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

Tactic:
antipode_left_assoc

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (((α_ P.X (Q.X ⊗ T.X) L.X).inv ≫ (P.X ◁ Q.actRight) ▷ L.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X) ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
          coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) =
    P.X ◁ ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
              coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)

Tactic:
rw [← Iso.inv_hom_id_assoc (α_ _ _ _) (P.X ◁ Q.actRight), comp_whiskerRight]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (((α_ P.X (Q.X ⊗ T.X) L.X).inv ≫ (α_ P.X Q.X T.X).inv ▷ L.X ≫ ((α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight) ▷ L.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X) ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
          coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) =
    P.X ◁ ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
              coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)