-- 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
A₁ A₂ A₃ : C
inst_2 : Closed.{v, u} A₁
inst_3 : Closed.{v, u} A₂
inst_4 : Closed.{v, u} A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
rw :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
rw₁ :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂)
        ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₂) :
            (a : tensorLeft A₂ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₂)
          (Functor.map (tensoringLeft C) g))
        (pre f) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
rw₂ :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂)
        ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₂) :
            (a : tensorLeft A₂ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₂)
          (Functor.map (tensoringLeft C) g))
        ((conjugateEquiv (ihom.adjunction A₂) (ihom.adjunction A₁) :
            (a : tensorLeft A₁ ⟶ tensorLeft A₂) → ihom A₂ ⟶ ihom A₁)
          (Functor.map (tensoringLeft C) f)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
rw₃ :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) f ≫ Functor.map (tensoringLeft C) g) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁)) (pre (f ≫ g))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f))
have rw₄ : Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) : (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
      (Functor.map (tensoringLeft C) f ≫ Functor.map (tensoringLeft C) g) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) : (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
      (Functor.map (tensoringLeft C) f ≫ Functor.map (tensoringLeft C) g) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
Tactic: rw [pre, pre, pre, conjugateEquiv_comp, (tensoringLeft C).map_comp]