mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (ρ_ x✝¹).hom.unop).op =
    (αᵣ (unop x✝) (unop x✝¹) (unop (𝟙_ Cᵒᵖ))).symm.op.hom ≫ (ρᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝¹)))).symm.op.hom

Tactic:
apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

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✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (ρ_ x✝¹).hom.unop).op =
    (αᵣ (unop x✝) (unop x✝¹) (unop (𝟙_ Cᵒᵖ))).symm.op.hom ≫ (ρᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝¹)))).symm.op.hom

Tactic:
by
    apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ x ◁ y ◁ ihomUncurry x y z ≫ (α_ x y ((ihom (x ⊗ y)).obj z)).inv ≫ (ihom.ev (x ⊗ y)).app z =
    uncurry ((ihom.ev y).app ((ihom x).obj z))

Tactic:
rw [associator_inv_naturality_right_assoc, ← dsimp% uncurry_eq, uncurry_ihomUncurry]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ (α_ x y ((ihom y).obj ((ihom x).obj z))).inv ≫
      (α_ x y ((ihom y).obj ((ihom x).obj z))).hom ≫ x ◁ (ihom.ev y).app ((ihom x).obj z) ≫ (ihom.ev x).app z =
    uncurry ((ihom.ev y).app ((ihom x).obj z))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c j : C
⊢ Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      ℌ.π c j =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c))

Tactic:
← Wedge.mk_ι
      (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
      (H.obj c) (ℌ.π c) (ℌ.hπ c),

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
inst✝¹ : MonoidalClosed V
F H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c j : C
⊢ Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A) =
    (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom

Tactic:
ext : 1
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `TensorProduct.ext`
    refine TensorProduct.ext <| LinearMap.ext fun x => LinearMap.ext_ring ?_
    -- Porting note: this `dsimp` does nothing
    -- dsimp only [AlgCat.id_apply, TensorProduct.mk_apply, Algebra.linearMap_apply,
    --   LinearMap.compr₂_apply, Function.comp_apply, ModuleCat.MonoidalCategory.hom_apply,
    --   AlgCat.coe_comp]
    -- Porting note: because `dsimp` is not effective, `rw` needs to be changed to `erw`
    erw [compr₂_apply, compr₂ₛₗ_apply]
    simp only [hom_comp, hom_ofHom, id_coe, id_eq, LinearMap.comp_apply]
    erw [LinearMap.mul'_apply, ModuleCat.MonoidalCategory.rightUnitor_hom_apply, ← Algebra.commutes,
      ← Algebra.smul_def]
    dsimp

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 : Mon C
P : Bimod R S
⊢ μ ▷ P.X ≫ P.actLeft = (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft

Tactic:
left_assoc

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 : Mon C
P : Bimod R S
⊢ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft = (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft
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 : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actLeft (regular R) P ≫ hom P = R.X ◁ hom P ≫ P.actLeft

Tactic:
dsimp [hom, TensorBimod.actLeft, regular]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((PreservesCoequalizer.iso (tensorLeft R.X) (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
        colimMap
          (parallelPairHom (R.X ◁ μ ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (μ ▷ P.X)
            ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
            ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ μ ▷ R.X ▷ P.X) ((α_ R.X R.X P.X).inv ≫ μ ▷ P.X)
            ⋯ ⋯)) ≫
      coequalizer.desc P.actLeft ⋯ =
    R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| μ ▷ P.X ≫ P.actLeft

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

Tactic:
left_assoc

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

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
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.X R.X P.X).inv
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 : Mon C
P : Bimod R S
⊢ hom P ≫ inv P = 𝟙 (TensorBimod.X P (regular S))

Tactic:
by
  dsimp only [hom, inv, TensorBimod.X]
  ext; dsimp
  slice_lhs 1 2 => rw [coequalizer.π_desc]
  slice_lhs 1 2 => rw [rightUnitor_inv_naturality]
  slice_lhs 2 3 => rw [← whisker_exchange]
  slice_lhs 3 4 => rw [coequalizer.condition]
  slice_lhs 2 3 => rw [associator_naturality_right]
  slice_lhs 3 4 => rw [← whiskerLeft_comp, MonObj.mul_one]
  slice_rhs 1 2 => rw [Category.comp_id]
  monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actLeft P (regular S) ≫ hom P = R.X ◁ hom P ≫ P.actLeft

Tactic:
dsimp [hom, TensorBimod.actLeft, regular]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((PreservesCoequalizer.iso (tensorLeft R.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)).inv ≫
        colimMap
          (parallelPairHom (R.X ◁ P.actRight ▷ S.X) (R.X ◁ ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)) (P.actRight ▷ S.X)
            ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
            ((α_ R.X (P.X ⊗ S.X) S.X).inv ≫ (α_ R.X P.X S.X).inv ▷ S.X ≫ P.actLeft ▷ S.X ▷ S.X)
            ((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ⋯ ⋯)) ≫
      coequalizer.desc P.actRight ⋯ =
    R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
⊢ P.ind X ↔ ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W

Tactic:
refine ⟨fun ⟨J, _, _, pres, h⟩ Z g hZ ↦ ?_, fun hfac ↦ ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
x✝ : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable Z
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J X
h : ∀ (i : J), P (pres.diag.obj i)
⊢ ∃ W u v, u ≫ v = g ∧ P W

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
⊢ P.ind X
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₂'
⊢ (ι C V D).map (f ⊗ₘ f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')

Tactic:
dsimp +instances [mkMonoidalCategoryStruct]

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✝⁴ : 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₂'
⊢ (ι C V D).map (tensorHom f f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsArtinianObject X ↔ ∀ (f : ℕ → Subobject X), ¬StrictAnti f

Tactic:
refine ⟨fun _ ↦ not_strictAnti_of_wellFoundedLT, fun h ↦ ?_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictAnti f
⊢ IsArtinianObject X
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsNoetherianObject X ↔ ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
dsimp only [IsNoetherianObject]
  rw [ObjectProperty.is_iff, isNoetherianObject,
    wellFoundedGT_iff_monotone_chain_condition]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsNoetherianObject X ↔ ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F

Tactic:
isNoetherianObject_iff_monotone_chain_condition

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ (∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔
    ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
⊢ IsNoetherianObject X

Tactic:
isNoetherianObject_iff_monotone_chain_condition

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
⊢ ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsNoetherianObject Y
⊢ IsNoetherianObject X

Tactic:
isNoetherianObject_iff_monotone_chain_condition

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsNoetherianObject Y
⊢ ∀ (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)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ whiskerRight f (N.tensorBimod P) =
    (M.associatorBimod N P).inv ≫ whiskerRight (whiskerRight f N) P ≫ (M'.associatorBimod N P).hom

Tactic:
dsimp [tensorHom, tensorBimod, associatorBimod]
  ext
  apply coequalizer.hom_ext
  dsimp
  slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
  dsimp [TensorBimod.X, AssociatorBimod.inv]
  slice_rhs 1 2 => rw [coequalizer.π_desc]
  dsimp [AssociatorBimod.invAux, AssociatorBimod.hom]
  refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
  simp only [curriedTensor_obj_map]
  slice_rhs 1 3 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
  slice_rhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
  slice_rhs 2 3 => rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one]
  slice_rhs 3 4 => rw [coequalizer.π_desc]
  dsimp [AssociatorBimod.homAux]
  slice_rhs 2 2 => rw [comp_whiskerRight]
  slice_rhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
  slice_rhs 2 3 => rw [associator_naturality_left]
  slice_rhs 1 3 => rw [Iso.inv_hom_id_assoc]
  slice_lhs 1 2 => rw [whisker_exchange]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : ∀ (a : X ≅ Y), False
f : X ⟶ Y
⊢ f = 0

Tactic:
have p := not_congr (isIso_iff_nonzero f)

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : ∀ (a : X ≅ Y), False
f : X ⟶ Y
p : ¬IsIso f ↔ ¬f ≠ 0
⊢ f = 0
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
by
  obtain (h | h) := subsingleton_or_nontrivial (X ⟶ Y)
  · rw [finrank_zero_of_subsingleton]
    exact zero_le_one
  · obtain ⟨f, nz⟩ := (nontrivial_iff_exists_ne 0).mp h
    have fi := (isIso_iff_nonzero f).mpr nz
    refine finrank_le_one f ?_
    intro g
    obtain ⟨c, w⟩ := endomorphism_simple_eq_smul_id 𝕜 (g ≫ inv f)
    exact ⟨c, by simpa using w =≫ f⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ ∑ x, ∑ x_1, f i✝ x_1 ≫ g x_1 x ≫ h x j✝ = ∑ x, ∑ j, f i✝ x ≫ g x j ≫ h j j✝

Tactic:
rw [Finset.sum_comm]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
x✝ : IsIso (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g₁ g₂ : Y ⟶ Z
h : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
⊢ f ≫ g₁ ≫ toStep W Z = f ≫ g₂ ≫ toStep W Z

Tactic:
simp [reassoc_of% h]

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

Goal state before:
pp: case refine_2
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).P ≤ D₂'.P

Tactic:
exact le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left

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

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ ∃ α x, ∃ (_ : IsCardinalFiltered α κ), ∃ F, F.Final

Tactic:
by
  have := isFiltered_of_isCardinalFiltered κ.ord.ToType κ
  obtain ⟨α, _, _, F, _⟩ :=
    exists_cardinal_directed.aux (J × κ.ord.ToType) κ (fun ⟨j, x⟩ ↦
      ⟨⟨j, Order.succ x⟩, (𝟙 _, homOfLE (Order.le_succ x)), ⟨fun ⟨_, f⟩ ↦ by
        have : NoMaxOrder κ.ord.ToType :=
          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
        exact not_isMax _ (Order.max_of_succ_le (leOfHom f))⟩⟩)
  exact ⟨_, _, inferInstance, F ⋙ Prod.fst _ _, inferInstance⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (coherentTopology D)) X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
rw [mem_inducedTopology_iff_of_isCoverDense] at hS

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj X)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁶ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁵ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁴ : ConcreteCategory A FA
inst✝³ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝² : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝¹ : HasWeakSheafify J A
f : Arrow (Sheaf J A)
inst✝ : J.HasSheafCompose (forget A)
⊢ Mono ((functorialLocallySurjectiveInjectiveFactorization J data).p.app f)

Tactic:
by
  apply mono_of_isLocallyInjective

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (regularTopology D)) X
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
rw [mem_inducedTopology_iff_of_isCoverDense] at hS

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₂.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).inv) =
    (e i₁).inv ≫ D₁.hom i₁ i₂

Tactic:
rw [← cancel_epi (e i₁).hom, ← reassoc_of% (comm i₁ i₂), ← Functor.map_comp, ← Functor.map_comp]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ f₁ ≫ f i₁ = f₂ ≫ f i₂

Tactic:
by rw [hf₁, hf₂]

Goal state after: