[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A : Mon_ C
M : Mod_ A
⊢ (𝟙 A.X ⊗ M.act) ≫ M.act = (α_ A.X A.X M.X).inv ≫ (A.mul ⊗ 𝟙 M.X) ≫ M.act
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A : Mon_ C
M✝ M : Mod_ A
⊢ (𝟙 M).hom = 𝟙 M.X
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.one ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act = (λ_ M.X).hom
[PROOFSTEP]
slice_lhs 1 2 => rw [← comp_tensor_id]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (A.one ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (A.one ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (A.one ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.one ≫ f.hom ⊗ 𝟙 M.X) ≫ M.act = (λ_ M.X).hom
[PROOFSTEP]
rw [f.one_hom, one_act]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫ (𝟙 A.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act
[PROOFSTEP]
slice_rhs 2 3 => rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 A.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act) ≫ (f.hom ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 A.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act) ≫ (f.hom ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 A.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act) ≫ (f.hom ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫ ((f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (𝟙 B.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act)) ≫ M.act
[PROOFSTEP]
rw [id_tensor_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫ ((f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (𝟙 B.X ⊗ M.act)) ≫ M.act
[PROOFSTEP]
slice_rhs 4 5 => rw [Mod_.assoc_flip]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ M.act) ≫ M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| 𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X
[PROOFSTEP]
rw [Mod_.assoc_flip]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ M.act) ≫ M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| 𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X
[PROOFSTEP]
rw [Mod_.assoc_flip]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ M.act) ≫ M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| 𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X
[PROOFSTEP]
rw [Mod_.assoc_flip]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫
      (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (α_ B.X B.X M.X).inv ≫ (B.mul ⊗ 𝟙 M.X) ≫ M.act
[PROOFSTEP]
slice_rhs 3 4 => rw [associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (α_ B.X B.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
[PROOFSTEP]
rw [associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (α_ B.X B.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
[PROOFSTEP]
rw [associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (α_ B.X B.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
[PROOFSTEP]
rw [associator_inv_naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫
      (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (((α_ B.X A.X M.X).inv ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)) ≫ (B.mul ⊗ 𝟙 M.X)) ≫ M.act
[PROOFSTEP]
slice_rhs 2 3 => rw [← tensor_id, associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (α_ B.X A.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [← tensor_id, associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (α_ B.X A.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [← tensor_id, associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (α_ B.X A.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [← tensor_id, associator_inv_naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫
      ((((α_ A.X A.X M.X).inv ≫ ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X)) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)) ≫ (B.mul ⊗ 𝟙 M.X)) ≫ M.act
[PROOFSTEP]
slice_rhs 1 3 => rw [Iso.hom_inv_id_assoc]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom ≫ (α_ A.X A.X M.X).inv ≫ ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [Iso.hom_inv_id_assoc]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom ≫ (α_ A.X A.X M.X).inv ≫ ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [Iso.hom_inv_id_assoc]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom ≫ (α_ A.X A.X M.X).inv ≫ ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    ((((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)) ≫ (B.mul ⊗ 𝟙 M.X)) ≫ M.act
[PROOFSTEP]
slice_rhs 1 2 => rw [← comp_tensor_id, tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, tensor_id_comp_id_tensor]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act = (((f.hom ⊗ f.hom) ⊗ 𝟙 M.X) ≫ (B.mul ⊗ 𝟙 M.X)) ≫ M.act
[PROOFSTEP]
slice_rhs 1 2 => rw [← comp_tensor_id, ← f.mul_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ f.hom) ⊗ 𝟙 M.X) ≫ (B.mul ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, ← f.mul_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ f.hom) ⊗ 𝟙 M.X) ≫ (B.mul ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, ← f.mul_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ f.hom) ⊗ 𝟙 M.X) ≫ (B.mul ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, ← f.mul_hom]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act = (A.mul ≫ f.hom ⊗ 𝟙 M.X) ≫ M.act
[PROOFSTEP]
rw [comp_tensor_id, Category.assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
⊢ ((fun M => mk M.X ((f.hom ⊗ 𝟙 M.X) ≫ M.act)) X✝).act ≫ g.hom =
    (𝟙 A.X ⊗ g.hom) ≫ ((fun M => mk M.X ((f.hom ⊗ 𝟙 M.X) ≫ M.act)) Y✝).act
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
⊢ ((f.hom ⊗ 𝟙 X✝.X) ≫ X✝.act) ≫ g.hom = (𝟙 A.X ⊗ g.hom) ≫ (f.hom ⊗ 𝟙 Y✝.X) ≫ Y✝.act
[PROOFSTEP]
slice_rhs 1 2 => rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 A.X ⊗ g.hom) ≫ (f.hom ⊗ 𝟙 Y✝.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| Y✝.act
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 A.X ⊗ g.hom) ≫ (f.hom ⊗ 𝟙 Y✝.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| Y✝.act
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 A.X ⊗ g.hom) ≫ (f.hom ⊗ 𝟙 Y✝.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| Y✝.act
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
⊢ ((f.hom ⊗ 𝟙 X✝.X) ≫ X✝.act) ≫ g.hom = ((f.hom ⊗ 𝟙 X✝.X) ≫ (𝟙 B.X ⊗ g.hom)) ≫ Y✝.act
[PROOFSTEP]
slice_rhs 2 3 => rw [← g.act_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 B.X ⊗ g.hom) ≫ Y✝.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| f.hom ⊗ 𝟙 X✝.X
[PROOFSTEP]
rw [← g.act_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 B.X ⊗ g.hom) ≫ Y✝.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| f.hom ⊗ 𝟙 X✝.X
[PROOFSTEP]
rw [← g.act_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 B.X ⊗ g.hom) ≫ Y✝.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| f.hom ⊗ 𝟙 X✝.X
[PROOFSTEP]
rw [← g.act_hom]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
⊢ ((f.hom ⊗ 𝟙 X✝.X) ≫ X✝.act) ≫ g.hom = (f.hom ⊗ 𝟙 X✝.X) ≫ X✝.act ≫ g.hom
[PROOFSTEP]
rw [Category.assoc]
