-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (α_ K₁ K₂ K₃)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
                (Functor.obj (forget C c) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂))
                (Functor.obj (forget C c) K₃))) ≪≫
          (Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
                  (Functor.obj (forget C c) K₁) (Functor.obj (forget C c) K₂))) ⊗ᵢ
            Iso.refl (Functor.obj (forget C c) K₃))) ≪≫
        α_ (Functor.obj (forget C c) K₁) (Functor.obj (forget C c) K₂) (Functor.obj (forget C c) K₃) ≪≫
          (Iso.refl (Functor.obj (forget C c) K₁) ⊗ᵢ
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
                  (Functor.obj (forget C c) K₂) (Functor.obj (forget C c) K₃))) ≪≫
            Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
                (Functor.obj (forget C c) K₁)
                (Functor.obj (forget C c) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₂ K₃)))).hom
have dsimp : Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
  (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ⊗ₘ
        𝟙 K₃.X)) ≫
    Iso.hom (α_ K₁.X K₂.X K₃.X) ≫
      (𝟙 K₁.X ⊗ₘ
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₂.X
              K₃.X)) ≫
        𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₂ K₃).X)
Tactic: dsimp [forget]