-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A')) F) → TwoSquare (ihom A) F F (ihom (F.obj A')))
        (TwoSquare.whiskerRight (Iso.inv (prodComparisonNatIso F A)) (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerBottom (B := ihom (F.obj A))
        ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
            (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
          (Iso.inv (prodComparisonNatIso F A)))
        ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A')) :
            (a : tensorLeft (F.obj A') ⟶ tensorLeft (F.obj A)) → ihom (F.obj A) ⟶ ihom (F.obj A'))
          (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
vcomp2 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A')) F) → TwoSquare (ihom A) F F (ihom (F.obj A')))
        (TwoSquare.whiskerLeft (Iso.inv (prodComparisonNatIso F A')) (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerTop (T' := ihom A')
        ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A')) :
            (a : TwoSquare F (tensorLeft A') (tensorLeft (F.obj A')) F) → TwoSquare (ihom A') F F (ihom (F.obj A')))
          (Iso.inv (prodComparisonNatIso F A')))
        ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A') :
            (a : tensorLeft A' ⟶ tensorLeft A) → ihom A ⟶ ihom A')
          (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
⊢ Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerBottom (B := ihom (F.obj A))
      ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
        (Iso.inv (prodComparisonNatIso F A)))
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A')) :
          (a : tensorLeft (F.obj A') ⟶ tensorLeft (F.obj A)) → ihom (F.obj A) ⟶ ihom (F.obj A'))
        (Functor.map (tensoringLeft D) (F.map f))))
    (TwoSquare.whiskerTop (T' := ihom A')
      ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A')) :
          (a : TwoSquare F (tensorLeft A') (tensorLeft (F.obj A')) F) → TwoSquare (ihom A') F F (ihom (F.obj A')))
        (Iso.inv (prodComparisonNatIso F A')))
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A') : (a : tensorLeft A' ⟶ tensorLeft A) → ihom A ⟶ ihom A')
        (Functor.map (tensoringLeft C) f)))
have rw : Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')) :
        (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A')) F) → TwoSquare (ihom A) F F (ihom (F.obj A')))
      (TwoSquare.whiskerRight (Iso.inv (prodComparisonNatIso F A)) (Functor.map (curriedTensor D) (F.map f))) :
    TwoSquare (ihom A) F F (ihom (F.obj A')))
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')) :
        (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A')) F) → TwoSquare (ihom A) F F (ihom (F.obj A')))
      (TwoSquare.whiskerLeft (Iso.inv (prodComparisonNatIso F A')) (Functor.map (curriedTensor C) f)) :
    TwoSquare (ihom A) F F (ihom (F.obj A')))
Tactic: rw [← vcomp1, ← vcomp2]