mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
⊢ (∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
      [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
      [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
      (Functor.pi L).IsLocalization (MorphismProperty.pi W)) →
    ∀ {C : J₂ → Type u₁} {D : J₂ → Type u₂} [inst : (j : J₂) → Category.{v₁, u₁} (C j)]
      [inst_1 : (j : J₂) → Category.{v₂, u₂} (D j)] (L : (j : J₂) → C j ⥤ D j) (W : (j : J₂) → MorphismProperty (C j))
      [∀ (j : J₂), (W j).ContainsIdentities] [∀ (j : J₂), (L j).IsLocalization (W j)],
      (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
hJ₁

Goal state after:
case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
⊢ ∀ {C : J₂ → Type u₁} {D : J₂ → Type u₂} [inst : (j : J₂) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₂) → Category.{v₂, u₂} (D j)] (L : (j : J₂) → C j ⥤ D j) (W : (j : J₂) → MorphismProperty (C j))
    [∀ (j : J₂), (W j).ContainsIdentities] [∀ (j : J₂), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝¹ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝ : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
⊢ ∀ (W : (j : J₂) → MorphismProperty (C₂ j)) [∀ (j : J₂), (W j).ContainsIdentities]
    [∀ (j : J₂), (L₂ j).IsLocalization (W j)], (Functor.pi L₂).IsLocalization (MorphismProperty.pi W)

Tactic:
W₂

Goal state after:
case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝¹ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝ : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
⊢ ∀ [∀ (j : J₂), (W₂ j).ContainsIdentities] [∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)],
    (Functor.pi L₂).IsLocalization (MorphismProperty.pi W₂)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
E : ((j : J₁) → C₂ (e j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ (e j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor
⊢ (MorphismProperty.pi fun j ↦ W₂ (e j)) ≤ (MorphismProperty.pi W₂).isoClosure.inverseImage E.functor

Tactic:
intro _

Goal state after:
case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
E : ((j : J₁) → C₂ (e j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ (e j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor
X✝ : (i : J₁) → C₂ (e i)
⊢ ∀ ⦃Y : (i : J₁) → C₂ (e i)⦄ (f : X✝ ⟶ Y),
    MorphismProperty.pi (fun j ↦ W₂ (e j)) f → (MorphismProperty.pi W₂).isoClosure.inverseImage E.functor f
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case associator_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₁✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₃✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((projectMapAux f✝ f₁✝ ⊗ₘ projectMapAux f✝ f₂✝) ⊗ₘ projectMapAux f✝ f₃✝) ≫
      (α_ (projectObj f✝ Y₁✝) (projectObj f✝ Y₂✝) (projectObj f✝ Y₃✝)).hom =
    (α_ (projectObj f✝ X₁✝) (projectObj f✝ X₂✝) (projectObj f✝ X₃✝)).hom ≫
      (projectMapAux f✝ f₁✝ ⊗ₘ projectMapAux f✝ f₂✝ ⊗ₘ projectMapAux f✝ f₃✝)

Tactic:
rw [MonoidalCategory.associator_naturality]

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₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Arrow.Hom.right ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = Arrow.Hom.right (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
by simp [whisker_exchange_assoc]

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₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ pushout.inl (((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.inl (((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:
by simp [whisker_exchange_assoc]

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
⊢ leftSMul M X ≫ fst X X = γ

Tactic:
simp [leftSMul]

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
⊢ leftSMul M X ≫ snd X X = snd M X

Tactic:
simp [leftSMul]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
⊢ ∀ {X : C} (a b c : X ⟶ R), (a + b) * c = a * c + b * c

Tactic:
← add_mul_iff,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)

Tactic:
rw [IsSubterminal.def] at hA

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ A ⨯ A ≅ A

Tactic:
by
  letI := IsSubterminal.isIso_diag hA
  apply (asIso (diag A)).symm

Goal state after:
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
this : HasFiniteProducts D
⊢ i.obj X ⨯ i.obj Y ≅ i.obj X ⊗ i.obj Y

Tactic:
refine Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit (pair (i.obj X) (i.obj Y)))
              (tensorProductIsBinaryProduct _ _)

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

Goal state before:
pp: case comm2
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
l : i.EssImageSubcategory ⥤ D
φ : l ⋙ i ≅ i.essImage.ι
B : D
⊢ i ⋙ ihom (i.obj B) ≅ (i.essImage.lift (i ⋙ ihom (i.obj B)) ⋯ ⋙ l) ⋙ i

Tactic:
exact (i.essImage.liftCompιIso _ _).symm.trans <|
            (Functor.isoWhiskerLeft _ φ.symm).trans (Functor.associator _ _ _).symm

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
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 ▷ TensorBimod.X Q L)
            ((α_ P.X S.X (TensorBimod.X Q L)).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 ▷ TensorBimod.X Q L)
            ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)

Tactic:
dsimp [TensorBimod.X]

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.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)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ normalizeIsoApp C (X.tensor Y) n = normalizeIsoApp' C (X.tensor Y) n.as

Tactic:
by
      rw [normalizeIsoApp, normalizeIsoApp']
      rw [normalizeIsoApp_eq X n]
      rw [normalizeIsoApp_eq Y ⟨normalizeObj X n.as⟩]
      simp

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
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.actRight ▷ L.X ≫
      (α_ 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)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ 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)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)

Tactic:
dsimp [TensorBimod.X]

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.actRight ▷ L.X ≫
      (α_ 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) =
    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)
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
⊢ p.toCostructuredArrow.Final

Tactic:
by
  have := isFiltered_of_isCardinalFiltered J κ
  rw [Functor.final_iff_of_isFiltered]
  refine ⟨fun f ↦ ?_, fun {f j} g₁ g₂ ↦ ?_⟩
  · obtain ⟨j, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit f.hom
    exact ⟨j, ⟨CostructuredArrow.homMk (ObjectProperty.homMk g)⟩⟩
  · obtain ⟨k, a, h⟩ := IsCardinalPresentable.exists_eq_of_isColimit' κ p.isColimit
      g₁.left.hom g₂.left.hom ((CostructuredArrow.w g₁).trans (CostructuredArrow.w g₂).symm)
    exact ⟨k, a, by cat_disch⟩

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✝³ : MonoidalCategoryStruct D
inst✝² : LawfulDayConvolutionMonoidalCategoryStruct C V D
d d' d'' : 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)
z x y : C
⊢ (unit ((ι C V D).obj d) ((ι C V D).obj d')).app (x, y) ▷ ((ι C V D).obj d'').obj z ≫
      (unit ((ι C V D).obj d ⊛ (ι C V D).obj d') ((ι C V D).obj d'')).app (x ⊗ y, z) ≫
        ((ι C V D).map (α_ d d' d'').hom).app ((x ⊗ y) ⊗ z) =
    (α_ (((ι C V D).obj d).obj x) (((ι C V D).obj d').obj y) (((ι C V D).obj d'').obj z)).hom ≫
      ((ι C V D).obj d).obj x ◁ (unit ((ι C V D).obj d') ((ι C V D).obj d'')).app (y, z) ≫
        (unit ((ι C V D).obj d) ((ι C V D).obj d' ⊛ (ι C V D).obj d'')).app (x, y ⊗ z) ≫
          ((ι C V D).obj d ⊛ (ι C V D).obj d' ⊛ (ι C V D).obj d'').map (α_ x y z).inv

Tactic:
exact associator_hom_unit_unit V _ _ _ _ _ _

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

Goal state before:
pp: case refine_1.comp.refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y✝¹ : C
f✝ : X ⟶ Y✝¹
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
U Y : C
j : F.I₀
v : U ⟶ F.X j
i : (Precoverage.ZeroHypercover.pullback₁ (F.f j) E).I₀
⊢ K.morphismProperty (pullback.snd (F.f j) (E.f i))

Tactic:
exact (F.pullback₂ (E.f i)).morphismProperty j

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ (MonoOver X)ᵒᵖ
⊢ IsFiltered.IsEventuallyConstant G

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m

Tactic:
· obtain ⟨n, hn⟩ := h ⟨_, (G ⋙ (Subobject.equivMonoOver X).inverse.op ⋙
      (orderDualEquivalence _).inverse).monotone⟩
    refine ⟨n, fun m hm ↦ ?_⟩
    rw [← isIso_unop_iff, MonoOver.isIso_iff_subobjectMk_eq]
    exact (hn m (leOfHom hm)).symm

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: 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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ whiskerRight f (regular Y) = M.rightUnitorBimod.hom ≫ f ≫ N.rightUnitorBimod.inv

Tactic:
dsimp [tensorHom, regular, rightUnitorBimod]
  ext
  apply coequalizer.hom_ext
  dsimp
  slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
  dsimp [RightUnitorBimod.hom]
  slice_rhs 1 2 => rw [coequalizer.π_desc]
  dsimp [RightUnitorBimod.inv]
  slice_rhs 1 2 => rw [Hom.right_act_hom]
  slice_rhs 2 3 => rw [rightUnitor_inv_naturality]
  slice_rhs 3 4 => rw [← whisker_exchange]
  slice_rhs 4 5 => rw [coequalizer.condition]
  slice_rhs 3 4 => rw [associator_naturality_right]
  slice_rhs 4 5 => rw [← whiskerLeft_comp, MonObj.mul_one]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ Projective P → (MorphismProperty.epimorphisms C).llp 0

Tactic:
intro _

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
a✝ : Projective P
⊢ (MorphismProperty.epimorphisms C).llp 0
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : c ∈ spectrum 𝕜 (End.of f)
⊢ c • 𝟙 X = f

Tactic:
spectrum.mem_iff,

Goal state after:
case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : ¬IsUnit ((algebraMap 𝕜 (End X)) c - End.of f)
⊢ c • 𝟙 X = f
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
hF : ∀ (j : J), IsCardinalFiltered (↑(F.obj j)) κ
this : IsFiltered J
K : Type u
f : K → CoconePt hc
hK : Cardinal.mk K < κ
⊢ ∃ j, ∀ (k : K), f k ≤ j

Tactic:
← hasCardinalLT_iff_cardinal_mk_lt

Goal state after:
κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
hF : ∀ (j : J), IsCardinalFiltered (↑(F.obj j)) κ
this : IsFiltered J
K : Type u
f : K → CoconePt hc
hK : HasCardinalLT K κ
⊢ ∃ j, ∀ (k : K), f k ≤ j
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ j →
      ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
        0

Tactic:
intro b _ hb
              rw [dif_pos rfl, dif_neg, zero_comp]
              simp only
              tauto

Goal state after: