-- Mathlib/Algebra/Homology/Monoidal.lean
lemma rightUnitor'_inv (i : I) :
    (rightUnitor' K).inv i = (ρ_ (K.X i)).inv ≫ ((K.X i) ◁ (singleObjXSelf c 0 (𝟙_ C)).inv) ≫
      ιTensorObj K (tensorUnit C c) i 0 i (add_zero i)

Proof state:
case e_a.e_f
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 = (singleObjXSelf c 0 (𝟙_ C)).inv

Tactic:
rw [← cancel_epi (GradedObject.Monoidal.tensorUnit₀ (I := I)).hom, Iso.hom_inv_id_assoc]

Result:
case e_a.e_f
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ (tensorUnitIso C c).hom 0 = GradedObject.Monoidal.tensorUnit₀.hom ≫ (singleObjXSelf c 0 (𝟙_ C)).inv

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ K.X i ◁ GradedObject.Monoidal.tensorUnit₀.inv ≫
      (𝟙 K.X i ⊗ (tensorUnitIso C c).hom 0) ≫ GradedObject.Monoidal.ιTensorObj K.X (tensorUnit C c).X i 0 i ⋯ =
    K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) i 0 i ⋯

Tactic:
dsimp

Result:
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ K.X i ◁ GradedObject.Monoidal.tensorUnit₀.inv ≫
      (𝟙 (K.X i) ⊗ (tensorUnitIso C c).hom 0) ≫ GradedObject.Monoidal.ιTensorObj K.X (tensorUnit C c).X i 0 i ⋯ =
    K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) i 0 i ⋯

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ K.rightUnitor'.inv i =
    (ρ_ (K.X i)).inv ≫ K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) i 0 i ⋯

Tactic:
dsimp [rightUnitor']

Result:
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ (GradedObject.Monoidal.rightUnitor K.X).inv i ≫ GradedObject.Monoidal.tensorHom (𝟙 K.X) (tensorUnitIso C c).hom i =
    (ρ_ (K.X i)).inv ≫ K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) i 0 i ⋯

Proof state:
case e_a.e_f
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ (GradedObject.singleObjApplyIsoOfEq 0 (𝟙_ C) 0 ⋯ ≪≫ (singleObjXIsoOfEq c 0 (𝟙_ C) 0 ⋯).symm).hom =
    GradedObject.Monoidal.tensorUnit₀.hom ≫ (singleObjXSelf c 0 (𝟙_ C)).inv

Tactic:
rfl

Result:
no goals