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

Goal state before:
pp: 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✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).hom = ∑ j, X ◁ biproduct.π f j ≫ biproduct.ι (fun j ↦ X ⊗ f j) j

Tactic:
ext

Goal state after:
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✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝ =
    (∑ j, X ◁ biproduct.π f j ≫ biproduct.ι (fun j ↦ X ⊗ f j) j) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: 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✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).inv = ∑ j, biproduct.π (fun j ↦ X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Tactic:
ext

Goal state after:
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✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ (leftDistributor X f).inv =
    biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ ∑ j, biproduct.π (fun j ↦ X ⊗ f j) j ≫ X ◁ biproduct.ι f j
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
⊢ ((asIso (𝟙 X) ⊗ᵢ leftDistributor Y f) ≪≫ leftDistributor X fun j ↦ Y ⊗ f j) =
    (α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun x ↦ α_ X Y (f x)

Tactic:
ext

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 Y : C
f : J → C
val✝ : Fintype J
j✝ : J
⊢ ((asIso (𝟙 X) ⊗ᵢ leftDistributor Y f) ≪≫ leftDistributor X fun j ↦ Y ⊗ f j).hom ≫
      biproduct.π (fun j ↦ X ⊗ Y ⊗ f j) j✝ =
    ((α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun x ↦ α_ X Y (f x)).hom ≫
      biproduct.π (fun j ↦ X ⊗ Y ⊗ f j) j✝
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: 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✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).hom = ∑ j, biproduct.π f j ▷ X ≫ biproduct.ι (fun j ↦ f j ⊗ X) j

Tactic:
ext

Goal state after:
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✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j ↦ f j ⊗ X) j✝ =
    (∑ j, biproduct.π f j ▷ X ≫ biproduct.ι (fun j ↦ f j ⊗ X) j) ≫ biproduct.π (fun j ↦ f j ⊗ X) j✝
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: 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✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).inv = ∑ j, biproduct.π (fun j ↦ f j ⊗ X) j ≫ biproduct.ι f j ▷ X

Tactic:
ext

Goal state after:
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✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.ι (fun j ↦ f j ⊗ X) j✝ ≫ (rightDistributor f X).inv =
    biproduct.ι (fun j ↦ f j ⊗ X) j✝ ≫ ∑ j, biproduct.π (fun j ↦ f j ⊗ X) j ≫ biproduct.ι f j ▷ X
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
⊢ (rightDistributor f X ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ f j ⊗ X) Y =
    α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ (f x) X Y).symm

Tactic:
ext

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
f : J → C
X Y : C
val✝ : Fintype J
j✝ : J
⊢ ((rightDistributor f X ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ f j ⊗ X) Y).hom ≫
      biproduct.π (fun j ↦ (f j ⊗ X) ⊗ Y) j✝ =
    (α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ (f x) X Y).symm).hom ≫
      biproduct.π (fun j ↦ (f j ⊗ X) ⊗ Y) j✝
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
⊢ (leftDistributor X f ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ X ⊗ f j) Y =
    α_ X (⨁ f) Y ≪≫
      (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y) ≪≫
        (leftDistributor X fun j ↦ f j ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ X (f x) Y).symm

Tactic:
ext

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
⊢ ((leftDistributor X f ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ X ⊗ f j) Y).hom ≫
      biproduct.π (fun j ↦ (X ⊗ f j) ⊗ Y) j✝ =
    (α_ X (⨁ f) Y ≪≫
          (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y) ≪≫
            (leftDistributor X fun j ↦ f j ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ X (f x) Y).symm).hom ≫
      biproduct.π (fun j ↦ (X ⊗ f j) ⊗ Y) j✝
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
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h
val✝ : Fintype J
⊢ (leftDistributor X f).inv ≫ g = (leftDistributor X f).inv ≫ h

Tactic:
ext

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 Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h
val✝ : Fintype J
j✝ : J
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ g =
    biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ h
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
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j
val✝ : Fintype J
⊢ g ≫ (leftDistributor Y f).hom = h ≫ (leftDistributor Y f).hom

Tactic:
ext

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 Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j
val✝ : Fintype J
j✝ : J
⊢ (g ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j ↦ Y ⊗ f j) j✝ =
    (h ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j ↦ Y ⊗ f j) j✝
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: 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 Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h
⊢ (α_ X Y (⨁ f)).hom ≫ g = (α_ X Y (⨁ f)).hom ≫ h

Tactic:
ext

Goal state after:
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 Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h
j✝ : J
⊢ (X ⊗ Y) ◁ biproduct.ι f j✝ ≫ (α_ X Y (⨁ f)).hom ≫ g = (X ⊗ Y) ◁ biproduct.ι f j✝ ≫ (α_ X Y (⨁ f)).hom ≫ h
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: 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 Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
⊢ g ≫ (α_ Y Z (⨁ f)).inv = h ≫ (α_ Y Z (⨁ f)).inv

Tactic:
ext

Goal state after:
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 Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
j✝ : J
⊢ (g ≫ (α_ Y Z (⨁ f)).inv) ≫ (Y ⊗ Z) ◁ biproduct.π f j✝ = (h ≫ (α_ Y Z (⨁ f)).inv) ≫ (Y ⊗ Z) ◁ biproduct.π f j✝
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
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
val✝ : Fintype J
⊢ (rightDistributor f X).inv ≫ g = (rightDistributor f X).inv ≫ h

Tactic:
ext

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
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
val✝ : Fintype J
j✝ : J
⊢ biproduct.ι (fun j ↦ f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g =
    biproduct.ι (fun j ↦ f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h
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
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
val✝ : Fintype J
⊢ g ≫ (rightDistributor f Y).hom = h ≫ (rightDistributor f Y).hom

Tactic:
ext

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
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
val✝ : Fintype J
j✝ : J
⊢ (g ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j ↦ f j ⊗ Y) j✝ =
    (h ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j ↦ f j ⊗ Y) j✝
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: 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 Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
⊢ (α_ (⨁ f) X Y).inv ≫ g = (α_ (⨁ f) X Y).inv ≫ h

Tactic:
ext

Goal state after:
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 Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
j✝ : J
⊢ biproduct.ι f j✝ ▷ (X ⊗ Y) ≫ (α_ (⨁ f) X Y).inv ≫ g = biproduct.ι f j✝ ▷ (X ⊗ Y) ≫ (α_ (⨁ f) X Y).inv ≫ h
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: 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 Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
⊢ g ≫ (α_ (⨁ f) Y Z).hom = h ≫ (α_ (⨁ f) Y Z).hom

Tactic:
ext

Goal state after:
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 Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
j✝ : J
⊢ (g ≫ (α_ (⨁ f) Y Z).hom) ≫ biproduct.π f j✝ ▷ (Y ⊗ Z) = (h ≫ (α_ (⨁ f) Y Z).hom) ≫ biproduct.π f j✝ ▷ (Y ⊗ Z)
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : p ⊗ f₁ ≅ pf₁
η_g₁ : p ⊗ g₁ ≅ pf₁
η_f₂ : pf₁ ⊗ f₂ ≅ pf₁f₂
η_g₂ : pf₁ ⊗ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ (η ⊗ᵢ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂

Tactic:
tensorIso_def

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : p ⊗ f₁ ≅ pf₁
η_g₁ : p ⊗ g₁ ≅ pf₁
η_f₂ : pf₁ ⊗ f₂ ≅ pf₁f₂
η_g₂ : pf₁ ⊗ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ (η ▷ f₂ ≪≫ g₁ ◁ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ (mk R ↑(of R R) ↑M).compr₂ₛₗ (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) =
    (mk R ↑(of R R) ↑M).compr₂ₛₗ (Hom.hom ((leftUnitor M).hom ≫ f))

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
x✝ : ↑M
⊢ (((mk R ↑(of R R) ↑M).compr₂ₛₗ (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom))) 1) x✝ =
    (((mk R ↑(of R R) ↑M).compr₂ₛₗ (Hom.hom ((leftUnitor M).hom ≫ f))) 1) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ (mk R ↑M ↑(of R R)).compr₂ₛₗ (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) =
    (mk R ↑M ↑(of R R)).compr₂ₛₗ (Hom.hom ((rightUnitor M).hom ≫ f))

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
x✝ : ↑M
⊢ (((mk R ↑M ↑(of R R)).compr₂ₛₗ (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom))) x✝) 1 =
    (((mk R ↑M ↑(of R R)).compr₂ₛₗ (Hom.hom ((rightUnitor M).hom ≫ f))) x✝) 1
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
⊢ (TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f) = (TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)) x✝¹) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
⊢ (TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f) = (TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)) x✝¹) 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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ δ F X Y ▷ T ≫ μ F X Y ▷ T = 𝟙 (F.obj (X ⊗ Y) ⊗ T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, δ_μ, id_whiskerRight]

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

Goal state before:
pp: case δ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ δ F = δ F

Tactic:
ext

Goal state after:
case δ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ μ F = μ F

Tactic:
ext

Goal state after:
case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ = μ F x✝¹ x✝
Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence

Goal state before:
pp: case e'_2.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
e_2✝ : ↑A = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A)
⊢ DistribMulAction.toDistribSMul.toSMul = ZSMul.toSMul

Tactic:
ext

Goal state after:
case e'_2.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
e_2✝ : ↑A = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A)
x✝¹ : ℤ
x✝ : ↑A
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence

Goal state before:
pp: case e'_3.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
⊢ DistribMulAction.toDistribSMul.toSMul = ZSMul.toSMul

Tactic:
ext

Goal state after:
case e'_3.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
x✝¹ : ℤ
x✝ : ↑B
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η : h ⟶ i
η₁ : g ⊗ h ⟶ g ⊗ i
η₂ : f ⊗ g ⊗ h ⟶ f ⊗ g ⊗ i
η₃ : f ⊗ g ⊗ h ⟶ (f ⊗ g) ⊗ i
η₄ : (f ⊗ g) ⊗ h ⟶ (f ⊗ g) ⊗ i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ (α_ f g i).inv = η₃
e_η₄ : (α_ f g h).hom ≫ η₃ = η₄
⊢ (f ⊗ g) ◁ η = η₄

Tactic:
by
  simp [e_η₁, e_η₂, e_η₃, e_η₄]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g h : C
η : f ⟶ f'
η₁ : f ⊗ g ⟶ f' ⊗ g
η₂ : (f ⊗ g) ⊗ h ⟶ (f' ⊗ g) ⊗ h
η₃ : (f ⊗ g) ⊗ h ⟶ f' ⊗ g ⊗ h
η₄ : f ⊗ g ⊗ h ⟶ f' ⊗ g ⊗ h
e_η₁ : η ▷ g = η₁
e_η₂ : η₁ ▷ h = η₂
e_η₃ : η₂ ≫ (α_ f' g h).hom = η₃
e_η₄ : (α_ f g h).inv ≫ η₃ = η₄
⊢ η ▷ (g ⊗ h) = η₄

Tactic:
by
  simp [e_η₁, e_η₂, e_η₃, e_η₄]

Goal state after:
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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ ε (F.prod G) ≫ η (F.prod G) = 𝟙 (𝟙_ (D × C'))

Tactic:
ext

Goal state after:
case h₁
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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (ε (F.prod G) ≫ η (F.prod G)).1 = (𝟙 (𝟙_ (D × C'))).1

case h₂
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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (ε (F.prod G) ≫ η (F.prod G)).2 = (𝟙 (𝟙_ (D × C'))).2
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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ η (F.prod G) ≫ ε (F.prod G) = 𝟙 ((F.prod G).obj (𝟙_ (C × E)))

Tactic:
ext

Goal state after:
case h₁
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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod G) ≫ ε (F.prod G)).1 = (𝟙 ((F.prod G).obj (𝟙_ (C × E)))).1

case h₂
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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (η (F.prod G) ≫ ε (F.prod G)).2 = (𝟙 ((F.prod G).obj (𝟙_ (C × E)))).2