-- Mathlib/Algebra/Homology/Monoidal.lean
@[reassoc]
lemma leftUnitor'_inv_comm (i j : I) :
    (leftUnitor' K).inv i ≫ (tensorObj (tensorUnit C c) K).d i j =
      K.d i j ≫ (leftUnitor' 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).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ K.leftUnitor'.inv i ≫ ((tensorUnit C c).tensorObj K).d i j = K.d i j ≫ K.leftUnitor'.inv j

Tactic:
simp only [leftUnitor'_inv, assoc, mapBifunctor.d_eq,
  Preadditive.comp_add, mapBifunctor.ι_D₁, mapBifunctor.ι_D₂,
  unit_tensor_d₁, comp_zero, zero_add]

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).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ (λ_ (K.X i)).inv ≫
      (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫ mapBifunctor.d₂ (tensorUnit C c) K (curriedTensor C) c 0 i j =
    K.d i j ≫ (λ_ (K.X j)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X j ≫ (tensorUnit C c).ιTensorObj K 0 j 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).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ c.π c c (0, j) = 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).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ (λ_ (K.X i)).inv ≫
      (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫
        (c.ε 0 • (tensorUnit C c).X 0 ◁ K.d i j ≫ (tensorUnit C c).ιMapBifunctor K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫ (λ_ (K.X j)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X j ≫ (tensorUnit C c).ιTensorObj K 0 j j ⋯

Tactic:
simp only [ComplexShape.ε_zero, one_smul, ← whisker_exchange_assoc,
  id_whiskerLeft, assoc, Iso.inv_hom_id_assoc]

Result:
no goals

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).flip.obj X₂)
i j : I
hij : ¬c.Rel i j
⊢ K.leftUnitor'.inv i ≫ ((tensorUnit C c).tensorObj K).d i j = K.d i j ≫ K.leftUnitor'.inv j

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

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).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ (λ_ (K.X i)).inv ≫
      (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫ mapBifunctor.d₂ (tensorUnit C c) K (curriedTensor C) c 0 i j =
    K.d i j ≫ (λ_ (K.X j)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X j ≫ (tensorUnit C c).ιTensorObj K 0 j 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).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ (λ_ (K.X i)).inv ≫
      (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫
        (c.ε₂ c c (0, i) •
          ((curriedTensor C).obj ((tensorUnit C c).X 0)).map (K.d i j) ≫
            (tensorUnit C c).ιMapBifunctor K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫ (λ_ (K.X j)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X j ≫ (tensorUnit C c).ιTensorObj K 0 j 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).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ (λ_ (K.X i)).inv ≫
      (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫
        (c.ε₂ c c (0, i) •
          ((curriedTensor C).obj ((tensorUnit C c).X 0)).map (K.d i j) ≫
            (tensorUnit C c).ιMapBifunctor K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫ (λ_ (K.X j)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X j ≫ (tensorUnit C c).ιTensorObj K 0 j 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).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ (λ_ (K.X i)).inv ≫
      (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫
        (c.ε 0 • (tensorUnit C c).X 0 ◁ K.d i j ≫ (tensorUnit C c).ιMapBifunctor K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫ (λ_ (K.X j)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X j ≫ (tensorUnit C c).ιTensorObj K 0 j j ⋯