-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (hypothesis)
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)))
tfae_1_to_3 :
  ∀
    (a :
      ∀ (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),
    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'))
⊢ List.TFAE
    [∀ (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))),
      ∀ (c : C) (d : D),
        IsIso (X := obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c)) (Y :=
          obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) (R.obj c))
          (NatTrans.app (pre (adj.unit.app d)) (R.obj c)),
      ∀ (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'))]
have tfae_2_iff_3 : (∀ (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c)) (Y :=
      obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) (R.obj c))
      (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) ↔
  ∀ (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'))
Tactic: tfae_have 2 ↔ 3 := by
    conv => lhs; intro c d; rw [isIso_iff_isIso_yoneda_map]
    conv => rhs; intro d d'; rw [isIso_iff_isIso_coyoneda_map]
    -- bring the quantifiers out of the `↔`:
    rw [forall_comm]; apply forall_congr'; intro d
    rw [forall_comm]; apply forall₂_congr; intro d' c
    -- `w₁, w₂,` are the two stacked commutative squares in the proof on nLab:
    have w₁ : ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c) =
        (adj.homEquiv _ _).symm ∘
          (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) ∘
            (adj.homEquiv _ _) := by ext; simp
    have w₂ : ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app ⟨d'⟩ : _ → _) =
          ((ihom.adjunction d).homEquiv _ _) ∘
            ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)) ∘
              ((ihom.adjunction ((L ⋙ R).obj d)).homEquiv _ _).symm := by
      rw [← Function.comp_assoc, ((ihom.adjunction ((L ⋙ R).obj d)).homEquiv _ _).eq_comp_symm]
      ext
      simp only [id_obj, yoneda_obj_obj, comp_obj, Function.comp_apply,
        yoneda_map_app, op_tensorObj, flip_obj_obj, yoneda_obj_obj, unop_tensorObj, op_whiskerRight,
        flip_map_app]
      rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit]
      simp
    rw [isIso_iff_bijective, isIso_iff_bijective, w₂, w₁]
    simp