mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y ≫ (DerivedCategory.singleFunctor C 0).map g))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map ((singleFunctor C 0).map g) ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯

Tactic:
← NatTrans.naturality

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          ((singleFunctor C 0 ⋙ DerivedCategory.Q).map g ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map ((singleFunctor C 0).map g) ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n✝ n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
⊢ R'.complex.d m n ≫ φ.hom.f n ≫ f = 0

Tactic:
simp [← φ.hom.comm_assoc, hf]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        HomologicalComplex.homologyMap
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map
              (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X)))
            0 ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex) =
    (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (F.rightDerivedToHomotopyCategory.map f)

Tactic:
← NatTrans.naturality

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        HomologicalComplex.homologyMap
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map
              (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X)))
            0 ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex) =
    (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) 0).map
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map
              (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X))) ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((injectiveResolutions C).obj Y).as)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ ∃ X' t, ∃ (_ : P.isoModSerre t), t ≫ f₁ = t ≫ f₂

Tactic:
refine ⟨_, kernel.ι (f₁ - f₂), ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ P.isoModSerre (kernel.ι (f₁ - f₂))

case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ kernel.ι (f₁ - f₂) ≫ f₁ = kernel.ι (f₁ - f₂) ≫ f₂
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
⊢ ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)

Tactic:
by
    apply ActionCategory.cases
    intros
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
⊢ ∀ (X Y Z : Action V G) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g

Tactic:
intros; ext; exact Linear.comp_smul _ _ _ _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasLeftDual (F.obj X)
this : ExactPairing (F.obj (G.obj ᘁ(F.obj X))) (F.obj X) :=
  exactPairingCongrLeft (adj.toEquivalence.counitIso.app ᘁ(F.obj X))
⊢ ExactPairing (G.obj ᘁ(F.obj X)) X

Tactic:
apply ExactPairing.ofFullyFaithful F

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasRightDual (F.obj X)
this : ExactPairing (F.obj X) (F.obj (G.obj (F.obj X)ᘁ)) :=
  exactPairingCongrRight (adj.toEquivalence.counitIso.app (F.obj X)ᘁ)
⊢ ExactPairing X (G.obj (F.obj X)ᘁ)

Tactic:
apply ExactPairing.ofFullyFaithful F

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝⁵ : L.Full
inst✝⁴ : L.Faithful
inst✝³ : G.Full
inst✝² : G.Faithful
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts D
⊢ Epi q.leftTriple.leftToRight ↔ Mono q.rightTriple.rightToLeft

Tactic:
by
  rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]
  exact q.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f g : a ⟶ b
hfg : f = g
⊢ f.base = g.base

Tactic:
by rw [hfg]

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
⊢ { iso := (EquivFunctor.mapEquiv m (𝟙 α).iso.toEquiv).toIso } = 𝟙 { of := m α.of }

Tactic:
ext x; exact congr_fun (EquivFunctor.map_refl' _) x

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X Y : ↑s.pt
f : X ⟶ Y
⊢ (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
have (j : _) := Functor.congr_hom congr($((w j).symm).toFunctor) f

Goal state after:
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X Y : ↑s.pt
f : X ⟶ Y
this : ∀ (j : J), (s.π.app j).toFunctor.map f = eqToHom ⋯ ≫ (m ≫ (limitCone F).π.app j).toFunctor.map f ≫ eqToHom ⋯
⊢ (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit

Goal state before:
pp: K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
this : Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))
X : K
y : (limit (F.op ⋙ coyoneda)).obj X
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
exact ⟨X, ⟨(limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) _).hom y⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
⊢ IsIso f

Tactic:
by
  have : IsIso (F.map f) := by
    apply (ConcreteCategory.isIso_iff_bijective (F.map f)).mpr
    apply (Fintype.bijective_iff_injective_and_card (F.map f)).mpr
    refine ⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩
    simp only [← Nat.card_eq_fintype_card, h]
  exact isIso_of_reflects_iso f F

Goal state after:
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).obj
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
⊢ (g * n * g⁻¹) • x = x

Tactic:
change g • n • (g⁻¹ • x) = x

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).obj
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
⊢ g • n • g⁻¹ • x = x
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
⊢ c ∈ S.objs → 𝟙 c ∈ S.arrows c c

Tactic:
rintro ⟨γ, hγ⟩
  convert! S.mul hγ (S.inv hγ)
  simp only [inv_eq_inv, IsIso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
γ₁ : c ⟶ c
x✝¹ : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
x✝ : γ₂ ∈ S.arrows c c
h : (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₂
⊢ γ₁ = γ₂

Tactic:
simpa only [inv_eq_inv, Category.assoc, IsIso.hom_inv_id, Category.comp_id,
      IsIso.hom_inv_id_assoc] using p ≫= h =≫ inv p

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p₂ ≫ f₃ = h.p₃ ≫ f₃

Tactic:
p₂₃_p₃_assoc

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₃ ≫ f₃ = h.p₃ ≫ f₃
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝¹ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, hf.incl.app b ≫ g₁ = hf.incl.app b ≫ g₂
x✝ : ↑(Set.Iio j)
k : J
hk : k ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone hf.F).ι.app ⟨k, hk⟩ ≫ hf.incl.app j ≫ g₁ =
    ((Set.principalSegIio j).cocone hf.F).ι.app ⟨k, hk⟩ ≫ hf.incl.app j ≫ g₂

Tactic:
by simpa using! hj' _ hk

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯ ≫
      ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom) =
    (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫ (sections I).map g) ≫
      ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom)

Tactic:
simp [← curry_natural_right]

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₃
this :
  X₁.right ◁ X₂.left ◁ Arrow.Hom.right f₃ ≫
      (α_ X₁.right X₂.left Y₃.right).inv ≫
        Arrow.Hom.right f₁ ▷ X₂.left ▷ Y₃.right ≫
          (α_ Y₁.right X₂.left Y₃.right).hom ≫
            Y₁.right ◁ Arrow.Hom.left f₂ ▷ Y₃.right ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) =
    X₁.right ◁ Arrow.Hom.left f₂ ▷ X₃.right ≫
      X₁.right ◁ Y₂.left ◁ Arrow.Hom.right f₃ ≫
        X₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) ≫
          Arrow.Hom.right f₁ ▷ pushout (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ 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 (((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₃))

Tactic:
by
      simp [← whisker_exchange_assoc, reassoc_of% this]

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₃
this :
  (α_ X₁.left X₂.right X₃.right).hom ≫
      X₁.left ◁ X₂.right ◁ Arrow.Hom.right f₃ ≫
        (α_ X₁.left X₂.right Y₃.right).inv ≫
          Arrow.Hom.left f₁ ▷ X₂.right ▷ Y₃.right ≫
            (α_ Y₁.left X₂.right Y₃.right).hom ≫ Y₁.left ◁ Arrow.Hom.right f₂ ▷ Y₃.right =
    Arrow.Hom.left f₁ ▷ X₂.right ▷ X₃.right ≫
      (α_ Y₁.left X₂.right X₃.right).hom ≫
        Y₁.left ◁ Arrow.Hom.right f₂ ▷ X₃.right ≫ Y₁.left ◁ Y₂.right ◁ Arrow.Hom.right f₃
⊢ (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₃))

Tactic:
by
      simp [← whisker_exchange_assoc, reassoc_of% this]

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₁} (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:
by
  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
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso (expComparison F A).natTrans

Tactic:
rw [← frobeniusMorphism_mate F h]; infer_instance

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

Goal state before:
pp: C : Type u
X : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ {X_1 Y : (Discrete ∘ NormalMonoidalObject) C} (f : X_1 ⟶ Y),
    ((tensorFunc C).obj X).map f ≫ (normalizeIsoApp C X Y).hom =
      (normalizeIsoApp C X X_1).hom ≫ ((normalize' C).obj X).map f

Tactic:
rintro ⟨X⟩ ⟨Y⟩ ⟨⟨f⟩⟩

Goal state after:
C : Type u
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X Y : NormalMonoidalObject C
f : { as := X }.as = { as := Y }.as
⊢ ((tensorFunc C).obj X✝).map { down := { down := f } } ≫ (normalizeIsoApp C X✝ { as := Y }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ ((normalize' C).obj X✝).map { down := { down := f } }
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).hom ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ (β_ A A).hom ≫
              A ◁ A ◁ A ◁ 𝒮 ≫
                A ◁ (α_ A A A).inv ≫
                  (((A ◁ (β_ A A).hom ▷ A ≫ A ◁ 𝒮 ▷ A ▷ A) ≫ A ◁ (α_ A A A).hom) ≫ (α_ A A (A ⊗ A)).inv) ≫ (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 9 10 =>
    rw [← whiskerLeft_comp, associator_naturality_left, whiskerLeft_comp]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ LinearMap.id (x, 1).1 * (Hom.hom (↟(Algebra.linearMap R ↑A))) (x, 1).2 =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑A ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)

Tactic:
ModuleCat.MonoidalCategory.rightUnitor_hom_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ LinearMap.id (x, 1).1 * (Hom.hom (↟(Algebra.linearMap R ↑A))) (x, 1).2 = 1 • x
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
X : C
⊢ IsFiltered (CostructuredArrow (ObjectProperty.isFinitelyPresentable C).ι X)

Tactic:
rw [← CategoryTheory.isCardinalFiltered_aleph0_iff.{w},
    ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
X : C
⊢ IsCardinalFiltered (CostructuredArrow (isCardinalPresentable C Cardinal.aleph0).ι X) Cardinal.aleph0
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
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
⊢ (ι C V D).map (ρ_ d).hom = (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom

Tactic:
apply corepresentableByRight
    (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.obj d) |>.homEquiv.injective

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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
⊢ (corepresentableByRight ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).homEquiv ((ι C V D).map (ρ_ d).hom) =
    (corepresentableByRight ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).homEquiv
      (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom