-- Mathlib/Algebra/Homology/Monoidal.lean
lemma rightUnitor'_inv_comm (i j : I) :
    (rightUnitor' K).inv i ≫ (tensorObj K (tensorUnit C c)).d i j =
      K.d i j ≫ (rightUnitor' K).inv j

Proof state:
case pos
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 j : I
hij : c.Rel i j
⊢ (ρ_ (K.X i)).inv ≫
      K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫
        (c.ε₁ c c (i, 0) •
          ((curriedTensor C).map (K.d i j)).app ((tensorUnit C c).X 0) ≫
            K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c j 0 j ⋯) =
    K.d i j ≫ (ρ_ (K.X j)).inv ≫ K.X j ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) j 0 j ⋯

Tactic:
dsimp

Result:
case pos
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 j : I
hij : c.Rel i j
⊢ (ρ_ (K.X i)).inv ≫
      K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫
        (1 • K.d i j ▷ (tensorUnit C c).X 0 ≫ K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c j 0 j ⋯) =
    K.d i j ≫ (ρ_ (K.X j)).inv ≫ K.X j ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) j 0 j ⋯

Proof state:
case pos
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 j : I
hij : c.Rel i j
⊢ K.rightUnitor'.inv i ≫ (K.tensorObj (tensorUnit C c)).d i j = K.d i j ≫ K.rightUnitor'.inv j

Tactic:
simp only [rightUnitor'_inv, assoc, mapBifunctor.d_eq,
  Preadditive.comp_add, mapBifunctor.ι_D₁, mapBifunctor.ι_D₂,
  tensor_unit_d₂, comp_zero, add_zero]

Result:
case pos
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 j : I
hij : c.Rel i j
⊢ (ρ_ (K.X i)).inv ≫
      K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ mapBifunctor.d₁ K (tensorUnit C c) (curriedTensor C) c i 0 j =
    K.d i j ≫ (ρ_ (K.X j)).inv ≫ K.X j ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) j 0 j ⋯

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 j : I
hij : c.Rel i j
⊢ c.π c c (j, 0) = j

Tactic:
simp

Result:
no goals

Proof state:
case pos
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 j : I
hij : c.Rel i j
⊢ (ρ_ (K.X i)).inv ≫
      K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ mapBifunctor.d₁ K (tensorUnit C c) (curriedTensor C) c i 0 j =
    K.d i j ≫ (ρ_ (K.X j)).inv ≫ K.X j ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) j 0 j ⋯

Tactic:
rw [mapBifunctor.d₁_eq _ _ _ _ hij _ _ (by simp)]

Result:
case pos
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 j : I
hij : c.Rel i j
⊢ (ρ_ (K.X i)).inv ≫
      K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫
        (c.ε₁ c c (i, 0) •
          ((curriedTensor C).map (K.d i j)).app ((tensorUnit C c).X 0) ≫
            K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c j 0 j ⋯) =
    K.d i j ≫ (ρ_ (K.X j)).inv ≫ K.X j ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) j 0 j ⋯

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 j : I
⊢ K.rightUnitor'.inv i ≫ (K.tensorObj (tensorUnit C c)).d i j = K.d i j ≫ K.rightUnitor'.inv j

Tactic:
by_cases hij : c.Rel i j

Result:
case pos
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 j : I
hij : c.Rel i j
⊢ K.rightUnitor'.inv i ≫ (K.tensorObj (tensorUnit C c)).d i j = K.d i j ≫ K.rightUnitor'.inv j

case neg
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 j : I
hij : ¬c.Rel i j
⊢ K.rightUnitor'.inv i ≫ (K.tensorObj (tensorUnit C c)).d i j = K.d i j ≫ K.rightUnitor'.inv j

Proof state:
case neg
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 j : I
hij : ¬c.Rel i j
⊢ K.rightUnitor'.inv i ≫ (K.tensorObj (tensorUnit C c)).d i j = K.d i j ≫ K.rightUnitor'.inv j

Tactic:
simp only [shape _ _ _ hij, comp_zero, zero_comp]

Result:
no goals