[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.73, u_1} C
inst✝ : MonoidalCategory C
⊢ Inhabited (MonoidalSingleObj C)
[PROOFSTEP]
unfold MonoidalSingleObj
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.73, u_1} C
inst✝ : MonoidalCategory C
⊢ Inhabited PUnit
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ : MonoidalSingleObj C
f✝ g✝ : a✝ ⟶ b✝
x✝ : f✝ ⟶ g✝
⊢ (fun {a b c} X Y Z f => 𝟙 X ⊗ f) (𝟙 a✝) f✝ g✝ x✝ =
    ((fun {a b} X => λ_ X) f✝).hom ≫ x✝ ≫ ((fun {a b} X => λ_ X) g✝).inv
[PROOFSTEP]
simp_rw [leftUnitor_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ c✝ d✝ : MonoidalSingleObj C
x✝⁴ : a✝ ⟶ b✝
x✝³ : b✝ ⟶ c✝
x✝² x✝¹ : c✝ ⟶ d✝
x✝ : x✝² ⟶ x✝¹
⊢ (fun {a b c} X Y Z f => 𝟙 X ⊗ f) (x✝⁴ ≫ x✝³) x✝² x✝¹ x✝ =
    ((fun {a b c d} X Y Z => α_ X Y Z) x✝⁴ x✝³ x✝²).hom ≫
      (fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝⁴ (x✝³ ≫ x✝²) (x✝³ ≫ x✝¹) ((fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝³ x✝² x✝¹ x✝) ≫
        ((fun {a b c d} X Y Z => α_ X Y Z) x✝⁴ x✝³ x✝¹).inv
[PROOFSTEP]
simp_rw [associator_inv_naturality, Iso.hom_inv_id_assoc, tensor_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ : MonoidalSingleObj C
f✝ g✝ : a✝ ⟶ b✝
x✝ : f✝ ⟶ g✝
⊢ (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) x✝ (𝟙 b✝) =
    ((fun {a b} X => ρ_ X) f✝).hom ≫ x✝ ≫ ((fun {a b} X => ρ_ X) g✝).inv
[PROOFSTEP]
simp_rw [rightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ c✝ d✝ : MonoidalSingleObj C
f✝ f'✝ : a✝ ⟶ b✝
x✝² : f✝ ⟶ f'✝
x✝¹ : b✝ ⟶ c✝
x✝ : c✝ ⟶ d✝
⊢ (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) x✝² (x✝¹ ≫ x✝) =
    ((fun {a b c d} X Y Z => α_ X Y Z) f✝ x✝¹ x✝).inv ≫
      (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) ((fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) x✝² x✝¹) x✝ ≫
        ((fun {a b c d} X Y Z => α_ X Y Z) f'✝ x✝¹ x✝).hom
[PROOFSTEP]
simp_rw [← tensor_id, associator_naturality, Iso.inv_hom_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ c✝ d✝ : MonoidalSingleObj C
x✝⁴ : a✝ ⟶ b✝
x✝³ x✝² : b✝ ⟶ c✝
x✝¹ : x✝³ ⟶ x✝²
x✝ : c✝ ⟶ d✝
⊢ (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) ((fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝⁴ x✝³ x✝² x✝¹) x✝ =
    ((fun {a b c d} X Y Z => α_ X Y Z) x✝⁴ x✝³ x✝).hom ≫
      (fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝⁴ (x✝³ ≫ x✝) (x✝² ≫ x✝) ((fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) x✝¹ x✝) ≫
        ((fun {a b c d} X Y Z => α_ X Y Z) x✝⁴ x✝² x✝).inv
[PROOFSTEP]
simp_rw [associator_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.162, u_1} C
inst✝ : MonoidalCategory C
a✝ b✝ c✝ d✝ e✝ : MonoidalSingleObj C
x✝³ : a✝ ⟶ b✝
x✝² : b✝ ⟶ c✝
x✝¹ : c✝ ⟶ d✝
x✝ : d✝ ⟶ e✝
⊢ (fun {a b c} {f g} f_1 Z => f_1 ⊗ 𝟙 Z) ((fun {a b c d} X Y Z => α_ X Y Z) x✝³ x✝² x✝¹).hom x✝ ≫
      ((fun {a b c d} X Y Z => α_ X Y Z) x✝³ (x✝² ≫ x✝¹) x✝).hom ≫
        (fun {a b c} X Y Z f => 𝟙 X ⊗ f) x✝³ ((x✝² ≫ x✝¹) ≫ x✝) (x✝² ≫ x✝¹ ≫ x✝)
          ((fun {a b c d} X Y Z => α_ X Y Z) x✝² x✝¹ x✝).hom =
    ((fun {a b c d} X Y Z => α_ X Y Z) (x✝³ ≫ x✝²) x✝¹ x✝).hom ≫
      ((fun {a b c d} X Y Z => α_ X Y Z) x✝³ x✝² (x✝¹ ≫ x✝)).hom
[PROOFSTEP]
simp_rw [pentagon]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.14692, u_1} C
inst✝ : MonoidalCategory C
X✝ Y✝ X'✝ Y'✝ : EndMonoidal (MonoidalSingleObj.star C)
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ ((Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).map f ⊗
        (Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).map g) ≫
      (fun X Y =>
          𝟙
            ((Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).obj X ⊗
              (Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).obj Y))
        Y✝ Y'✝ =
    (fun X Y =>
          𝟙
            ((Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).obj X ⊗
              (Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).obj Y))
        X✝ X'✝ ≫
      (Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).map (f ⊗ g)
[PROOFSTEP]
simp_rw [Category.id_comp, Category.comp_id]
  -- Should we provide further simp lemmas so this goal becomes visible?
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.14692, u_1} C
inst✝ : MonoidalCategory C
X✝ Y✝ X'✝ Y'✝ : EndMonoidal (MonoidalSingleObj.star C)
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ f ⊗ g = f ⊗ g
[PROOFSTEP]
exact (tensor_id_comp_id_tensor _ _).symm
