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

Goal state before:
pp: case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x,
      (X ◁ biproduct.π f x ⊗ₘ 𝟙 Y) ≫
        (biproduct.ι (fun j ↦ X ⊗ f j) x ⊗ₘ 𝟙 Y) ≫ (biproduct.π (fun j ↦ X ⊗ f j) j✝ ⊗ₘ 𝟙 Y) =
    ∑ x,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ biproduct.ι (fun j ↦ f j ⊗ Y) x) ≫
          X ◁ biproduct.π (fun j ↦ f j ⊗ Y) j✝ ≫ (α_ X (f j✝) Y).inv

Tactic:
← id_tensorHom

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x,
      ((𝟙 X ⊗ₘ biproduct.π f x) ⊗ₘ 𝟙 Y) ≫
        (biproduct.ι (fun j ↦ X ⊗ f j) x ⊗ₘ 𝟙 Y) ≫ (biproduct.π (fun j ↦ X ⊗ f j) j✝ ⊗ₘ 𝟙 Y) =
    ∑ x,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ biproduct.ι (fun j ↦ f j ⊗ Y) x) ≫
          (𝟙 X ⊗ₘ biproduct.π (fun j ↦ f j ⊗ Y) j✝) ≫ (α_ X (f j✝) Y).inv
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y : SemimoduleCat R
f : X ⟶ Y
Z : SemimoduleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ Z ◁ f

Tactic:
← id_tensorHom

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y : SemimoduleCat R
f : X ⟶ Y
Z : SemimoduleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ (𝟙 Z ⊗ₘ f)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
f : Y ⟶ Z
⊢ X ◁ f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X

Tactic:
← id_tensorHom

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
f : Y ⟶ Z
⊢ (𝟙 X ⊗ₘ f) ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Epi ((forget C).map f)

Tactic:
epi_iff_surjective

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (adj.homEquiv (X✝ ⊗ x✝) (F.obj X✝ ⊗ F.obj x✝)).symm
        ((adj.unit.app X✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj X✝) (F.obj x✝)) ≫
      F.map x✝¹ ▷ F.obj x✝ =
    F.map (x✝¹ ▷ x✝) ≫
      (adj.homEquiv (Y✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
        ((adj.unit.app Y✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj Y✝) (F.obj x✝))

Tactic:
← Adjunction.homEquiv_naturality_right_symm,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      (((adj.unit.app X✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj X✝) (F.obj x✝)) ≫ G.map (F.map x✝¹ ▷ F.obj x✝)) =
    F.map (x✝¹ ▷ x✝) ≫
      (adj.homEquiv (Y✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
        ((adj.unit.app Y✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj Y✝) (F.obj x✝))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj X✝)).symm
        ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app X✝) ≫ μ G (F.obj x✝¹) (F.obj X✝)) ≫
      F.obj x✝¹ ◁ F.map x✝ =
    F.map (x✝¹ ◁ x✝) ≫
      (adj.homEquiv (x✝¹ ⊗ Y✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
        ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app Y✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝))

Tactic:
← Adjunction.homEquiv_naturality_right_symm,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      (((adj.unit.app x✝¹ ⊗ₘ adj.unit.app X✝) ≫ μ G (F.obj x✝¹) (F.obj X✝)) ≫ G.map (F.obj x✝¹ ◁ F.map x✝)) =
    F.map (x✝¹ ◁ x✝) ≫
      (adj.homEquiv (x✝¹ ⊗ Y✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
        ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app Y✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
⊢ (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      ((adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj (X ⊗ Y) ⊗ F.obj Z)).symm
          ((adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
        (adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      (F.map (α_ X Y Z).hom ≫
        (adj.homEquiv (X ⊗ Y ⊗ Z) (F.obj X ⊗ F.obj (Y ⊗ Z))).symm
            ((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
          F.obj X ◁
            (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))

Tactic:
← Adjunction.homEquiv_naturality_right_symm,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
⊢ (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      ((adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z)).symm
        (((adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
          G.map
            ((adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm
                  ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
                F.obj Z ≫
              (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom))) =
    (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      (F.map (α_ X Y Z).hom ≫
        (adj.homEquiv (X ⊗ Y ⊗ Z) (F.obj X ⊗ F.obj (Y ⊗ Z))).symm
            ((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
          F.obj X ◁
            (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
⊢ (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      ((adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z)).symm
        (((adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
          G.map
            ((adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm
                  ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
                F.obj Z ≫
              (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom))) =
    (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      (F.map (α_ X Y Z).hom ≫
        (adj.homEquiv (X ⊗ Y ⊗ Z) (F.obj X ⊗ F.obj (Y ⊗ Z))).symm
            ((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
          F.obj X ◁
            (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))

Tactic:
← Adjunction.homEquiv_naturality_right_symm,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
⊢ (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      ((adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z)).symm
        (((adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
          G.map
            ((adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm
                  ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
                F.obj Z ≫
              (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom))) =
    (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      (F.map (α_ X Y Z).hom ≫
        (adj.homEquiv (X ⊗ Y ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z)).symm
          (((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
            G.map
              (F.obj X ◁
                (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
                  ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (X ⊗ Y) ▷ G.obj Z ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ i.hom.app (X ⊗ Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z)

Tactic:
simp only [← Category.assoc]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ ((((((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫ LaxMonoidal.μ F X Y ▷ G.obj Z) ≫ i.hom.app (X ⊗ Y) ▷ G.obj Z) ≫
            (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z)) ≫
          LaxMonoidal.μ F (X ⊗ Y) Z) ≫
        F.map (α_ X Y Z).hom) ≫
      i.hom.app (X ⊗ Y ⊗ Z) =
    ((((((α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
              G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
            G.obj X ◁ i.hom.app (Y ⊗ Z)) ≫
          (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z))) ≫
        LaxMonoidal.μ F X (Y ⊗ Z)) ≫
      i.hom.app (X ⊗ Y ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫ tensorμ Y₁ Y₂ V₁ V₂ = tensorμ X₁ X₂ U₁ U₂ ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)

Tactic:
dsimp only [tensorμ]
  simp_rw [← id_tensorHom, ← tensorHom_id]
  slice_lhs 1 2 => rw [associator_naturality]
  slice_lhs 2 3 =>
    rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_inv_naturality,
      ← tensorHom_comp_tensorHom]
  slice_lhs 3 4 =>
    rw [tensorHom_comp_tensorHom, tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, comp_id g₂,
      ← id_comp g₂, braiding_naturality, ← tensorHom_comp_tensorHom, ← tensorHom_comp_tensorHom]
  slice_lhs 4 5 =>
    rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_naturality,
      ← tensorHom_comp_tensorHom]
  slice_lhs 5 6 => rw [associator_inv_naturality]
  simp only [assoc]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
⊢ (⅟x).fst = ⅟x.fst

Tactic:
by
  let := invertibleFstOfInvertible x
  convert! (rfl : _ = ⅟x.fst)

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹³ : CommSemiring S
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra S R
inst✝⁸ : Module S M
inst✝⁷ : Module R M
inst✝⁶ : Module Rᵐᵒᵖ M
inst✝⁵ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁴ : IsScalarTower S R M
inst✝³ : IsScalarTower S Rᵐᵒᵖ M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (algebraMap S R) s •> x.snd = x.snd <• (algebraMap S R) s

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹³ : CommSemiring S
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra S R
inst✝⁸ : Module S M
inst✝⁷ : Module R M
inst✝⁶ : Module Rᵐᵒᵖ M
inst✝⁵ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁴ : IsScalarTower S R M
inst✝³ : IsScalarTower S Rᵐᵒᵖ M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (s •> 1) •> x.snd = x.snd <• s •> 1
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
⊢ comul ∘ₗ coeFnLinearMap R = map (coeFnLinearMap R) (coeFnLinearMap R) ∘ₗ comul

Tactic:
apply LinearMap.ext fun x ↦ ?_
  have (i : n) (x : A i) : Decidable (x ≠ 0) := Classical.propDecidable _
  rw [← DFinsupp.sum_single (f := x)]
  aesop (add simp [map_map, DFinsupp.single_eq_pi_single])

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
⊢ { toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction f,
          invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction f, left_inv := ⋯, right_inv := ⋯ }.symm
      g =
    (restrictScalars f).map g ≫ (RestrictionCoextensionAdj.counit' f).app Y

Tactic:
ext
      simp [RestrictionCoextensionAdj.counit']

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_3
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ ∀ (m : S) (x : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (m • x) =
      (RingHom.id S) m • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x

Tactic:
intro s

Goal state after:
case refine_3
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
⊢ ∀ (x : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • x) =
      (RingHom.id S) s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
X✝ Y✝ : Comon C
f : X✝ ⟶ Y✝
⊢ η ≫ f.hom.op = η

Tactic:
by apply Quiver.Hom.unop_inj; simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
X✝ Y✝ : Comon C
f : X✝ ⟶ Y✝
⊢ μ ≫ f.hom.op = (f.hom.op ⊗ₘ f.hom.op) ≫ μ

Tactic:
by apply Quiver.Hom.unop_inj; simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → x ∈ span s → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : x ∈ span s), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : x ∈ span s), p x hx → p (x * b) ⋯
x✝ : R
hx✝ : x✝ ∈ span s
J : TwoSidedIdeal R := mk' {x | ∃ (hx : x ∈ span s), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x : R
hx : x ∈ s
⊢ x - 0 ∈ span s

Tactic:
by simpa using (mem_span_iff.2 fun I a ↦ a hx)

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
⊢ Monotone fun I ↦ { ringCon := I.ringCon.comap f }

Tactic:
intro I

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I : TwoSidedIdeal S
⊢ ∀ ⦃b : TwoSidedIdeal S⦄,
    I ≤ b → (fun I ↦ { ringCon := I.ringCon.comap f }) I ≤ (fun I ↦ { ringCon := I.ringCon.comap f }) b
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x : Rᵐᵒᵖ
⊢ x ∈ asIdealOpposite I ↔ MulOpposite.unop x ∈ I

Tactic:
simpa [asIdealOpposite, asIdeal, TwoSidedIdeal.mem_iff, RingCon.op_iff] using
    ⟨I.ringCon.symm, I.ringCon.symm⟩

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ I.jacobson
⊢ ∀ ⦃I : Ideal R⦄, I ∈ M → x ∈ I

Tactic:
intro I

Goal state after:
case mpr
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
⊢ I ∈ M → x ∈ I
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
hM : ⊥.IsMaximal
⊢ False

Tactic:
exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero))

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
⊢ ∀ (s : S) (n : ℕ), ∃ c l m k, f (a ^ (k + n) * c) = f (a ^ (k + l) * b ^ m) * s

Tactic:
intro s

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
⊢ ∀ (n : ℕ), ∃ c l m k, f (a ^ (k + n) * c) = f (a ^ (k + l) * b ^ m) * s
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J

Tactic:
intro I

Goal state after:
case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
⊢ ∀ (x : R), maximalIdeal R ≤ I → x ∉ maximalIdeal R → x ∈ I → 1 ∈ I
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g

Tactic:
have := hI.isIso_to g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this✝ : IsIso f
this : IsIso g
⊢ f = g
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
⊢ f = g

Tactic:
by
  have := hI.isIso_to f
  have := hI.isIso_to g
  exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ selfZPow x B ↑(n - m) * (algebraMap R B) (x ^ m) = (algebraMap R B) (x ^ n)

Tactic:
selfZPow_natCast,

Goal state after:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ (algebraMap R B) x ^ (n - m) * (algebraMap R B) (x ^ m) = (algebraMap R B) (x ^ n)