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
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
slice_lhs :
  Eq.{v_2 + 1} (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⟶ R.obj c)
    (Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ≫
      (((adj.unit.app (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d) ≫
              R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)) ≫
                inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)))) ≫
            R.map (L.map (Iso.hom (β_ (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d)))) ≫
          R.map (L.map (NatTrans.app (ihom.ev d) (R.obj c)))) ≫
        inv (adj.unit.app (R.1 c)))
    (NatTrans.app (ihom.ev d) (R.obj c))
⊢ Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⟶ R.obj c)
    (Iso.hom (β_ 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)) ⊗ₘ adj.unit.app d) ≫
                adj.unit.app
                  (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj (L.obj (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))))
                    (R.obj (L.obj d)))) ≫
              inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)))) ≫
            R.map (L.map (Iso.hom (β_ (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d)))) ≫
          R.map (L.map (NatTrans.app (ihom.ev d) (R.obj c)))) ≫
        inv (adj.unit.app (R.1 c)))
    (NatTrans.app (ihom.ev d) (R.obj c))

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

Premises used: CategoryTheory.Adjunction.unit_naturality_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
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
c : C
d : D
inst_7 :
  IsIso (X :=
    L.obj
      (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)))
        (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d)))
    (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ Eq.{v_2 + 1} (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⟶ R.obj c)
    (Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c))) ≫
      (((adj.unit.app (tensorObj.{v_2, u_2} (𝒞 := inst_1) (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d) ≫
              R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)) ≫
                inv (R.map (L.map (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) ⊗ₘ adj.unit.app d)))) ≫
            R.map (L.map (Iso.hom (β_ (obj.{v_2, v_2, u_2, u_2} (ihom d) (R.obj c)) d)))) ≫
          R.map (L.map (NatTrans.app (ihom.ev d) (R.obj c)))) ≫
        inv (adj.unit.app (R.1 c)))
    (NatTrans.app (ihom.ev d) (R.obj c))

Tactic:
simp
-- 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
⊢ ∀ (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:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀
    (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'))

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
h_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'))
h : ∀ (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_1
d d' : D
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d') d)
    ((𝟙 d ⊗ₘ adj.unit.app d') ≫ Iso.hom (β_ d ((L ⋙ R).obj d')))
    (Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ≫ (adj.unit.app d' ⊗ₘ 𝟙 d))

Tactic:
have := braiding_naturality (𝟙 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
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
h_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'))
h : ∀ (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_1
d d' : D
this :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d') d)
    ((𝟙 d ⊗ₘ adj.unit.app d') ≫ Iso.hom (β_ d ((L ⋙ R).obj d')))
    (Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ≫ (adj.unit.app d' ⊗ₘ 𝟙 d))
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) d ((L ⋙ R).obj d'))
    (d ◁ adj.unit.app d')
    ((Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ≫ (adj.unit.app d' ⊗ₘ 𝟙 d)) ≫ Iso.inv (β_ d ((L ⋙ R).obj d')))

Tactic:
rw [← Iso.eq_comp_inv, id_tensorHom] at this

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.Iso.eq_comp_inv
-- 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
h_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'))
h : ∀ (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_1
d d' : D
this :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) d ((L ⋙ R).obj d'))
    (d ◁ adj.unit.app d')
    ((Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ≫ (adj.unit.app d' ⊗ₘ 𝟙 d)) ≫ Iso.inv (β_ d ((L ⋙ R).obj d')))
rw :
  IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
    (L.map
      ((Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ≫ (adj.unit.app d' ⊗ₘ 𝟙 d)) ≫
        Iso.inv (β_ d ((L ⋙ R).obj d'))))
⊢ IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
    (L.map (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
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
h_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'))
h : ∀ (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_1
d d' : D
this :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) d ((L ⋙ R).obj d'))
    (d ◁ adj.unit.app d')
    ((Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ≫ (adj.unit.app d' ⊗ₘ 𝟙 d)) ≫ Iso.inv (β_ d ((L ⋙ R).obj d')))
simp :
  IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d d'))
    (L.map (Iso.hom (β_ d d')) ≫ L.map (adj.unit.app d' ▷ d) ≫ L.map (Iso.inv (β_ d (R.obj (L.obj d')))))
⊢ IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
    (L.map
      ((Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ≫ (adj.unit.app d' ⊗ₘ 𝟙 d)) ≫
        Iso.inv (β_ d ((L ⋙ R).obj d'))))

Tactic:
simp only [map_comp, id_obj, comp_obj, tensorHom_id, Category.assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.MonoidalCategory.tensorHom_id
-- 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
h_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'))
h : ∀ (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_1
d d' : D
this :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) d ((L ⋙ R).obj d'))
    (d ◁ adj.unit.app d')
    ((Iso.hom (β_ d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')) ≫ (adj.unit.app d' ⊗ₘ 𝟙 d)) ≫ Iso.inv (β_ d ((L ⋙ R).obj d')))
⊢ IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d d'))
    (L.map (Iso.hom (β_ d d')) ≫ L.map (adj.unit.app d' ▷ d) ≫ L.map (Iso.inv (β_ d (R.obj (L.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
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
h_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'))
h : ∀ (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_1
⊢ ∀ (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (d ◁ adj.unit.app d'))

Tactic:
have h' : ∀ d d', IsIso (L.map (d ◁ (adj.unit.app d'))) := by
      intro d d'
      have := braiding_naturality (𝟙 d) (adj.unit.app d')
      rw [← Iso.eq_comp_inv, id_tensorHom] at this
      rw [this]
      simp only [map_comp, id_obj, comp_obj, tensorHom_id, Category.assoc]
      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
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
h_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'))
h : ∀ (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_1
h' :
  ∀ (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (d ◁ adj.unit.app d'))
d d' : D
⊢ Eq (α :=
    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') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d'))
    (adj.unit.app d ⊗ₘ adj.unit.app d') (adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d')

Tactic:
simp [← tensorHom_id, ← id_tensorHom, tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_id
-- 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
h_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'))
h : ∀ (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_1
h' :
  ∀ (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (d ◁ adj.unit.app d'))
d d' : D
⊢ Eq (α :=
    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') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d'))
    (adj.unit.app d ⊗ₘ adj.unit.app d') (adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d')

Tactic:
have : (adj.unit.app d) ⊗ₘ (adj.unit.app d') =
        (adj.unit.app d ▷ d') ≫ (((L ⋙ R).obj _) ◁ adj.unit.app d') := by
      simp [← tensorHom_id, ← id_tensorHom, tensorHom_comp_tensorHom]
-- 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
h_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'))
h : ∀ (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_1
h' :
  ∀ (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (d ◁ adj.unit.app d'))
d d' : D
this :
  Eq (α :=
    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') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d'))
    (adj.unit.app d ⊗ₘ adj.unit.app d') (adj.unit.app d ▷ d' ≫ (L ⋙ R).obj 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')))
    (L.map (adj.unit.app d ▷ d') ≫ L.map ((L ⋙ R).obj 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')))
    (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
rw [this, map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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
h_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'))
h : ∀ (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_1
h' :
  ∀ (d d' : D),
    IsIso (X := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) d (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (d ◁ adj.unit.app d'))
d d' : D
this :
  Eq (α :=
    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') ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) ((L ⋙ R).obj d) ((L ⋙ R).obj d'))
    (adj.unit.app d ⊗ₘ adj.unit.app d') (adj.unit.app d ▷ d' ≫ (L ⋙ R).obj 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')))
    (L.map (adj.unit.app d ▷ d') ≫ L.map ((L ⋙ R).obj 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
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
⊢ ∀
    (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'))

Tactic:
tfae_have 3 → 4
  | h => by
    -- We can commute the tensor product in the condition that `L.map ((adj.unit.app d) ▷ d')` is
    -- an isomorphism:
    have h' : ∀ d d', IsIso (L.map (d ◁ (adj.unit.app d'))) := by
      intro d d'
      have := braiding_naturality (𝟙 d) (adj.unit.app d')
      rw [← Iso.eq_comp_inv, id_tensorHom] at this
      rw [this]
      simp only [map_comp, id_obj, comp_obj, tensorHom_id, Category.assoc]
      infer_instance
    intro d d'
    -- We then write the tensor product of the two units as the composition of the whiskered units,
    -- and conclude.
    have : (adj.unit.app d) ⊗ₘ (adj.unit.app d') =
        (adj.unit.app d ▷ d') ≫ (((L ⋙ R).obj _) ◁ adj.unit.app d') := by
      simp [← tensorHom_id, ← id_tensorHom, tensorHom_comp_tensorHom]
    rw [this, map_comp]
    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
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'))
⊢ ∀ (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:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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'))
⊢ ∀ (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:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false