mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
j : J
x✝¹ : R
x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝

Tactic:
simp

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
j : J
x✝¹ : R
x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ ↑(x✝¹ • (equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j =
    x✝¹ • ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_1.e_a
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
j : J
⊢ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) 1 = 1 j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
x y : ↑s.1
j : J
⊢ ↑((equivShrink ↑(F ⋙ forget (AlgCat R)).sections).symm
          (EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
            ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x * y), ⋯⟩))
      j =
    ↑((equivShrink ↑(F ⋙ forget (AlgCat R)).sections).symm
          (EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
              ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ *
            EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
              ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩))
      j

Tactic:
simp

Goal state after:
case refine_2
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
x y : ↑s.1
j : J
⊢ (ConcreteCategory.hom (s.π.app j)) x * (ConcreteCategory.hom (s.π.app j)) y =
    ↑(⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ * ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩) j
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_3
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
j : J
⊢ ↑((equivShrink ↑(F ⋙ forget (AlgCat R)).sections).symm
          (EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
            ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) 0, ⋯⟩))
      j =
    ↑((equivShrink ↑(F ⋙ forget (AlgCat R)).sections).symm 0) j

Tactic:
simp

Goal state after:
case refine_3
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
j : J
⊢ 0 = ↑0 j
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_4
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
x y : ↑s.1
j : J
⊢ ↑((equivShrink ↑(F ⋙ forget (AlgCat R)).sections).symm
          (EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
            ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x + y), ⋯⟩))
      j =
    ↑((equivShrink ↑(F ⋙ forget (AlgCat R)).sections).symm
          (EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
              ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ +
            EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
              ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩))
      j

Tactic:
simp

Goal state after:
case refine_4
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
x y : ↑s.1
j : J
⊢ (ConcreteCategory.hom (s.π.app j)) x + (ConcreteCategory.hom (s.π.app j)) y =
    ↑(⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ + ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩) j
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
g g' : ↑(limit.cone (parallelPair f 0)).1
⊢ ↑⟨(ConcreteCategory.hom (kernel.ι f)) (g + g'), ⋯⟩ =
    ↑(⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩ + ⟨(ConcreteCategory.hom (kernel.ι f)) g', ⋯⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ (Hom.hom
        ((ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } ≫
            kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯) ≫
          equalizer.ι f 0))
      x✝ =
    (Hom.hom (𝟙 (kernel f) ≫ equalizer.ι f 0)) x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (𝟙_ C ◁ f ≫ (λ_ Y).hom) ≫ (λ_ Y).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ₘ f = (((𝟙 X ⊗ₘ 𝟙 Y) ⊗ₘ f) ≫ (α_ X Y Z').hom) ≫ (α_ X Y Z').inv

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ▷ 𝟙_ C = (f ▷ 𝟙_ C ≫ (ρ_ Y).hom) ≫ (ρ_ Y).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ f ⊗ₘ 𝟙 (Y ⊗ Z) = (α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ (f ⊗ₘ 𝟙 Y ⊗ₘ 𝟙 Z)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z = (((𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z) ≫ (α_ X Y' Z).hom) ≫ (α_ X Y' Z).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ f ▷ Y ▷ Z = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom = (α_ X Y Z).hom ≫ X ◁ f ▷ Z

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ X ◁ f ▷ Z ≫ (α_ X Y' Z).inv = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ X ◁ f ▷ Z = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ X ◁ Y ◁ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ X ◁ Y ◁ f ≫ (α_ X Y Z').inv = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ X ◁ Y ◁ f = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ≫ (λ_ Y).inv = (λ_ X).inv ≫ 𝟙_ C ◁ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
⊢ f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ f ▷ 𝟙_ C

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f = (ρ_ X).inv ≫ f ▷ 𝟙_ C ≫ (ρ_ Y).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ 𝟙_ C ◁ f = 𝟙_ C ◁ g ↔ f = g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ f ▷ 𝟙_ C = g ▷ 𝟙_ C ↔ f = g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv (W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z) =
    inv ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom) ≫ (α_ (W ⊗ X) Y Z).inv =
    (W ◁ (α_ X Y Z).inv ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv) ≫ (α_ (W ⊗ X) Y Z).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom) =
    inv ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv) =
    inv ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ ((α_ W X (Y ⊗ Z)).inv ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv) ≫ (α_ W X Y).inv ▷ Z =
    ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z) ≫ (α_ W X Y).inv ▷ Z

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv) =
    inv ((α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z) =
    inv (W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ inv ((λ_ X).inv ▷ Y) = inv ((λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ inv (X ◁ (ρ_ Y).inv) = inv ((ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ (λ_ X).hom ▷ Y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).inv = (λ_ X).inv ▷ Y ≫ (α_ (𝟙_ C) X Y).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ X ◁ (ρ_ Y).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ (X ⊗ Y)).inv = X ◁ (ρ_ Y).inv ≫ (α_ X Y (𝟙_ C)).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f.hom ⊗ₘ g) ≫ (f.inv ⊗ₘ h) = (𝟙 V ⊗ₘ g) ≫ (𝟙 V ⊗ₘ h)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f.inv ⊗ₘ g) ≫ (f.hom ⊗ₘ h) = (𝟙 W ⊗ₘ g) ≫ (𝟙 W ⊗ₘ h)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ₘ f.hom) ≫ (h ⊗ₘ f.inv) = (g ⊗ₘ 𝟙 V) ≫ (h ⊗ₘ 𝟙 V)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ₘ f.inv) ≫ (h ⊗ₘ f.hom) = (g ⊗ₘ 𝟙 W) ≫ (h ⊗ₘ 𝟙 W)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ⊗ₘ g) ≫ (inv f ⊗ₘ h) = (𝟙 V ⊗ₘ g) ≫ (𝟙 V ⊗ₘ h)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (inv f ⊗ₘ g) ≫ (f ⊗ₘ h) = (𝟙 W ⊗ₘ g) ≫ (𝟙 W ⊗ₘ h)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ₘ f) ≫ (h ⊗ₘ inv f) = (g ⊗ₘ 𝟙 V) ≫ (h ⊗ₘ 𝟙 V)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ₘ inv f) ≫ (h ⊗ₘ f) = (g ⊗ₘ 𝟙 W) ≫ (h ⊗ₘ 𝟙 W)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ f ≫ g ⊗ₘ 𝟙 Z = (f ⊗ₘ 𝟙 Z) ≫ (g ⊗ₘ 𝟙 Z)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ₘ f ≫ g = (𝟙 Z ⊗ₘ f) ≫ (𝟙 Z ⊗ₘ g)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ 𝟙 (𝟙_ C) ⊗ₘ f = 𝟙 (𝟙_ C) ⊗ₘ g ↔ f = g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ f ⊗ₘ 𝟙 (𝟙_ C) = g ⊗ₘ 𝟙 (𝟙_ C) ↔ f = g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z✝ X Y Z Z' : C
f : Z ⟶ Z'
⊢ (tensorLeft (X ⊗ Y)).map f ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (tensorLeft Y ⋙ tensorLeft X).map f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z✝ X Y Z Z' : C
f : Z ⟶ Z'
⊢ (tensorRight (X ⊗ Y)).map f ≫ (α_ Z' X Y).symm.hom = (α_ Z X Y).symm.hom ≫ (tensorRight X ⋙ tensorRight Y).map f

Tactic:
simp

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y X' Y' : J
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (F.map f ⊗ₘ G.map g) ≫ (α.app Y ⊗ₘ β.app Y') = (α.app X ⊗ₘ β.app X') ≫ (F'.map f ⊗ₘ G'.map g)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) 1, ⋯⟩ =
    1

Tactic:
simp

Goal state after:
case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ (equivShrink ↑(F ⋙ forget SemiRingCat).sections) ⟨fun j ↦ 1, ⋯⟩ = 1
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        (α_ (F.obj W) (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj X ⊗ F.obj Y) (F.obj Z)).hom ≫
            (((F.obj W ◁ 𝟙 ((F.obj X ⊗ F.obj Y) ⊗ F.obj Z) ≫ F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom) ≫
                F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom) ≫
              (fData.μIso W (X ⊗ Y ⊗ Z)).hom =
    (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (α_ (F.obj (W ⊗ X)) (F.obj Y) (F.obj Z)).hom ≫
        (fData.μIso W X).inv ▷ (F.obj Y ⊗ F.obj Z) ≫
          (F.obj W ⊗ F.obj X) ◁ (fData.μIso Y Z).hom ≫
            (α_ (F.obj W) (F.obj X) (F.obj (Y ⊗ Z))).hom ≫
              F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom ≫ (fData.μIso W (X ⊗ Y ⊗ Z)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: case refine_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) 0, ⋯⟩ =
    0

Tactic:
simp

Goal state after:
case refine_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ (equivShrink ↑(F ⋙ forget SemiRingCat).sections) ⟨fun j ↦ 0, ⋯⟩ = 0
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
⊢ r • f = (r • 𝟙 X) ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : Linear R C
inst✝¹ : Linear R D
F : C ⥤ D
e : C ≌ D
inst✝ : Functor.Linear R e.functor
X✝ Y✝ : D
r : X✝ ⟶ Y✝
f : R
⊢ e.functor.map (e.inverse.map (f • r)) = e.functor.map (f • e.inverse.map r)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ Functor.OplaxMonoidal.δ F X Y ≫ F.obj X ◁ F.map (r • f) ≫ Functor.LaxMonoidal.μ F X Z = F.map (r • X ◁ f)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ Functor.OplaxMonoidal.δ F X Z ≫ F.map (r • f) ▷ F.obj Z ≫ Functor.LaxMonoidal.μ F Y Z = F.map (r • f ▷ Z)

Tactic:
simp

Goal state after:
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 Y : C
f : J → C
val✝ : Fintype J
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x,
        if h : x = j✝ then (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ biproduct.π f x) ≫ (𝟙 X ⊗ₘ eqToHom ⋯)
        else (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ biproduct.π f x) ≫ (𝟙 X ⊗ₘ 0)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ₘ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0

Tactic:
simp

Goal state after:
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
f : J → C
X Y : C
val✝ : Fintype J
j✝ : J
⊢ (∑ x, if h : x = j✝ then (biproduct.π f x ⊗ₘ 𝟙 X) ≫ eqToHom ⋯ ⊗ₘ 𝟙 Y else (biproduct.π f x ⊗ₘ 𝟙 X) ≫ 0 ⊗ₘ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ₘ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv

Tactic:
simp

Goal state after: