-- 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
⊢ (if hi : 0 = 0 then GradedObject.singleObjApplyIsoOfEq 0 (𝟙_ C) 0 hi ≪≫ (singleObjXIsoOfEq c 0 (𝟙_ C) 0 hi).symm
      else { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom =
    GradedObject.Monoidal.tensorUnit₀.hom ≫ (singleObjXSelf c 0 (𝟙_ C)).inv

Tactic:
rw [dif_pos rfl]

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
⊢ (GradedObject.singleObjApplyIsoOfEq 0 (𝟙_ C) 0 ⋯ ≪≫ (singleObjXIsoOfEq c 0 (𝟙_ C) 0 ⋯).symm).hom =
    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:
rw [id_tensorHom, ← MonoidalCategory.whiskerLeft_comp_assoc]

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 ≫ (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:
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

Tactic:
dsimp [tensorUnitIso]

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
⊢ (if hi : 0 = 0 then GradedObject.singleObjApplyIsoOfEq 0 (𝟙_ C) 0 hi ≪≫ (singleObjXIsoOfEq c 0 (𝟙_ C) 0 hi).symm
      else { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom =
    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 ≫ (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:
congr 2

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
⊢ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 = (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
⊢ (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 ⋯

Tactic:
rw [GradedObject.Monoidal.rightUnitor_inv_apply, assoc, assoc, Iso.cancel_iso_inv_left,
  GradedObject.Monoidal.ι_tensorHom]

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 ⋯