-- Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean
private lemma adjRetraction_is_retraction (c : C) (d : D)
    [IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))] :
    adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetraction adj c d = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
this :
  d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ CategoryTheory.Monoidal.Reflective.adjRetractionAux adj c d =
    (ihom.ev d).app (R.obj c)
⊢ adj.unit.app ((ihom d).obj (R.obj c)) ≫ CategoryTheory.Monoidal.Reflective.adjRetraction adj c d =
    𝟙 ((𝟭 D).obj ((ihom d).obj (R.obj c)))

Tactic:
simp only [id_obj, comp_obj, adjRetraction, ← curry_natural_left, this]

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
this :
  d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ CategoryTheory.Monoidal.Reflective.adjRetractionAux adj c d =
    (ihom.ev d).app (R.obj c)
⊢ curry ((ihom.ev d).app (R.obj c)) = 𝟙 ((ihom d).obj (R.obj c))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ CategoryTheory.Monoidal.Reflective.adjRetractionAux adj c d =
    (ihom.ev d).app (R.obj c)

Tactic:
simp only [id_obj, comp_obj, adjRetractionAux, Functor.map_inv, Functor.comp_map,
  braiding_naturality_right_assoc]

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      adj.unit.app ((ihom d).obj (R.obj c)) ▷ d ≫
        R.obj (L.obj ((ihom d).obj (R.obj c))) ◁ adj.unit.app d ≫
          adj.unit.app (R.obj (L.obj ((ihom d).obj (R.obj c))) ⊗ R.obj (L.obj d)) ≫
            inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))) ≫
              R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom) ≫
                R.map (L.map ((ihom.ev d).app (R.obj c))) ≫ inv (adj.unit.app (R.toPrefunctor.1 c)) =
    (ihom.ev d).app (R.obj c)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ adj.unit.app ((ihom d).obj (R.obj c)) ≫ CategoryTheory.Monoidal.Reflective.adjRetraction adj c d =
    𝟙 ((𝟭 D).obj ((ihom d).obj (R.obj c)))

Tactic:
suffices (_ ◁ adj.unit.app _) ≫ adjRetractionAux adj c d = (ihom.ev _).app _ by
  simp only [id_obj, comp_obj, adjRetraction, ← curry_natural_left, this]
  simp [curry_eq]

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ CategoryTheory.Monoidal.Reflective.adjRetractionAux adj c d =
    (ihom.ev d).app (R.obj c)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      (((((adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d) ≫
                adj.unit.app (R.obj (L.obj ((ihom d).obj (R.obj c))) ⊗ R.obj (L.obj d))) ≫
              inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d)))) ≫
            R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)) ≫
          R.map (L.map ((ihom.ev d).app (R.obj c)))) ≫
        inv (adj.unit.app (R.toPrefunctor.1 c)) =
    (ihom.ev d).app (R.obj c)

Tactic:
slice_lhs 2 4 =>
  rw [← adj.unit_naturality_assoc]

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      (((adj.unit.app ((ihom d).obj (R.obj c) ⊗ d) ≫
              R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d)) ≫
                inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d)))) ≫
            R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)) ≫
          R.map (L.map ((ihom.ev d).app (R.obj c)))) ≫
        inv (adj.unit.app (R.toPrefunctor.1 c)) =
    (ihom.ev d).app (R.obj c)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, 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
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
this :
  d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ CategoryTheory.Monoidal.Reflective.adjRetractionAux adj c d =
    (ihom.ev d).app (R.obj c)
⊢ curry ((ihom.ev d).app (R.obj c)) = 𝟙 ((ihom d).obj (R.obj c))

Tactic:
simp [curry_eq]

Result:
no goals