-- Mathlib/CategoryTheory/Closed/Functor.lean
theorem expComparison_whiskerLeft {A A' : C} (f : A' ⟶ A) :
    (expComparison F A).whiskerBottom (pre (F.map f)) =
      (expComparison F A').whiskerTop (pre f)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
⊢ ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) ((tensoringLeft D).map (F.map f))) =
    ((mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) ((tensoringLeft C).map f))

Tactic:
have vcomp1 := mateEquiv_conjugateEquiv_vcomp
  (exp.adjunction A) (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))
  ((prodComparisonNatIso F A).inv) (((curriedTensor D).map (F.map f)))

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
⊢ ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) ((tensoringLeft D).map (F.map f))) =
    ((mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) ((tensoringLeft C).map f))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) ((curriedTensor C).map f))
⊢ (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.mk F (tensorLeft A) (tensorLeft (F.obj A')) F
        (whiskerLeft F ((curriedTensor D).map (F.map f)) ≫ natTrans (prodComparisonNatIso F A).inv)) =
    (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.mk F (tensorLeft A) (tensorLeft (F.obj A')) F
        (natTrans (prodComparisonNatIso F A').inv ≫ whiskerRight ((curriedTensor C).map f) F))

Tactic:
congr 1

Result:
case h.e_6.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) ((curriedTensor C).map f))
⊢ TwoSquare.mk F (tensorLeft A) (tensorLeft (F.obj A')) F
      (whiskerLeft F ((curriedTensor D).map (F.map f)) ≫ natTrans (prodComparisonNatIso F A).inv) =
    TwoSquare.mk F (tensorLeft A) (tensorLeft (F.obj A')) F
      (natTrans (prodComparisonNatIso F A').inv ≫ whiskerRight ((curriedTensor C).map f) F)

Proof state:
case h.e_6.h.h.w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) ((curriedTensor C).map f))
B : C
⊢ prodComparison F A' B ≫ F.map f ▷ F.obj B ≫ inv (prodComparison F A B) = F.map (f ▷ B)

Tactic:
rw [← prodComparison_inv_natural_whiskerRight F f]

Result:
case h.e_6.h.h.w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) ((curriedTensor C).map f))
B : C
⊢ prodComparison F A' B ≫ inv (prodComparison F A' B) ≫ F.map (f ▷ B) = F.map (f ▷ B)