-- Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean
theorem isIso_tfae : List.TFAE
    [ ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
    , ∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c))
    , ∀ (d d' : D), IsIso (L.map ((adj.unit.app d) ▷ d'))
    , ∀ (d d' : D), IsIso (L.map ((adj.unit.app d) ⊗ (adj.unit.app d')))]

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
⊢ [∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c))),
      ∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c)),
      ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')),
      ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))].TFAE

Tactic:
tfae_have 1 → 3
| h, d, d' => by
  rw [isIso_iff_isIso_coyoneda_map]
  intro c
  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
  rw [w₁, isIso_iff_bijective]
  simp only [comp_obj, coyoneda_obj_obj, id_obj, EquivLike.comp_bijective,
    EquivLike.bijective_comp]
  have w₂ : ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)) =
      ((yoneda.obj (R.obj c)).mapIso (β_ _ _)).hom ∘
        ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c)) ∘
          ((yoneda.obj (R.obj c)).mapIso (β_ _ _)).hom := by ext; simp
  rw [w₂, ← types_comp, ← types_comp, ← isIso_iff_bijective]
  refine IsIso.comp_isIso' (IsIso.comp_isIso' inferInstance ?_) inferInstance
  have w₃ : ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c)) =
      ((ihom.adjunction d').homEquiv _ _).symm ∘
        ((coyoneda.map (adj.unit.app _).op).app _) ∘ (ihom.adjunction d').homEquiv _ _ := by
    ext
    simp only [id_obj, op_tensorObj, coyoneda_obj_obj, unop_tensorObj, comp_obj,
      coyoneda_map_app, Quiver.Hom.unop_op, Function.comp_apply,
      Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]
    simp
  rw [w₃, isIso_iff_bijective]
  simp only [comp_obj, op_tensorObj, coyoneda_obj_obj, unop_tensorObj, id_obj,
    yoneda_obj_obj, tensorLeft_obj, EquivLike.comp_bijective, EquivLike.bijective_comp]
  have w₄ : (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj ⟨d⟩).map (adj.unit.app ((ihom d').obj (R.obj c))) =
        (coyoneda.obj ⟨(L ⋙ R).obj d⟩).map (adj.unit.app ((ihom d').obj (R.obj c))) ≫
          (coyoneda.map (adj.unit.app d).op).app _ := by simp
  rw [← isIso_iff_bijective]
  suffices IsIso ((coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj ⟨d⟩).map (adj.unit.app ((ihom d').obj (R.obj c)))) from
    IsIso.of_isIso_comp_right _ ((coyoneda.obj ⟨d⟩).map (adj.unit.app ((ihom d').obj (R.obj c))))
  rw [w₄]
  refine IsIso.comp_isIso' inferInstance ?_
  constructor
  refine ⟨fun f ↦ R.map ((adj.homEquiv _ _).symm f), ?_, by ext; simp⟩
  ext f
  simp only [comp_obj, coyoneda_obj_obj, id_obj, Adjunction.homEquiv_counit,
    map_comp, types_comp_apply, coyoneda_map_app, Quiver.Hom.unop_op, Category.assoc,
    types_id_apply]
  have : f = R.map (R.preimage f) := by simp
  rw [this]
  simp [← map_comp, ← map_comp_assoc, -map_preimage]

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
⊢ [∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c))),
      ∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c)),
      ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')),
      ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))].TFAE

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
⊢ IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

Tactic:
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

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  (coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)