-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : Functor.{v₁, v₁, u₁, u₂} C D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) B :
        (a : (reflector i).obj (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) ⟶ B) → A ⊗ i.obj (L.obj (A ⟹ i.obj B)) ⟶ i.obj B)
      (CategoryStruct.comp (Y := (reflector i).obj (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)))
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) (L.obj A) (L.obj (i.obj (L.obj (A ⟹ i.obj B)))))
          (prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))))
          (L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))))
        ((Equiv.symm (ir.homEquiv (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)) B) :
            (a : (ihom A ⋙ tensorLeft A).obj (i.obj B) ⟶ i.obj B) →
              (reflector i).obj ((ihom A ⋙ tensorLeft A).obj (i.obj B)) ⟶ B)
          (NatTrans.app (ihom.ev A) (i.obj B)))))
rw :
  Eq (α := (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (A ⟹ i.obj B)) ⟶ B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj (A ⟹ i.obj B)))
      (prodComparison (reflector i) A (A ⟹ i.obj B))
      (CategoryStruct.comp (Y := (reflector i).obj (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)))
        (inv (prodComparison (reflector i) A (A ⟹ i.obj B)))
        ((Equiv.symm (ir.homEquiv (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)) B) :
            (a : (ihom A ⋙ tensorLeft A).obj (i.obj B) ⟶ i.obj B) →
              (reflector i).obj ((ihom A ⋙ tensorLeft A).obj (i.obj B)) ⟶ B)
          (NatTrans.app (ihom.ev A) (i.obj B)))))
    ((Equiv.symm (ir.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) A (A ⟹ i.obj B)) B) :
        (a : A ⊗ (A ⟹ i.obj B) ⟶ i.obj B) → (reflector i).obj (A ⊗ (A ⟹ i.obj B)) ⟶ B)
      (NatTrans.app (ihom.ev A) (i.obj B)))
⊢ η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)

Tactic:
rw [← curry_natural_left, curry_eq_iff, uncurry_id_eq_ev, ← ir.homEquiv_naturality_left,
      ir.homEquiv_apply_eq, Category.assoc, Category.assoc,
      prodComparison_natural_whiskerLeft_assoc, ← whiskerLeft_comp_assoc,
      ir.left_triangle_components, whiskerLeft_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft_assoc, CategoryTheory.MonoidalClosed.curry_natural_left, CategoryTheory.MonoidalClosed.curry_eq_iff, CategoryTheory.MonoidalClosed.uncurry_id_eq_ev, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Adjunction.homEquiv_apply_eq, CategoryTheory.Adjunction.homEquiv_naturality_left, CategoryTheory.Adjunction.left_triangle_components, CategoryTheory.Category.id_comp