-- 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
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
tfae_3_to_4 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
          (L.map (adj.unit.app d ▷ d')))
    (d d' : D),
    IsIso (X :=
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X :=
          L.obj
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
          (L.map (adj.unit.app d ⊗ₘ adj.unit.app d')))
    (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
      (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
h :
  ∀ (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
      (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
d d' : D
c : C
w₁ :
  Eq (α :=
    (a :
        (fun (X : Type v_1) ↦ X)
          (obj (obj coyoneda (Opposite.op (L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) d')))) c)) →
      (fun (X : Type v_1) ↦ X)
        (obj
          (obj coyoneda
            (Opposite.op (L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))))
          c))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (map coyoneda (Quiver.Hom.op (L.map (adj.unit.app d ▷ d')))) c)) :
      (a : (fun (X : Type v_1) ↦ X) ((coyoneda.obj (Opposite.op (L.obj ((L ⋙ R).obj d ⊗ d')))).obj c)) →
        (fun (X : Type v_1) ↦ X) ((coyoneda.obj (Opposite.op (L.obj ((𝟭 D).obj d ⊗ d')))).obj c))
    (Function.comp (β :=
      Opposite.unop (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d')) ⟶ R.obj c)
      (⇑(Equiv.symm
            (adj.homEquiv
              (Opposite.unop (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d')))
              c)) :
        (a : Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d')) ⟶ R.obj c) →
          L.obj (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) ⟶ c)
      (Function.comp (β :=
        (fun (X : Type v_2) ↦ X)
          (obj (obj coyoneda (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) d'))) (R.obj c)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (map coyoneda (Quiver.Hom.op (adj.unit.app d ▷ d'))) (R.obj c))) :
          (a : (fun (X : Type v_2) ↦ X) ((coyoneda.obj (Opposite.op ((L ⋙ R).obj d ⊗ d'))).obj (R.obj c))) →
            (fun (X : Type v_2) ↦ X) ((coyoneda.obj (Opposite.op ((𝟭 D).obj d ⊗ d'))).obj (R.obj c)))
        (⇑(adj.homEquiv (Opposite.unop (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) d'))) c) :
          (a : L.obj (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) ⟶ c) →
            Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d')) ⟶ R.obj c)))
w₂ :
  Eq (α :=
    obj (obj coyoneda (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) d'))) (R.obj c) ⟶
      obj (obj coyoneda (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d')))
        (R.obj c))
    (NatTrans.app (map coyoneda (Quiver.Hom.op (adj.unit.app d ▷ d'))) (R.obj c))
    (Iso.hom (mapIso (obj yoneda (R.obj c)) (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))) ≫
      NatTrans.app (map coyoneda (Quiver.Hom.op (d' ◁ adj.unit.app d))) (R.obj c) ≫
        Iso.hom
          (mapIso (obj yoneda (R.obj c))
            (β_ (Opposite.op d') (Opposite.op ((𝟭 D : Functor.{v_2, v_2, u_2, u_2} D D).1 d)))))
x :
  (fun (X : Type v_2) ↦ X)
    (obj (obj coyoneda (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) d' ((L ⋙ R).obj d)))) (R.obj c))
⊢ Eq (α :=
    (fun (X : Type v_2) ↦ X)
      (obj (obj coyoneda (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) d' (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))))
        (R.obj c)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (map coyoneda (Quiver.Hom.op (d' ◁ adj.unit.app d))) (R.obj c)) :
          (a : (fun (X : Type v_2) ↦ X) ((coyoneda.obj (Opposite.op (d' ⊗ (L ⋙ R).obj d))).obj (R.obj c))) →
            (fun (X : Type v_2) ↦ X) ((coyoneda.obj (Opposite.op (d' ⊗ (𝟭 D).obj d))).obj (R.obj c)))
        x :
      (fun (X : Type v_2) ↦ X)
        (obj (obj coyoneda (Opposite.op (tensorObj.{v_2, u_2} (𝒞 := inst_1) d' (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))))
          (R.obj c)))
    (Function.comp (β :=
        Opposite.unop (Opposite.op (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) ⟶ obj.{v_2, v_2, u_2, u_2} (ihom d') (R.obj c))
        (⇑(Equiv.symm
              (Adjunction.homEquiv (ihom.adjunction d') (Opposite.unop (Opposite.op (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
                (R.obj c))) :
          (a : Opposite.unop (Opposite.op ((𝟭 D).obj d)) ⟶ (ihom d').obj (R.obj c)) →
            (tensorLeft d').obj (Opposite.unop (Opposite.op ((𝟭 D).obj d))) ⟶ R.obj c)
        (Function.comp (β :=
          (fun (X : Type v_2) ↦ X)
            (obj (obj coyoneda (Opposite.op ((L ⋙ R).obj d))) (obj.{v_2, v_2, u_2, u_2} (ihom d') (R.obj c))))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (map coyoneda (adj.unit.app d).op) (obj.{v_2, v_2, u_2, u_2} (ihom d') (R.obj c)))) :
            (a :
                (fun (X : Type v_2) ↦ X) ((coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).obj ((ihom d').obj (R.obj c)))) →
              (fun (X : Type v_2) ↦ X) ((coyoneda.obj (Opposite.op ((𝟭 D).obj d))).obj ((ihom d').obj (R.obj c))))
          (⇑(Adjunction.homEquiv (ihom.adjunction d') (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) (R.obj c)) :
            (a : (tensorLeft d').obj (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) ⟶ R.obj c) →
              Opposite.unop (Opposite.op ((L ⋙ R).obj d)) ⟶ (ihom d').obj (R.obj c)))
        x :
      obj.{v_2, v_2, u_2, u_2} (tensorLeft d') (Opposite.unop (Opposite.op (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))) ⟶
        R.obj c)
have h₁ : Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) d' d ⟶ R.obj c)
  (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (map (obj yoneda (R.obj c)) (Quiver.Hom.op (d' ◁ adj.unit.app d))) :
          TypeCat.Fun (tensorObj.{v_2, u_2} (𝒞 := inst_1) d' (R.obj (L.obj d)) ⟶ R.obj c)
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) d' d ⟶ R.obj c)) :
        (a : d' ⊗ R.obj (L.obj d) ⟶ R.obj c) → d' ⊗ d ⟶ R.obj c)
      x :
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d' d ⟶ R.obj c)
  (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (tensorLeft d') (obj.{v_2, v_2, u_2, u_2} (ihom d') (R.obj c)))
      (map (tensorLeft d')
        (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (map (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom d') (R.obj c))) (adj.unit.app d).op) :
              TypeCat.Fun (R.obj (L.obj d) ⟶ obj.{v_2, v_2, u_2, u_2} (ihom d') (R.obj c))
                (d ⟶ obj.{v_2, v_2, u_2, u_2} (ihom d') (R.obj c))) :
            (a : R.obj (L.obj d) ⟶ (ihom d').obj (R.obj c)) → d ⟶ (ihom d').obj (R.obj c))
          (NatTrans.app (Adjunction.unit (ihom.adjunction d')) (R.obj (L.obj d)) ≫ map (ihom d') x :
            R.obj (L.obj d) ⟶ obj.{v_2, v_2, u_2, u_2} (ihom d') (R.obj c))))
      (NatTrans.app (Adjunction.counit (ihom.adjunction d')) (R.obj c)) :
    obj.{v_2, v_2, u_2, u_2} (tensorLeft d') d ⟶ R.obj c)
Tactic: simp only [id_obj, op_tensorObj, flip_obj_obj, yoneda_obj_obj, unop_tensorObj, comp_obj,
        flip_map_app, Function.comp_apply, Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]