[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
⊢ 𝟙 X ⊗ f = X ◁ f
[PROOFSTEP]
simp [tensorHom_def]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ f ⊗ 𝟙 Y = f ▷ Y
[PROOFSTEP]
simp [tensorHom_def]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g
[PROOFSTEP]
simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
X Y X' Y' : C
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f : X ≅ Y
g : X' ≅ Y'
⊢ (f.hom ⊗ g.hom) ≫ (f.inv ⊗ g.inv) = 𝟙 (X ⊗ X')
[PROOFSTEP]
rw [← tensor_comp, Iso.hom_inv_id, Iso.hom_inv_id, ← tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
X Y X' Y' : C
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f : X ≅ Y
g : X' ≅ Y'
⊢ (f.inv ⊗ g.inv) ≫ (f.hom ⊗ g.hom) = 𝟙 (Y ⊗ Y')
[PROOFSTEP]
rw [← tensor_comp, Iso.inv_hom_id, Iso.inv_hom_id, ← tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝⁴ : MonoidalCategory C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
inst✝¹ : IsIso f
g : Y ⟶ Z
inst✝ : IsIso g
⊢ inv (f ⊗ g) = inv f ⊗ inv g
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case hom_inv_id
C_1 : Type u
𝒞 : Category.{v, u} C_1
inst : MonoidalCategory C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
inst_3 : IsIso f
g : Y ⟶ Z
inst_4 : IsIso g
⊢ (f ⊗ g) ≫ (inv f ⊗ inv g) = 𝟙 (W ⊗ Y)
[PROOFSTEP]
simp [← tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V W✝ X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ⊗ if h : P then g h else g' h) = if h : P then f ⊗ g h else f ⊗ g' h
[PROOFSTEP]
split_ifs
[GOAL]
case pos
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V W✝ X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ f ⊗ g h✝ = f ⊗ g h✝
[PROOFSTEP]
rfl
[GOAL]
case neg
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V W✝ X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ f ⊗ g' h✝ = f ⊗ g' h✝
[PROOFSTEP]
rfl
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V W✝ X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (if h : P then g h else g' h) ⊗ f = if h : P then g h ⊗ f else g' h ⊗ f
[PROOFSTEP]
split_ifs
[GOAL]
case pos
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V W✝ X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ g h✝ ⊗ f = g h✝ ⊗ f
[PROOFSTEP]
rfl
[GOAL]
case neg
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V W✝ X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ g' h✝ ⊗ f = g' h✝ ⊗ f
[PROOFSTEP]
rfl
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ f ≫ g ⊗ 𝟙 Z = (f ⊗ 𝟙 Z) ≫ (g ⊗ 𝟙 Z)
[PROOFSTEP]
rw [← tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ f ≫ g ⊗ 𝟙 Z = f ≫ g ⊗ 𝟙 Z ≫ 𝟙 Z
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ f ≫ g = (𝟙 Z ⊗ f) ≫ (𝟙 Z ⊗ g)
[PROOFSTEP]
rw [← tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ f ≫ g = 𝟙 Z ≫ 𝟙 Z ⊗ f ≫ g
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ (𝟙 Y ⊗ f) ≫ (g ⊗ 𝟙 X) = g ⊗ f
[PROOFSTEP]
rw [← tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ 𝟙 Y ≫ g ⊗ f ≫ 𝟙 X = g ⊗ f
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ (g ⊗ 𝟙 W) ≫ (𝟙 Z ⊗ f) = g ⊗ f
[PROOFSTEP]
rw [← tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ g ≫ 𝟙 Z ⊗ 𝟙 W ≫ f = g ⊗ f
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
f : X ⟶ Y
⊢ f ⊗ 𝟙 (𝟙_ C) = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv
[PROOFSTEP]
rw [← rightUnitor_naturality_assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
f : X ⟶ Y
⊢ 𝟙 (𝟙_ C) ⊗ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv
[PROOFSTEP]
rw [← leftUnitor_naturality_assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y Z X X' : C
f : X ⟶ X'
⊢ f ≫ (λ_ X').inv = (λ_ X).inv ≫ (𝟙 tensorUnit' ⊗ f)
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y Z X X' : C
f : X ⟶ X'
⊢ f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ (f ⊗ 𝟙 tensorUnit')
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
⊢ 𝟙 (𝟙_ C) ⊗ f = 𝟙 (𝟙_ C) ⊗ g ↔ f = g
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
⊢ f ⊗ 𝟙 (𝟙_ C) = g ⊗ 𝟙 (𝟙_ C) ↔ f = g
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
simp [pentagon]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
⊢ (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ (𝟙 X ⊗ (ρ_ Y).hom)
[PROOFSTEP]
rw [← tensor_right_iff, comp_tensor_id, ← cancel_mono (α_ X Y (𝟙_ C)).hom, assoc, associator_naturality, ←
  triangle_assoc, ← triangle, id_tensor_comp, pentagon_assoc, ← associator_naturality, tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
⊢ inv (ρ_ (X ⊗ Y)).inv = inv ((𝟙 X ⊗ (ρ_ Y).inv) ≫ (α_ X Y (𝟙_ C)).inv)
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
⊢ (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ⊗ 𝟙 Y) = 𝟙 X ⊗ (λ_ Y).hom
[PROOFSTEP]
rw [← triangle, Iso.inv_hom_id_assoc]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
⊢ (𝟙 X ⊗ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ⊗ 𝟙 Y
[PROOFSTEP]
apply (cancel_mono ((ρ_ X).hom ⊗ 𝟙 Y)).1
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
⊢ ((𝟙 X ⊗ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv) ≫ ((ρ_ X).hom ⊗ 𝟙 Y) = ((ρ_ X).inv ⊗ 𝟙 Y) ≫ ((ρ_ X).hom ⊗ 𝟙 Y)
[PROOFSTEP]
simp only [triangle_assoc_comp_right, assoc]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z X Y : C
⊢ (𝟙 X ⊗ (λ_ Y).inv) ≫ (𝟙 X ⊗ (λ_ Y).hom) = ((ρ_ X).inv ⊗ 𝟙 Y) ≫ ((ρ_ X).hom ⊗ 𝟙 Y)
[PROOFSTEP]
rw [← id_tensor_comp, Iso.inv_hom_id, ← comp_tensor_id, Iso.inv_hom_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z✝ X Y Z X' Y' Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ g ⊗ h) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h)
[PROOFSTEP]
rw [comp_inv_eq, assoc, associator_naturality]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z✝ X Y Z X' Y' Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ f ⊗ g ⊗ h = (α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ (f ⊗ g ⊗ h)
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z✝ X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ g) ⊗ h = (α_ X Y Z).hom ≫ (f ⊗ g ⊗ h) ≫ (α_ X' Y' Z').inv
[PROOFSTEP]
rw [associator_inv_naturality, hom_inv_id_assoc]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z✝ X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ f ⊗ g ⊗ h = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) ≫ (α_ X' Y' Z').hom
[PROOFSTEP]
rw [associator_naturality, inv_hom_id_assoc]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z✝ X Y Z Z' : C
h : Z ⟶ Z'
⊢ (𝟙 (X ⊗ Y) ⊗ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ 𝟙 Y ⊗ h)
[PROOFSTEP]
rw [← tensor_id, associator_naturality]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z✝ X Y Z X' : C
f : X ⟶ X'
⊢ (f ⊗ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ 𝟙 Y) ⊗ 𝟙 Z)
[PROOFSTEP]
rw [← tensor_id, associator_inv_naturality]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V✝ W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
rw [← tensor_comp, f.hom_inv_id, id_tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V✝ W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
rw [← tensor_comp, f.inv_hom_id, id_tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V✝ W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
rw [← tensor_comp, f.hom_inv_id, comp_tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V✝ W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
rw [← tensor_comp, f.inv_hom_id, comp_tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V✝ W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
rw [← tensor_comp, IsIso.hom_inv_id, id_tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V✝ W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
rw [← tensor_comp, IsIso.inv_hom_id, id_tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V✝ W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
rw [← tensor_comp, IsIso.hom_inv_id, comp_tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
U V✝ W✝ X✝ Y✝ Z✝ 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)
[PROOFSTEP]
rw [← tensor_comp, IsIso.inv_hom_id, comp_tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
⊢ ∀ {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    (fun {X₁ Y₁ X₂ Y₂} => tensorHom) f g =
      (fun {X₁ X₂} f X => whiskerRight f X) f X₂ ≫ (fun X x x_1 f => whiskerLeft X f) Y₁ X₂ Y₂ g
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
X₁✝ Y₁✝ X₂✝ Y₂✝ : C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (fun {X₁ Y₁ X₂ Y₂} => tensorHom) f✝ g✝ =
    (fun {X₁ X₂} f X => whiskerRight f X) f✝ X₂✝ ≫ (fun X x x_1 f => whiskerLeft X f) Y₁✝ X₂✝ Y₂✝ g✝
[PROOFSTEP]
simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
⊢ ∀ (X Y : C), (fun X x x_1 f => whiskerLeft X f) X Y Y (𝟙 Y) = 𝟙 (tensorObj X Y)
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
X✝ Y✝ : C
⊢ (fun X x x_1 f => whiskerLeft X f) X✝ Y✝ Y✝ (𝟙 Y✝) = 𝟙 (tensorObj X✝ Y✝)
[PROOFSTEP]
simp [← id_tensorHom, ← tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
⊢ ∀ (X Y : C), (fun {X₁ X₂} f X => whiskerRight f X) (𝟙 X) Y = 𝟙 (tensorObj X Y)
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
X✝ Y✝ : C
⊢ (fun {X₁ X₂} f X => whiskerRight f X) (𝟙 X✝) Y✝ = 𝟙 (tensorObj X✝ Y✝)
[PROOFSTEP]
simp [← tensorHom_id, tensor_id]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
⊢ ∀ (W X Y Z : C),
    (fun {X₁ Y₁ X₂ Y₂} => tensorHom) (associator W X Y).hom (𝟙 Z) ≫
        (associator W (tensorObj X Y) Z).hom ≫ (fun {X₁ Y₁ X₂ Y₂} => tensorHom) (𝟙 W) (associator X Y Z).hom =
      (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
W✝ X✝ Y✝ Z✝ : C
⊢ (fun {X₁ Y₁ X₂ Y₂} => tensorHom) (associator W✝ X✝ Y✝).hom (𝟙 Z✝) ≫
      (associator W✝ (tensorObj X✝ Y✝) Z✝).hom ≫ (fun {X₁ Y₁ X₂ Y₂} => tensorHom) (𝟙 W✝) (associator X✝ Y✝ Z✝).hom =
    (associator (tensorObj W✝ X✝) Y✝ Z✝).hom ≫ (associator W✝ X✝ (tensorObj Y✝ Z✝)).hom
[PROOFSTEP]
simp [← id_tensorHom, ← tensorHom_id, pentagon]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
⊢ ∀ (X Y : C),
    (associator X tensorUnit' Y).hom ≫ (fun {X₁ Y₁ X₂ Y₂} => tensorHom) (𝟙 X) (leftUnitor Y).hom =
      (fun {X₁ Y₁ X₂ Y₂} => tensorHom) (rightUnitor X).hom (𝟙 Y)
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y Z : C
tensorObj : C → C → C
tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
whiskerLeft :
  optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom (𝟙 X) f
whiskerRight :
  optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom f (𝟙 Y)
tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂)) _auto✝
id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f) _auto✝
tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y) _auto✝
tensor_comp :
  autoParam
    (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
    _auto✝
tensorUnit' : C
associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
associator_naturality :
  autoParam
    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (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₃))
    _auto✝
leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X
leftUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f) _auto✝
rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X
rightUnitor_naturality :
  autoParam (∀ {X Y : C} (f : X ⟶ Y), tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f)
    _auto✝
pentagon :
  autoParam
    (∀ (W X Y Z : C),
      tensorHom (associator W X Y).hom (𝟙 Z) ≫
          (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
        (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
    _auto✝
triangle :
  autoParam
    (∀ (X Y : C),
      (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y))
    _auto✝
X✝ Y✝ : C
⊢ (associator X✝ tensorUnit' Y✝).hom ≫ (fun {X₁ Y₁ X₂ Y₂} => tensorHom) (𝟙 X✝) (leftUnitor Y✝).hom =
    (fun {X₁ Y₁ X₂ Y₂} => tensorHom) (rightUnitor X✝).hom (𝟙 Y✝)
[PROOFSTEP]
simp [← id_tensorHom, ← tensorHom_id, triangle]
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ (X : C × C × C) → (leftAssocTensor C).obj X ≅ (rightAssocTensor C).obj X
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X✝ : C × C × C
⊢ (leftAssocTensor C).obj X✝ ≅ (rightAssocTensor C).obj X✝
[PROOFSTEP]
apply MonoidalCategory.associator
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ ∀ {X Y : C × C × C} (f : X ⟶ Y),
    (leftAssocTensor C).map f ≫ (α_ Y.fst Y.snd.fst Y.snd.snd).hom =
      (α_ X.fst X.snd.fst X.snd.snd).hom ≫ (rightAssocTensor C).map f
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X✝ Y✝ : C × C × C
f✝ : X✝ ⟶ Y✝
⊢ (leftAssocTensor C).map f✝ ≫ (α_ Y✝.fst Y✝.snd.fst Y✝.snd.snd).hom =
    (α_ X✝.fst X✝.snd.fst X✝.snd.snd).hom ≫ (rightAssocTensor C).map f✝
[PROOFSTEP]
apply MonoidalCategory.associator_naturality
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ (X : C) → (tensorUnitLeft C).obj X ≅ (𝟭 C).obj X
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X✝ : C
⊢ (tensorUnitLeft C).obj X✝ ≅ (𝟭 C).obj X✝
[PROOFSTEP]
apply MonoidalCategory.leftUnitor
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ ∀ {X Y : C} (f : X ⟶ Y), (tensorUnitLeft C).map f ≫ (λ_ Y).hom = (λ_ X).hom ≫ (𝟭 C).map f
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (tensorUnitLeft C).map f✝ ≫ (λ_ Y✝).hom = (λ_ X✝).hom ≫ (𝟭 C).map f✝
[PROOFSTEP]
apply MonoidalCategory.leftUnitor_naturality
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ (X : C) → (tensorUnitRight C).obj X ≅ (𝟭 C).obj X
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X✝ : C
⊢ (tensorUnitRight C).obj X✝ ≅ (𝟭 C).obj X✝
[PROOFSTEP]
apply MonoidalCategory.rightUnitor
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ ∀ {X Y : C} (f : X ⟶ Y), (tensorUnitRight C).map f ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ (𝟭 C).map f
[PROOFSTEP]
intros
[GOAL]
C✝ : Type u
𝒞 : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (tensorUnitRight C).map f✝ ≫ (ρ_ Y✝).hom = (ρ_ X✝).hom ≫ (𝟭 C).map f✝
[PROOFSTEP]
apply MonoidalCategory.rightUnitor_naturality
[GOAL]
C✝¹ : Type u
𝒞 : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
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
[PROOFSTEP]
dsimp
[GOAL]
C✝¹ : Type u
𝒞 : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
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)
[PROOFSTEP]
rw [← tensor_id]
[GOAL]
C✝¹ : Type u
𝒞 : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
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)
[PROOFSTEP]
apply associator_naturality
[GOAL]
C✝¹ : Type u
𝒞 : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ NatTrans.app (tensorLeftTensor X Y).inv Z = (α_ X Y Z).inv
[PROOFSTEP]
simp [tensorLeftTensor]
[GOAL]
C✝² : Type u
𝒞 : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
h : (tensoringLeft C).map f = (tensoringLeft C).map g
⊢ f = g
[PROOFSTEP]
injections h
[GOAL]
C✝² : Type u
𝒞 : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
h : (fun Z => f ⊗ 𝟙 Z) = fun Z => g ⊗ 𝟙 Z
⊢ f = g
[PROOFSTEP]
replace h := congr_fun h (𝟙_ C)
[GOAL]
C✝² : Type u
𝒞 : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
h : f ⊗ 𝟙 (𝟙_ C) = g ⊗ 𝟙 (𝟙_ C)
⊢ f = g
[PROOFSTEP]
simpa using h
[GOAL]
C✝² : Type u
𝒞 : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
h : (tensoringRight C).map f = (tensoringRight C).map g
⊢ f = g
[PROOFSTEP]
injections h
[GOAL]
C✝² : Type u
𝒞 : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
h : (fun Z => 𝟙 Z ⊗ f) = fun Z => 𝟙 Z ⊗ g
⊢ f = g
[PROOFSTEP]
replace h := congr_fun h (𝟙_ C)
[GOAL]
C✝² : Type u
𝒞 : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
h : 𝟙 (𝟙_ C) ⊗ f = 𝟙 (𝟙_ C) ⊗ g
⊢ f = g
[PROOFSTEP]
simpa using h
[GOAL]
C✝³ : Type u
𝒞 : Category.{v, u} C✝³
inst✝⁸ : MonoidalCategory C✝³
C✝² : Type u
inst✝⁷ : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (tensorRight (X ⊗ Y)).map f ≫ ((fun Z => (α_ Z X Y).symm) Z').hom =
    ((fun Z => (α_ Z X Y).symm) Z).hom ≫ (tensorRight X ⋙ tensorRight Y).map f
[PROOFSTEP]
dsimp
[GOAL]
C✝³ : Type u
𝒞 : Category.{v, u} C✝³
inst✝⁸ : MonoidalCategory C✝³
C✝² : Type u
inst✝⁷ : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (f ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ Z' X Y).inv = (α_ Z X Y).inv ≫ ((f ⊗ 𝟙 X) ⊗ 𝟙 Y)
[PROOFSTEP]
rw [← tensor_id]
[GOAL]
C✝³ : Type u
𝒞 : Category.{v, u} C✝³
inst✝⁸ : MonoidalCategory C✝³
C✝² : Type u
inst✝⁷ : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (f ⊗ 𝟙 X ⊗ 𝟙 Y) ≫ (α_ Z' X Y).inv = (α_ Z X Y).inv ≫ ((f ⊗ 𝟙 X) ⊗ 𝟙 Y)
[PROOFSTEP]
apply associator_inv_naturality
[GOAL]
C✝³ : Type u
𝒞 : Category.{v, u} C✝³
inst✝⁸ : MonoidalCategory C✝³
C✝² : Type u
inst✝⁷ : Category.{v, u} C✝²
inst✝⁶ : MonoidalCategory C✝²
C✝¹ : Type u
inst✝⁵ : Category.{v, u} C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category.{v, u} C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ NatTrans.app (tensorRightTensor X Y).inv Z = (α_ Z X Y).hom
[PROOFSTEP]
simp [tensorRightTensor]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
⊢ ∀ {X₁ Y₁ X₂ Y₂ : C₁ × C₂} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    (fun {X₁ Y₁ X₂ Y₂} f g => (f.fst ⊗ g.fst, f.snd ⊗ g.snd)) f g =
      (fun {X₁ X₂} f X => (f.fst ▷ X.fst, f.snd ▷ X.snd)) f X₂ ≫
        (fun X x x_1 f => (X.fst ◁ f.fst, X.snd ◁ f.snd)) Y₁ X₂ Y₂ g
[PROOFSTEP]
simp [tensorHom_def]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (λ_ X).hom.fst = (λ_ X.fst).hom
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).hom.fst = (λ_ (fst✝, snd✝).fst).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (λ_ X).hom.snd = (λ_ X.snd).hom
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).hom.snd = (λ_ (fst✝, snd✝).snd).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (λ_ X).inv.fst = (λ_ X.fst).inv
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).inv.fst = (λ_ (fst✝, snd✝).fst).inv
[PROOFSTEP]
rfl
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (λ_ X).inv.snd = (λ_ X.snd).inv
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).inv.snd = (λ_ (fst✝, snd✝).snd).inv
[PROOFSTEP]
rfl
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (ρ_ X).hom.fst = (ρ_ X.fst).hom
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).hom.fst = (ρ_ (fst✝, snd✝).fst).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (ρ_ X).hom.snd = (ρ_ X.snd).hom
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).hom.snd = (ρ_ (fst✝, snd✝).snd).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (ρ_ X).inv.fst = (ρ_ X.fst).inv
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).inv.fst = (ρ_ (fst✝, snd✝).fst).inv
[PROOFSTEP]
rfl
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (ρ_ X).inv.snd = (ρ_ X.snd).inv
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u
𝒞 : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).inv.snd = (ρ_ (fst✝, snd✝).snd).inv
[PROOFSTEP]
rfl