-- 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
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
h' : ∀ (d d' : D), IsIso (L.map (d ◁ adj.unit.app d'))
d d' : D
this : adj.unit.app d ⊗ adj.unit.app d' = adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'
⊢ IsIso (L.map (adj.unit.app d ⊗ adj.unit.app d'))

Tactic:
rw [this, map_comp]

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
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
h' : ∀ (d d' : D), IsIso (L.map (d ◁ adj.unit.app d'))
d d' : D
this : adj.unit.app d ⊗ adj.unit.app d' = adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'
⊢ IsIso (L.map (adj.unit.app d ▷ d') ≫ L.map ((L ⋙ R).obj d ◁ adj.unit.app d'))

Proof state:
case out.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)))
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)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).toPrefunctor.1 d)))).hom ∘
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ∘
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).toPrefunctor.1 d)) (Opposite.op d'))).hom
w₃ :
  (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) =
    ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d))) (R.obj c)).symm ∘
      (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ∘
        ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) (R.obj c))
w₄ :
  (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj (Opposite.op d)).map (adj.unit.app ((ihom d').obj (R.obj c))) =
    (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).map (adj.unit.app ((ihom d').obj (R.obj c))) ≫
      (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
f : (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).obj ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
⊢ ((coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c))) ≫ fun f =>
        R.map ((adj.homEquiv d (L.obj ((ihom d').obj (R.obj c)))).symm f))
      f =
    𝟙 ((coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).obj ((L ⋙ R).obj ((ihom d').obj (R.obj c)))) f

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

Result:
case out.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)))
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)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).toPrefunctor.1 d)))).hom ∘
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ∘
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).toPrefunctor.1 d)) (Opposite.op d'))).hom
w₃ :
  (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) =
    ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d))) (R.obj c)).symm ∘
      (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ∘
        ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) (R.obj c))
w₄ :
  (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj (Opposite.op d)).map (adj.unit.app ((ihom d').obj (R.obj c))) =
    (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).map (adj.unit.app ((ihom d').obj (R.obj c))) ≫
      (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
f : (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).obj ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
⊢ R.map (L.map (adj.unit.app d)) ≫ R.map (L.map f) ≫ R.map (adj.counit.app (L.obj ((ihom d').obj (R.obj c)))) = f

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)))
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)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).toPrefunctor.1 d)))).hom ∘
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ∘
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).toPrefunctor.1 d)) (Opposite.op d'))).hom
a✝ : (coyoneda.obj (Opposite.op (d' ⊗ (L ⋙ R).obj d))).obj (R.obj c)
⊢ d' ◁ adj.unit.app d ≫ a✝ =
    (tensorLeft d').map (adj.unit.app d ≫ (ihom.adjunction d').unit.app (R.obj (L.obj d)) ≫ (ihom d').map a✝) ≫
      (ihom.adjunction d').counit.app (R.obj c)

Tactic:
simp

Result:
no goals