Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: case a.a.a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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)) ⊗ₘ adj.unit.app d) ≫
    adj.unit.app ((L ⋙ R).obj ((ihom d).obj (R.obj c)) ⊗ (L ⋙ R).obj d) ≫
      inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d)))

pp: case a.a.a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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))
| R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)

pp: case a.a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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))
| R.map (L.map ((ihom.ev d).app (R.obj c)))

pp: case a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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))
| inv (adj.unit.app (R.1 c))

pp: case a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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

Tactic:
rw [← adj.unit_naturality_assoc]

Goal state after:
case a.a.a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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) ⊗ 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)))

case a.a.a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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))
| R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)

case a.a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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))
| R.map (L.map ((ihom.ev d).app (R.obj c)))

case a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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))
| inv (adj.unit.app (R.1 c))

case a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, 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