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
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))
⊢ 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)) ▷ d ≫
        R.obj (L.obj (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)
have slice_lhs : 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 3 =>
    simp only [← id_tensorHom, ← tensorHom_id, tensorHom_comp_tensorHom, Category.id_comp,
      Category.comp_id]
-- 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
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))
| (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)))
have a : 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)))
Tactic: rw [← adj.unit_naturality_assoc]
-- 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
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 (α := 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))
have 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))
Tactic: slice_lhs 2 4 =>
    rw [← adj.unit_naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (hypothesis)
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'))
have 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))
Tactic: have := braiding_naturality (𝟙 d) (adj.unit.app d')
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (hypothesis)
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))
⊢ 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'))
have 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')))
Tactic: rw [← Iso.eq_comp_inv, id_tensorHom] at this
Cleared hypotheses: this
-- 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
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 (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
    (L.map (d ◁ adj.unit.app d'))
have 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'))))
Tactic: rw [this]
-- 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
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 (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'))))
have 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')))))
Tactic: simp only [map_comp, id_obj, comp_obj, tensorHom_id, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (hypothesis)
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) (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'))
have 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'))
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (hypothesis)
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
⊢ 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'))
have 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')
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]
-- 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
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 ⊗ₘ adj.unit.app d'))
have 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'))
Tactic: rw [this, map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (hypothesis)
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
⊢ 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'))]
have 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'))
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (hypothesis)
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'))
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) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x : C
x_1 : D
x_2 : Reflective R := { toFull := inst_6, toFaithful := inst_5, L := L, adj := adj }
⊢ IsIso (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (obj.{v_2, v_2, u_2, u_2} (ihom x_1) (R.obj x)))
    (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom x_1) (R.obj x)))
have this : IsIso adj.toMonad.μ
Tactic: have : IsIso adj.toMonad.μ := μ_iso_of_reflective (R := R)
-- 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'))
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) (obj.{v_2, v_2, u_2, u_2} (𝟭 D) d')))
      (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x : C
x_1 : D
x_2 : Reflective R := { toFull := inst_6, toFaithful := inst_5, L := L, adj := adj }
this : IsIso adj.toMonad.μ
⊢ IsIso (X := obj.{v_2, v_2, u_2, u_2} (ihom x_1) (R.obj x))
    (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom x_1) (R.obj x)))
have rw : IsSplitMono (X := obj.{v_2, v_2, u_2, u_2} (ihom x_1) (R.obj x))
  (adj.unit.app (obj.{v_2, v_2, u_2, u_2} (ihom x_1) (R.obj x)))
Tactic: rw [← dsimp% [Adjunction.toMonad] adj.toMonad.isSplitMono_iff_isIso_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (hypothesis)
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'))
⊢ 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'))]
have 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)))
Tactic: tfae_have 4 → 1
  | _, _, _ => by
    -- It is enough to show that the unit is a split monomorphism, and the retraction is given
    -- by `adjRetraction` above.
    let _ : Reflective R := { L := L, adj := adj }
    have : IsIso adj.toMonad.μ := μ_iso_of_reflective (R := R)
    dsimp
    rw [← dsimp% [Adjunction.toMonad] adj.toMonad.isSplitMono_iff_isIso_unit]
    exact ⟨⟨adjRetraction adj _ _, adjRetraction_is_retraction adj _ _⟩⟩