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)))
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'))
⊢ (∀ (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)
have 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)
Tactic: apply forall_congr'
-- 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
⊢ (∀ (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)
have 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)
Tactic: rw [forall_comm]
-- 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
⊢ (∀ (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)
have 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)
Tactic: apply forall₂_congr
-- 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
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'))
have 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')))
Tactic: have := δ _ _ _ ≫= μ_natural L (adj.unit.app 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
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')))
⊢ 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 (α :=
  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
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
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')))
    (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')))
  (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: 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
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),
    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)))
have 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'))
Tactic: rw [((isIso_tfae adj).out 0 3 :)]
-- 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
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
⊢ tensorLeft c ⊣ R ⋙ ihom (R.obj c) ⋙ L
have refine_1 : R ⋙ tensorLeft (R.obj c) ⋙ L ≅ tensorLeft c ⋙ 𝟭 C
Tactic: refine ((ihom.adjunction (R.obj c)).comp adj).restrictFullyFaithful
      (FullyFaithful.ofFullyFaithful R)
      (FullyFaithful.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
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
⊢ tensorLeft c ⊣ R ⋙ ihom (R.obj c) ⋙ L
have refine_2 : 𝟭 C ⋙ R ⋙ ihom (R.obj c) ≅ (R ⋙ ihom (R.obj c) ⋙ L) ⋙ R
Tactic: refine ((ihom.adjunction (R.obj c)).comp adj).restrictFullyFaithful
      (FullyFaithful.ofFullyFaithful R)
      (FullyFaithful.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
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
⊢ R ⋙ tensorLeft (R.obj c) ⋙ L ≅ tensorLeft c ⋙ 𝟭 C
have 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)
Tactic: refine NatIso.ofComponents (fun _ ↦ (μIso L _ _).symm ≪≫
        asIso ((adj.counit.app _) ⊗ₘ (adj.counit.app _))) (fun _ ↦ ?_)
-- 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
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 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)
have refine_1 : Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
  (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
  ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
Tactic: dsimp
-- 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
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 X Y : C
x : X ⟶ Y
⊢ Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
have refine_1 : Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
  (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
  (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
Tactic: rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]
-- 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
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 X Y : C
x : X ⟶ Y
refine_1 :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
⊢ Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
have refine_1₁ : Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
  (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ L.map (R.map x) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
  (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
Tactic: rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]