-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c X Y : C
x : X ⟶ Y
refine_1 :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₁ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ L.map (R.map x) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₂ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫
      L.obj (R.obj c) ◁ L.map (R.map x) ≫ L.obj (R.obj c) ◁ adj.counit.app Y ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₃ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ (L.map (R.map x) ≫ adj.counit.app Y) ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₄ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ (adj.counit.app X ≫ x) ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₅ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ adj.counit.app c ▷ L.obj (R.obj X) ≫ c ◁ (adj.counit.app X ≫ x))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
⊢ Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
have refine_1₆ : Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
  (δ L (R.obj c) (R.obj X) ≫ adj.counit.app c ▷ L.obj (R.obj X) ≫ c ◁ (adj.counit.app X ≫ x))
  (δ L (R.obj c) (R.obj X) ≫ adj.counit.app c ▷ L.obj (R.obj X) ≫ c ◁ adj.counit.app X ≫ c ◁ x)
Tactic: rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]