mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ i₂ + i₁ + i₃ = k

Tactic:
add_comm i₂ i₁,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ i₁ + i₂ + i₃ = k
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ {p | Discrete.Arrows c d p} → Groupoid.inv p ∈ {p | Discrete.Arrows d c p}

Tactic:
by rintro _ _ _ ⟨⟩; simp only [inv_eq_inv, IsIso.inv_id]; constructor

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a b c d : C ⋆ D
f : a.Hom b
g : b.Hom c
h : c.Hom d
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases a

Goal state after:
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
b c d : C ⋆ D
g : b.Hom c
h : c.Hom d
a✝ : C
f : (left a✝).Hom b
⊢ comp (comp f g) h = comp f (comp g h)

case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
b c d : C ⋆ D
g : b.Hom c
h : c.Hom d
a✝ : D
f : (right a✝).Hom b
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Limits.Pi

Goal state before:
pp: I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
m : (coconeOfCoconeCompEval c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeCompEval c).ι.app j ≫ m = s.ι.app j
⊢ m = fun i ↦ (P i).desc (coconeCompEval s i)

Tactic:
funext i
    exact (P i).uniq (coconeCompEval s i) (m i) fun j => congr_fun (w j) i

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.FinCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a : Option C
⊢ (fun x ↦
        match x with
        | of a => some a
        | star => none)
      ((fun x ↦
          match x with
          | some a => of a
          | none => star)
        a) =
    a

Tactic:
cases a

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
⊢ (fun x ↦
        match x with
        | of a => some a
        | star => none)
      ((fun x ↦
          match x with
          | some a => of a
          | none => star)
        none) =
    none

case some
C : Type u
inst✝ : Category.{v, u} C
val✝ : C
⊢ (fun x ↦
        match x with
        | of a => some a
        | star => none)
      ((fun x ↦
          match x with
          | some a => of a
          | none => star)
        (some val✝)) =
    some val✝
Module: Mathlib.CategoryTheory.WithTerminal.FinCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a : WithTerminal C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        a) =
    a

Tactic:
cases a

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        (of a✝)) =
    of a✝

case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        star) =
    star
Module: Mathlib.CategoryTheory.WithTerminal.FinCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a : WithInitial C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        a) =
    a

Tactic:
cases a

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        (of a✝)) =
    of a✝

case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        star) =
    star
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ ∀ (j : WithTerminal J),
    ((Cone.postcompose
                  (NatIso.ofComponents
                      (fun i ↦
                        WithTerminal.casesOn i
                          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                      ⋯).hom).obj
              (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).π.app
        j =
      (Iso.refl
            ((Cone.postcompose
                    (NatIso.ofComponents
                        (fun i ↦
                          WithTerminal.casesOn i
                            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
                        ⋯).hom).obj
                (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })).pt).hom ≫
        ((Over.forget F).mapCone
                { pt := G,
                  π :=
                    {
                      app := fun i ↦
                        WithTerminal.casesOn i α.app
                          (Over.mkIdTerminal.from (((const (WithTerminal J)).obj G).obj WithTerminal.star)),
                      naturality := ⋯ } }).π.app
          j

Tactic:
by rintro ⟨⟩ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
r t : Cone F
i : r ≅ t
x✝ : IsWeakLimit r
⊢ (fun h ↦ h.ofIsoWeakLimit i.symm) ((fun h ↦ h.ofIsoWeakLimit i) x✝) = x✝

Tactic:
simp [ofIsoWeakLimit]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
r t : Cone F
i : r ≅ t
x✝ : IsWeakLimit t
⊢ (fun h ↦ h.ofIsoWeakLimit i) ((fun h ↦ h.ofIsoWeakLimit i.symm) x✝) = x✝

Tactic:
simp [ofIsoWeakLimit]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝ : IsIso η
φ : CatCospanTransform F' G' F'' G''
⊢ inv (η ▷ φ) = inv η ▷ φ

Tactic:
by
  apply IsIso.inv_eq_of_hom_inv_id
  simp [← comp_whiskerRight]

Goal state after:
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
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  ((curriedTensorPre F).obj Y₁).map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ ((curriedTensorPost F).obj Y₁).map e₂.hom
⊢ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))

Tactic:
have h₂ := congr_app ((curriedTensorPreIsoPost L W F G).hom.naturality e₁.hom)

Goal state after:
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
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  ((curriedTensorPre F).obj Y₁).map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ ((curriedTensorPost F).obj Y₁).map e₂.hom
h₂ :
  ∀ (X : D),
    ((curriedTensorPre F).map e₁.hom ≫ (curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁ ≫ (curriedTensorPost F).map e₁.hom).app X
⊢ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ.hom ≫ M.X.X ◁ Δ.hom = Δ.hom ≫ Δ.hom ▷ M.X.X ≫ (α_ M.X.X M.X.X M.X.X).hom

Tactic:
by
    simp_rw [← BimonObjAux_comul, ComonObj.comul_assoc]

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

Tactic:
slice_lhs 1 2 => rw [associator_naturality_left]

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
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)
⊢ ((α_ (P.X ⊗ S.X) Q.X T.X).hom ≫ P.actRight ▷ (Q.X ⊗ T.X)) ≫ P.X ◁ Q.actRight =
    ((α_ (P.X ⊗ S.X) Q.X T.X).hom ≫ (α_ P.X S.X (Q.X ⊗ T.X)).hom ≫ P.X ◁ S.X ◁ Q.actRight ≫ (α_ P.X S.X Q.X).inv) ≫
      P.actRight ▷ Q.X
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h₁
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
X Y : D
⊢ BinaryFan.fst
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))) =
    (_root_.id (asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))).symm).hom ≫
      (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).fst

Tactic:
simp only [BinaryFan.fst, Cone.postcompose, pairComp]

Goal state after:
case h₁
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
X Y : D
⊢ ((i.mapCone
              (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y))).π ≫
          (diagramIsoPair (pair X Y ⋙ i)).hom).app
      { as := WalkingPair.left } =
    (_root_.id (asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))).symm).hom ≫
      (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).π.app { as := WalkingPair.left }
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.actRight ▷ Q.X ▷ L.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) =
    ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.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)

Tactic:
slice_lhs 1 2 => rw [associator_naturality_left]

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 ⊗ S.X) Q.X L.X).hom ≫ P.actRight ▷ (Q.X ⊗ L.X)) ≫
        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) =
    ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.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)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ (bijection i A B ((reflector i).obj A ⊗ (reflector i).obj B))
        ((bijection i A B ((reflector i).obj A ⊗ (reflector i).obj B)).symm
          (𝟙 ((reflector i).obj A ⊗ (reflector i).obj B))) ≫
      (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) =
    (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B)))

Tactic:
Equiv.apply_symm_apply,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ 𝟙 ((reflector i).obj A ⊗ (reflector i).obj B) ≫
      (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) =
    (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B)))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x * 1 = x

Tactic:
convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_one A)) (x ⊗ₜ (1 : R))

Goal state after:
case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = (Hom.hom (MonoidalCategoryStruct.rightUnitor A).hom) (x ⊗ₜ[R] 1)
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
⊢ (mopEquiv C).inverse.map (MonObj.one ≫ f.mop) = (mopEquiv C).inverse.map MonObj.one

Tactic:
simpa [-IsMonHom.one_hom] using! IsMonHom.one_hom f

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
⊢ (mopEquiv C).functor.map (MonObj.one ≫ f.unmop) = (mopEquiv C).functor.map MonObj.one

Tactic:
simpa [-IsMonHom.one_hom] using! IsMonHom.one_hom f

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hp : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
⊢ P.ind.ind = P.ind

Tactic:
by
  refine le_antisymm (fun X Y f hf ↦ ?_) P.ind.le_ind
  have : P.underObj ≤ ObjectProperty.isFinitelyPresentable.{w} (Under X) := fun f hf ↦ hp _ hf
  simpa [ind_iff_ind_underMk, underObj_ind_eq_ind_underObj,
    ObjectProperty.ind_ind.{w} this] using hf

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
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore 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) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
d₁ d₁' d₂ d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
u₁ u₂ : C
⊢ (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₁')).app (u₁, u₂) ≫
      (tensorObjIsoConvolution C V d₁ d₁').hom.app (u₁ ⊗ u₂) ≫
        (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')).app (u₁ ⊗ u₂) ≫
          (tensorObjIsoConvolution C V d₂ d₂').inv.app (u₁ ⊗ u₂) =
    (((ι C V D).map f).app u₁ ⊗ₘ ((ι C V D).map f').app u₂) ≫
      (DayConvolution.unit ((ι C V D).obj d₂) ((ι C V D).obj d₂')).app (u₁, u₂)

Tactic:
simp +instances [convolutions, convolutionUnitApp_eq]

Goal state after: