-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : X ⟶ Y
g : Y ⟶ Z
rw :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      curry' f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
          (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' g) (comp X Y Z)
rw₁ :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      curry' f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) g
rw₂ :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))
        (Iso.hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ curry' f ≫ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)))
        (Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) g)
rw₃ :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))
          (curry' f ≫ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)))
          (Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) g)
rw₄ :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        curry' f ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))
            (Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)))
            (Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) g)
rw₅ :
  Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry' (f ≫ g))
    (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ curry' f ≫ Functor.map (ihom X) g)
rw₆ :
  Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry' (f ≫ g))
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))
      (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))))
      (Iso.hom (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ curry' f ≫ Functor.map (ihom X) g))
⊢ Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry' (f ≫ g))
    (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
        (curry' f ⊗ₘ curry' g) (comp X Y Z))
have rw₇ : Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry' (f ≫ g))
  (curry' f ≫ Functor.map (ihom X) g)
Tactic: rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id,
    Category.assoc, Category.assoc, Iso.inv_hom_id_assoc, ← unitors_equal,
    Iso.inv_hom_id_assoc, curry'_ihom_map]