awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
tfae_3_to_4 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
          (L.map (adj.unit.app d ▷ d')))
    (d d' : D),
    IsIso (X :=
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X :=
          L.obj
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
          (L.map (adj.unit.app d ⊗ₘ adj.unit.app d')))
    (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
      (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
tfae_1_to_3 :
  ∀
    (a :
      ∀ (c : C) (d : D),
        IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
          (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
    (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
      (L.map (adj.unit.app d ▷ d'))
h :
  ∀ (a : D),
    (∀ (a_1 : C) (c : D),
        IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj a)) (R.obj a_1))) (Opposite.op c))
          (Y :=
          obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) a)) (R.obj a_1)))
            (Opposite.op c))
          (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app a)) (R.obj a_1))) (Opposite.op c))) ↔
      ∀ (d' : D) (c : C),
        IsIso (X := obj (obj coyoneda (Opposite.op (L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj a) d')))) c)
          (NatTrans.app (map coyoneda (Quiver.Hom.op (L.map (adj.unit.app a ▷ d')))) c)
⊢ (∀ (b : D) (a : C) (c : D),
      IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj b)) (R.obj a))) (Opposite.op c)) (Y :=
        obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) b)) (R.obj a))) (Opposite.op c))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app b)) (R.obj a))) (Opposite.op c))) ↔
    ∀ (d d' : D) (c : C),
      IsIso (X := obj (obj coyoneda (Opposite.op (L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) d')))) c)
        (NatTrans.app (map coyoneda (Quiver.Hom.op (L.map (adj.unit.app d ▷ d')))) c)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
tfae_3_to_4 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
          (L.map (adj.unit.app d ▷ d')))
    (d d' : D),
    IsIso (X :=
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X :=
          L.obj
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
          (L.map (adj.unit.app d ⊗ₘ adj.unit.app d')))
    (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
      (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
tfae_1_to_3 :
  ∀
    (a :
      ∀ (c : C) (d : D),
        IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
          (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
    (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
      (L.map (adj.unit.app d ▷ d'))
d : D
h :
  (∀ (b : D) (a : C),
      IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj a))) (Opposite.op b)) (Y :=
        obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) (R.obj a))) (Opposite.op b))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj a))) (Opposite.op b))) ↔
    ∀ (d' : D) (c : C),
      IsIso (X := obj (obj coyoneda (Opposite.op (L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) d')))) c)
        (NatTrans.app (map coyoneda (Quiver.Hom.op (L.map (adj.unit.app d ▷ d')))) c)
⊢ (∀ (a : C) (c : D),
      IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj a))) (Opposite.op c)) (Y :=
        obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) (R.obj a))) (Opposite.op c))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj a))) (Opposite.op c))) ↔
    ∀ (d' : D) (c : C),
      IsIso (X := obj (obj coyoneda (Opposite.op (L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) d')))) c)
        (NatTrans.app (map coyoneda (Quiver.Hom.op (L.map (adj.unit.app d ▷ d')))) c)

Tactic:
rw [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
tfae_3_to_4 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
          (L.map (adj.unit.app d ▷ d')))
    (d d' : D),
    IsIso (X :=
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X :=
          L.obj
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
          (L.map (adj.unit.app d ⊗ₘ adj.unit.app d')))
    (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
      (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
tfae_1_to_3 :
  ∀
    (a :
      ∀ (c : C) (d : D),
        IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
          (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
    (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
      (L.map (adj.unit.app d ▷ d'))
d : D
h :
  ∀ (a : D) (b : C),
    IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj b))) (Opposite.op a)) (Y :=
        obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) (R.obj b))) (Opposite.op a))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj b))) (Opposite.op a)) ↔
      IsIso (X := obj (obj coyoneda (Opposite.op (L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) a)))) b)
        (NatTrans.app (map coyoneda (Quiver.Hom.op (L.map (adj.unit.app d ▷ a)))) b)
⊢ (∀ (b : D) (a : C),
      IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj a))) (Opposite.op b)) (Y :=
        obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) (R.obj a))) (Opposite.op b))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj a))) (Opposite.op b))) ↔
    ∀ (d' : D) (c : C),
      IsIso (X := obj (obj coyoneda (Opposite.op (L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) d')))) c)
        (NatTrans.app (map coyoneda (Quiver.Hom.op (L.map (adj.unit.app d ▷ d')))) c)

Tactic:
apply forall₂_congr

Premises used: forall₂_congr
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : R.Faithful
inst_6 : R.Full
L : Functor.{v_2, v_1, u_2, u_1} D C
adj : L ⊣ R
tfae_3_to_4 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
          (L.map (adj.unit.app d ▷ d')))
    (d d' : D),
    IsIso (X :=
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  ∀
    (a :
      ∀ (d d' : D),
        IsIso (X :=
          L.obj
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
          (L.map (adj.unit.app d ⊗ₘ adj.unit.app d')))
    (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
      (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
tfae_1_to_3 :
  ∀
    (a :
      ∀ (c : C) (d : D),
        IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
          (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
    (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
      (L.map (adj.unit.app d ▷ d'))
tfae_2_iff_3 :
  (∀ (c : C) (d : D),
      IsIso (X := obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c)) (Y :=
        obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) (R.obj c))
        (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) ↔
    ∀ (d d' : D),
      IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
        (L.map (adj.unit.app d ▷ d'))
⊢ List.TFAE
    [∀ (c : C) (d : D),
        IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
          (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))),
      ∀ (c : C) (d : D),
        IsIso (X := obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c)) (Y :=
          obj.{v_2, v_2, u_2, u_2} (ihom (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)) (R.obj c))
          (NatTrans.app (pre (adj.unit.app d)) (R.obj c)),
      ∀ (d d' : D),
        IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) d'))
          (L.map (adj.unit.app d ▷ d')),
      ∀ (d d' : D),
        IsIso (X :=
          L.obj
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
          (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))]

Tactic:
tfae_finish
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
d d' : D
⊢ Eq (α :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ⟶
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      ((L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      (μ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d') ≫
        L.map (adj.unit.app d ⊗ₘ adj.unit.app d')))

Tactic:
have := δ _ _ _ ≫= μ_natural L (adj.unit.app d) (adj.unit.app d')
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
d d' : D
this :
  Eq (α :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ⟶
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      ((L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      (μ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d') ≫
        L.map (adj.unit.app d ⊗ₘ adj.unit.app d')))
⊢ Eq (α :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ⟶
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      ((L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
rw [δ_μ_assoc] at this

Premises used: CategoryTheory.Functor.Monoidal.δ_μ_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
d d' : D
this :
  Eq (α :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ⟶
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      ((L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
rw :
  IsIso (X :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
    (Y := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      ((L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
⊢ IsIso (X :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
    (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
d d' : D
this :
  Eq (α :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ⟶
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      ((L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
⊢ IsIso (X :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
    (Y := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d')))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d))
        (L.obj (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (δ L (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d'))
      ((L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d')))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c : C
d : D
revert :
  ∀ (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
      (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
⊢ IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
    (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))

Tactic:
revert c d
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
rw :
  ∀ (d d' : D),
    IsIso (X :=
      L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
⊢ ∀ (c : C) (d : D),
    IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
      (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))

Tactic:
rw [((isIso_tfae adj).out 0 3 :)]

Premises used: List.TFAE.out, OfNat.ofNat, CategoryTheory.Monoidal.Reflective.isIso_tfae
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
d d' : D
⊢ IsIso (X :=
    L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
    (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c : C
refine_1 : R ⋙ tensorLeft (R.obj c) ⋙ L ≅ tensorLeft c ⋙ 𝟭 C
refine_2 : 𝟭 C ⋙ R ⋙ ihom (R.obj c) ≅ (R ⋙ ihom (R.obj c) ⋙ L) ⋙ R
⊢ tensorLeft c ⊣ R ⋙ ihom (R.obj c) ⋙ L

Tactic:
refine ((ihom.adjunction (R.obj c)).comp adj).restrictFullyFaithful
      (FullyFaithful.ofFullyFaithful R)
      (FullyFaithful.id _) ?_ ?_

Premises used: CategoryTheory.Adjunction.restrictFullyFaithful, CategoryTheory.Functor.FullyFaithful.id, CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.comp, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c : C
refine_1 :
  ∀ {X Y : C} (x : X ⟶ Y),
    Eq (α := (R ⋙ tensorLeft (R.obj c) ⋙ L).obj X ⟶ obj.{v_1, v_1, u_1, u_1} (tensorLeft c ⋙ 𝟭 C) Y)
      ((R ⋙ tensorLeft (R.obj c) ⋙ L).map x ≫
        Iso.hom
          ((fun (x : C) ↦
              (Iso.symm (μIso L (R.obj c) (R.obj x)) ≪≫ asIso (adj.counit.app c ⊗ₘ adj.counit.app x) :
                (R ⋙ tensorLeft (R.obj c) ⋙ L).obj x ≅ obj.{v_1, v_1, u_1, u_1} (tensorLeft c ⋙ 𝟭 C) x))
            Y))
      (Iso.hom
          ((fun (x : C) ↦
              (Iso.symm (μIso L (R.obj c) (R.obj x)) ≪≫ asIso (adj.counit.app c ⊗ₘ adj.counit.app x) :
                (R ⋙ tensorLeft (R.obj c) ⋙ L).obj x ≅ obj.{v_1, v_1, u_1, u_1} (tensorLeft c ⋙ 𝟭 C) x))
            X) ≫
        map (tensorLeft c ⋙ 𝟭 C) x)
⊢ R ⋙ tensorLeft (R.obj c) ⋙ L ≅ tensorLeft c ⋙ 𝟭 C

Tactic:
refine NatIso.ofComponents (fun _ ↦ (μIso L _ _).symm ≪≫
        asIso ((adj.counit.app _) ⊗ₘ (adj.counit.app _))) (fun _ ↦ ?_)

Premises used: CategoryTheory.Iso.trans, CategoryTheory.asIso, CategoryTheory.NatIso.ofComponents