-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
lemma triangle :
    (associator X₁ tensorUnit X₃).hom ≫ tensorHom (𝟙 X₁) (leftUnitor X₃).hom =
      tensorHom (rightUnitor X₁).hom (𝟙 X₃)

Proof state:
case convert_3
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{u_2, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₁₂Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₁₂ X₁ ((single₀ I).obj (𝟙_ C)) X₃

case convert_4
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{u_2, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₂₃Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₂₃ X₁ ((single₀ I).obj (𝟙_ C)) X₃

Tactic:
all_goals assumption

Result:
no goals

Proof state:
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{u_2, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ ∀ (X₁ X₃ : C),
    (((curriedAssociatorNatIso C).hom.app X₁).app (𝟙_ C)).app X₃ ≫
        ((curriedTensor C).obj X₁).map ((leftUnitorNatIso C).hom.app X₃) =
      ((curriedTensor C).map ((rightUnitorNatIso C).hom.app X₁)).app X₃

Tactic:
simp

Result:
no goals

Proof state:
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{u_2, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ (associator X₁ tensorUnit X₃).hom ≫ tensorHom (𝟙 X₁) (leftUnitor X₃).hom = tensorHom (rightUnitor X₁).hom (𝟙 X₃)

Tactic:
convert mapBifunctor_triangle (curriedAssociatorNatIso C) (𝟙_ C)
  (rightUnitorNatIso C) (leftUnitorNatIso C) (triangleIndexData I) X₁ X₃ (by simp)

Result:
case convert_3
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{u_2, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₁₂Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₁₂ X₁ ((single₀ I).obj (𝟙_ C)) X₃

case convert_4
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{u_2, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₂₃Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₂₃ X₁ ((single₀ I).obj (𝟙_ C)) X₃

Proof state:
case convert_4
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{u_2, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₂₃Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₂₃ X₁ ((single₀ I).obj (𝟙_ C)) X₃

Tactic:
assumption

Result:
no goals