-- 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:
case h
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'))
d : D
⊢ (∀ (y : D) (x : C), IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj x))).app (Opposite.op y))) ↔
    ∀ (d' : D) (c : C), IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

Tactic:
apply forall₂_congr

Result:
case h.h
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'))
d : D
⊢ ∀ (a : D) (b : C),
    IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj b))).app (Opposite.op a)) ↔
      IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ a)).op).app b)

Proof state:
case h.h
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'))
d : D
⊢ ∀ (a : D) (b : C),
    IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj b))).app (Opposite.op a)) ↔
      IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ a)).op).app b)

Tactic:
intro d' c

Result:
case h.h
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'))
d d' : D
c : C
⊢ IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d')) ↔
    IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

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
⊢ [∀ (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 3 → 4
| h => by
  have h' : ∀ d d', IsIso (L.map (d ◁ (adj.unit.app d'))) := by
    intro d d'
    have := braiding_naturality (𝟙 d) (adj.unit.app d')
    rw [← Iso.eq_comp_inv, id_tensorHom] at this
    rw [this]
    simp only [map_comp, id_obj, comp_obj, tensorHom_id, Category.assoc]
    infer_instance
  intro d d'
  have : (adj.unit.app d) ⊗ (adj.unit.app d') =
      (adj.unit.app d ▷ d') ≫ (((L ⋙ R).obj _) ◁ adj.unit.app d') := by
    simp [← tensorHom_id, ← id_tensorHom, ← tensor_comp]
  rw [this, map_comp]
  infer_instance

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'))
⊢ [∀ (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