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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f g h i : C
inst✝ : MonoidalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η : g ⟶ h
η' : g ≅ h
ih_η : η'.hom = η
⊢ (f ◁ᵢ η').hom = f ◁ η

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
⊢ (η' ▷ᵢ h).hom = η ▷ h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f₁ g₁ f₂ g₂ : C
η : f₁ ⟶ g₁
η' : f₁ ≅ g₁
ih_η : η'.hom = η
θ : f₂ ⟶ g₂
θ' : f₂ ≅ g₂
ih_θ : θ'.hom = θ
⊢ (η' ⊗ᵢ θ').hom = η ⊗ₘ θ

Tactic:
by

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (F ⋙ G).map x✝¹ ▷ (F ⋙ G).obj x✝ ≫ μ G (F.obj Y✝) (F.obj x✝) ≫ G.map (μ F Y✝ x✝) =
    (μ G (F.obj X✝) (F.obj x✝) ≫ G.map (μ F X✝ x✝)) ≫ (F ⋙ G).map (x✝¹ ▷ x✝)

Tactic:
by

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (F ⋙ G).obj x✝¹ ◁ (F ⋙ G).map x✝ ≫ μ G (F.obj x✝¹) (F.obj Y✝) ≫ G.map (μ F x✝¹ Y✝) =
    (μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝)) ≫ (F ⋙ G).map (x✝¹ ◁ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.CancelIso

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
⊢ f ≫ g = 𝟙 x

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.CancelIso

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
⊢ f ≫ g ≫ k = k

Tactic:
by

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ≫ G.map (μ F x✝² x✝¹)) ▷ (F ⋙ G).obj x✝ ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ (F ⋙ G).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((F ⋙ G).obj x✝²) ((F ⋙ G).obj x✝¹) ((F ⋙ G).obj x✝)).hom ≫
      (F ⋙ G).obj x✝² ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
by

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ δ F X X' ≫ (F.map f ⊗ₘ F.map g) = F.map (f ⊗ₘ g) ≫ δ F Y Y'

Tactic:
by

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M : SemimoduleCat R
N : SemimoduleCat R
⊢ tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (↑M ⊗[R] ↑N))

Tactic:
by

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ Y₁ Z₁ : SemimoduleCat R
X₂ Y₂ Z₂ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom f₁ f₂ ≫ tensorHom g₁ g₂ = tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg pfgh : C
η_f : p ⊗ f ≅ pf
η_g : pf ⊗ g ≅ pfg
η_h : pfg ⊗ h ≅ pfgh
⊢ (p ◁ α_ f g h ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h)).hom =
    (normalizeIsoComp (normalizeIsoComp η_f η_g) η_h).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ (p ◁ λ_ f ≪≫ η_f).hom = (normalizeIsoComp (ρ_ p) η_f).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ (p ◁ ρ_ f ≪≫ η_f).hom = (normalizeIsoComp η_f (ρ_ pf)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ p ◁ Iso.refl f ≪≫ η_f = η_f

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Tactic:
ext : 1
  apply TensorProduct.ext_threefold
  intro x y z
  rfl

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Tactic:
by

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
Y : D
f : F.obj X ⟶ Y
⊢ δ F (𝟙_ C) X ≫ (η F ⊗ₘ f) = F.map (λ_ X).hom ≫ (λ_ (F.obj X)).inv ≫ 𝟙_ D ◁ f

Tactic:
by

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
Y : D
f : F.obj X ⟶ Y
⊢ δ F X (𝟙_ C) ≫ (f ⊗ₘ η F) = F.map (ρ_ X).hom ≫ (ρ_ (F.obj X)).inv ≫ f ▷ 𝟙_ D

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Tactic:
by

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z =
    F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
W : SemimoduleCat R
X : SemimoduleCat R
Y : SemimoduleCat R
Z : SemimoduleCat R
⊢ whiskerRight (associator W X Y).hom Z ≫ (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom =
    (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom

Tactic:
by

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z =
    F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
⊢ (associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)

Tactic:
by

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
f : X ⟶ Y
X' : C
⊢ (G.map (δ F X X') ≫ δ G (F.obj X) (F.obj X')) ≫ (F ⋙ G).map f ▷ (F ⋙ G).obj X' =
    (F ⋙ G).map (f ▷ X') ≫ G.map (δ F Y X') ≫ δ G (F.obj Y) (F.obj X')

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ η_f = η_g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M₁ M₂ M₃ M₄ : SemimoduleCat R
f g : M₁ ⊗ M₂ ⊗ M₃ ⟶ M₄
h :
  ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
    (ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) = (ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.associator x✝² x✝¹ x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝² x✝¹))
                (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
          MonoidalCategory.tensorIso
            (Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                  (equivalenceSemimoduleCat.functor.obj x✝¹))).symm
            (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
        MonoidalCategoryStruct.associator (equivalenceSemimoduleCat.functor.obj x✝²)
            (equivalenceSemimoduleCat.functor.obj x✝¹) (equivalenceSemimoduleCat.functor.obj x✝) ≪≫
          MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝²))
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝¹)
                  (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
            Iso.refl
              (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝¹ x✝)))).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η = θ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.leftUnitor x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)))
                (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
          MonoidalCategory.tensorIso (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm
            (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
        MonoidalCategoryStruct.leftUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom

Tactic:
by

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (G.map (δ F x✝¹ X✝) ≫ δ G (F.obj x✝¹) (F.obj X✝)) ≫ (F ⋙ G).obj x✝¹ ◁ (F ⋙ G).map x✝ =
    (F ⋙ G).map (x✝¹ ◁ x✝) ≫ G.map (δ F x✝¹ Y✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.rightUnitor x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝)
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R))))).symm ≪≫
          MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))
            (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm) ≪≫
        MonoidalCategoryStruct.rightUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : 𝟙_ C ◁ η' ≪≫ η_g = η_f
Hθ : 𝟙_ C ◁ θ' ≪≫ η_g = η_f
⊢ η'.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : 𝟙_ C ◁ η' ≪≫ η_g = η_f
Hθ : 𝟙_ C ◁ θ' ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ'.hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : M₁ ⊗ M₂ ⊗ M₃ ⟶ M₄
h :
  ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
    (ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) = (ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ MonoidalPreadditive (ModuleCat R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (ModuleCat R)

Tactic:
by

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ (G.map (δ F (X ⊗ Y) Z) ≫ δ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
      (G.map (δ F X Y) ≫ δ G (F.obj X) (F.obj Y)) ▷ (F ⋙ G).obj Z ≫
        (α_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ((F ⋙ G).obj Z)).hom =
    (F ⋙ G).map (α_ X Y Z).hom ≫
      (G.map (δ F X (Y ⊗ Z)) ≫ δ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        (F ⋙ G).obj X ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ ε F ▷ T ≫ η F ▷ T = 𝟙 (𝟙_ D ⊗ T)

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ η F ▷ T ≫ ε F ▷ T = 𝟙 (F.obj (𝟙_ C) ⊗ T)

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ μ F X Y ▷ T ≫ δ F X Y ▷ T = 𝟙 ((F.obj X ⊗ F.obj Y) ⊗ T)

Tactic:
by

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
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:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ T ◁ ε F ≫ T ◁ η F = 𝟙 (T ⊗ 𝟙_ D)

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ T ◁ η F ≫ T ◁ ε F = 𝟙 (T ⊗ F.obj (𝟙_ C))

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ μ F X Y ≫ T ◁ δ F X Y = 𝟙 (T ⊗ F.obj X ⊗ F.obj Y)

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ δ F X Y ≫ T ◁ μ F X Y = 𝟙 (T ⊗ F.obj (X ⊗ Y))

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ F.map (f ⊗ₘ g) = δ F X X' ≫ (F.map f ⊗ₘ F.map g) ≫ μ F Y Y'

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
f : Y ⟶ Z
⊢ F.map (X ◁ f) = δ F X Y ≫ F.obj X ◁ F.map f ≫ μ F X Z

Tactic:
by

Goal state after: