awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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)))
h :
  ∀ (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'))
have rw : ∀ (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 [isIso_iff_isIso_coyoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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'))
| (∀ (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'))
have lhs : ∀ (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))
Tactic: lhs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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'))
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))
have rw : ∀ (c_1 : D),
  IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c))) (Opposite.op c_1)) (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 c))) (Opposite.op c_1))
    (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) (Opposite.op c_1))
Tactic: rw [isIso_iff_isIso_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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'))
| (∀ (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'))
have intro : ∀ (c : C) (d : D) (c_1 : D),
  IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c))) (Opposite.op c_1)) (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 c))) (Opposite.op c_1))
    (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) (Opposite.op c_1))
Tactic: lhs; intro c d; rw [isIso_iff_isIso_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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'))
⊢ (∀ (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'))
have conv : (∀ (c : C) (d c_1 : D),
    IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c))) (Opposite.op c_1)) (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 c))) (Opposite.op c_1))
      (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) (Opposite.op c_1))) ↔
  ∀ (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'))
Tactic: conv => lhs; intro c d; rw [isIso_iff_isIso_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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'))
| (∀ (c : C) (d c_1 : D),
      IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c))) (Opposite.op c_1)) (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 c)))
          (Opposite.op c_1))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) (Opposite.op c_1))) ↔
    ∀ (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'))
have rhs : ∀ (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'))
Tactic: rhs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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' : 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'))
have rw : ∀ (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 [isIso_iff_isIso_coyoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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'))
| (∀ (c : C) (d c_1 : D),
      IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c))) (Opposite.op c_1)) (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 c)))
          (Opposite.op c_1))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) (Opposite.op c_1))) ↔
    ∀ (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'))
have intro : ∀ (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: rhs; intro d d'; rw [isIso_iff_isIso_coyoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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'))
⊢ (∀ (c : C) (d c_1 : D),
      IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c))) (Opposite.op c_1)) (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 c)))
          (Opposite.op c_1))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) (Opposite.op c_1))) ↔
    ∀ (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'))
have conv : (∀ (c : C) (d c_1 : D),
    IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c))) (Opposite.op c_1)) (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 c))) (Opposite.op c_1))
      (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) (Opposite.op c_1))) ↔
  ∀ (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: conv => rhs; intro d d'; rw [isIso_iff_isIso_coyoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
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'))
⊢ (∀ (c : C) (d c_1 : D),
      IsIso (X := obj (obj yoneda (obj.{v_2, v_2, u_2, u_2} (ihom ((L ⋙ R).obj d)) (R.obj c))) (Opposite.op c_1)) (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 c)))
          (Opposite.op c_1))
        (NatTrans.app (map yoneda (NatTrans.app (pre (adj.unit.app d)) (R.obj c))) (Opposite.op c_1))) ↔
    ∀ (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)
have rw : (∀ (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: rw [forall_comm]