awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : B ⟶ A
X Y : C
g : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
rw :
  uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X)) =
    f ▷ Y ≫ g
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
      (B ◁ CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X))
      (NatTrans.app (ihom.ev B) X) =
    f ▷ Y ≫ g
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
        (B ◁ NatTrans.app (pre f) X))
      (NatTrans.app (ihom.ev B) X) =
    f ▷ Y ≫ g
rw₃ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
        (B ◁ NatTrans.app (pre f) X) (NatTrans.app (ihom.ev B) X)) =
    f ▷ Y ≫ g
⊢ uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X)) =
    uncurry (curry (f ▷ Y ≫ g))
have rw₄ : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
    (f ▷ Functor.obj.{v, v, u, u} (ihom A) X ≫ NatTrans.app (ihom.ev A) X) =
  f ▷ Y ≫ g
Tactic: rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc,
    id_tensor_pre_app_comp_ev, whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : B ⟶ A
X Y : C
g : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
rw :
  uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X)) =
    f ▷ Y ≫ g
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
      (B ◁ CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X))
      (NatTrans.app (ihom.ev B) X) =
    f ▷ Y ≫ g
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
        (B ◁ NatTrans.app (pre f) X))
      (NatTrans.app (ihom.ev B) X) =
    f ▷ Y ≫ g
rw₃ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
        (B ◁ NatTrans.app (pre f) X) (NatTrans.app (ihom.ev B) X)) =
    f ▷ Y ≫ g
rw₄ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
      (f ▷ Functor.obj.{v, v, u, u} (ihom A) X ≫ NatTrans.app (ihom.ev A) X) =
    f ▷ Y ≫ g
⊢ uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X)) =
    uncurry (curry (f ▷ Y ≫ g))
have rw₅ : f ▷ Y ≫
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) X)) (A ◁ curry g)
      (NatTrans.app (ihom.ev A) X) =
  f ▷ Y ≫ g
Tactic: rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc,
    id_tensor_pre_app_comp_ev, whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : B ⟶ A
X Y : C
g : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
rw :
  uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X)) =
    f ▷ Y ≫ g
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
      (B ◁ CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X))
      (NatTrans.app (ihom.ev B) X) =
    f ▷ Y ≫ g
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
        (B ◁ NatTrans.app (pre f) X))
      (NatTrans.app (ihom.ev B) X) =
    f ▷ Y ≫ g
rw₃ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
        (B ◁ NatTrans.app (pre f) X) (NatTrans.app (ihom.ev B) X)) =
    f ▷ Y ≫ g
rw₄ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
      (f ▷ Functor.obj.{v, v, u, u} (ihom A) X ≫ NatTrans.app (ihom.ev A) X) =
    f ▷ Y ≫ g
rw₅ :
  f ▷ Y ≫
      CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) X)) (A ◁ curry g)
        (NatTrans.app (ihom.ev A) X) =
    f ▷ Y ≫ g
⊢ uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X)) =
    uncurry (curry (f ▷ Y ≫ g))
have rw₆ : f ▷ Y ≫ g = f ▷ Y ≫ g
Tactic: rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc,
    id_tensor_pre_app_comp_ev, whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X Y : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X
g : B ⟶ A
⊢ Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (curry (uncurry (f ≫ NatTrans.app (pre g) X)))
    (curry (g ▷ Y ≫ uncurry f))
have rw : Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X) (curry (g ▷ Y ≫ uncurry f))
Tactic: rw [curry_uncurry, ← curry_pre_app, curry_uncurry]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X Y : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X
g : B ⟶ A
rw : Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X) (curry (g ▷ Y ≫ uncurry f))
⊢ Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (curry (uncurry (f ≫ NatTrans.app (pre g) X)))
    (curry (g ▷ Y ≫ uncurry f))
have rw₁ : Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X)
  (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry (uncurry f)) (NatTrans.app (pre g) X))
Tactic: rw [curry_uncurry, ← curry_pre_app, curry_uncurry]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X Y : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X
g : B ⟶ A
rw : Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X) (curry (g ▷ Y ≫ uncurry f))
rw₁ :
  Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X)
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry (uncurry f)) (NatTrans.app (pre g) X))
⊢ Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (curry (uncurry (f ≫ NatTrans.app (pre g) X)))
    (curry (g ▷ Y ≫ uncurry f))
have rw₂ : Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X) (f ≫ NatTrans.app (pre g) X)
Tactic: rw [curry_uncurry, ← curry_pre_app, curry_uncurry]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A)) (pre (𝟙 A)) (𝟙 (ihom A))
have rw : Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))
  ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A) : (a : tensorLeft A ⟶ tensorLeft A) → ihom A ⟶ ihom A)
      (𝟙 (Functor.obj (tensoringLeft C) A)) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))
  (𝟙 (ihom A) : Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))
Tactic: rw [pre, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A₁ A₂ A₃ : C
inst_2 : Closed.{v, u} A₁
inst_3 : Closed.{v, u} A₂
inst_4 : Closed.{v, u} A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁)) (pre (f ≫ g))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f))
have rw : Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) : (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
      (Functor.map (tensoringLeft C) (f ≫ g)) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f) : Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
Tactic: rw [pre, pre, pre, conjugateEquiv_comp, (tensoringLeft C).map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A₁ A₂ A₃ : C
inst_2 : Closed.{v, u} A₁
inst_3 : Closed.{v, u} A₂
inst_4 : Closed.{v, u} A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
rw :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁)) (pre (f ≫ g))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f))
have rw₁ : Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) : (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
      (Functor.map (tensoringLeft C) (f ≫ g)) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  (CategoryStruct.comp (Y := ihom A₂)
      ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₂) :
          (a : tensorLeft A₂ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₂)
        (Functor.map (tensoringLeft C) g))
      (pre f) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
Tactic: rw [pre, pre, pre, conjugateEquiv_comp, (tensoringLeft C).map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A₁ A₂ A₃ : C
inst_2 : Closed.{v, u} A₁
inst_3 : Closed.{v, u} A₂
inst_4 : Closed.{v, u} A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
rw :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
rw₁ :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂)
        ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₂) :
            (a : tensorLeft A₂ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₂)
          (Functor.map (tensoringLeft C) g))
        (pre f) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁)) (pre (f ≫ g))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f))
have rw₂ : Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) : (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
      (Functor.map (tensoringLeft C) (f ≫ g)) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  (CategoryStruct.comp (Y := ihom A₂)
      ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₂) :
          (a : tensorLeft A₂ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₂)
        (Functor.map (tensoringLeft C) g))
      ((conjugateEquiv (ihom.adjunction A₂) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₂) → ihom A₂ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) f)) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
Tactic: rw [pre, pre, pre, conjugateEquiv_comp, (tensoringLeft C).map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A₁ A₂ A₃ : C
inst_2 : Closed.{v, u} A₁
inst_3 : Closed.{v, u} A₂
inst_4 : Closed.{v, u} A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
rw :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
rw₁ :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂)
        ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₂) :
            (a : tensorLeft A₂ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₂)
          (Functor.map (tensoringLeft C) g))
        (pre f) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
rw₂ :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) :
          (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
        (Functor.map (tensoringLeft C) (f ≫ g)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
    (CategoryStruct.comp (Y := ihom A₂)
        ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₂) :
            (a : tensorLeft A₂ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₂)
          (Functor.map (tensoringLeft C) g))
        ((conjugateEquiv (ihom.adjunction A₂) (ihom.adjunction A₁) :
            (a : tensorLeft A₁ ⟶ tensorLeft A₂) → ihom A₂ ⟶ ihom A₁)
          (Functor.map (tensoringLeft C) f)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁)) (pre (f ≫ g))
    (CategoryStruct.comp (Y := ihom A₂) (pre g) (pre f))
have rw₃ : Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) : (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
      (Functor.map (tensoringLeft C) (f ≫ g)) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
  ((conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁) : (a : tensorLeft A₁ ⟶ tensorLeft A₃) → ihom A₃ ⟶ ihom A₁)
      (Functor.map (tensoringLeft C) f ≫ Functor.map (tensoringLeft C) g) :
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A₃) (ihom A₁))
Tactic: rw [pre, pre, pre, conjugateEquiv_comp, (tensoringLeft C).map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X_1 X' Y Y' Z : C
inst_2 : Closed.{v, u} A
inst_3 : MonoidalClosed.{v, u} C
X : Cᵒᵖ
⊢ Functor.IsRightAdjoint.{v, v, u, u} (Functor.obj internalHom X)
have dsimp : Functor.IsRightAdjoint.{v, v, u, u} (ihom (Opposite.unop X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
⊢ Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫ id x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ comp x x y =
    𝟙 (Functor.obj.{v, v, u, u} (ihom x) y)
have a : uncurry (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫ id x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ comp x x y) =
  uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
Tactic: apply uncurry_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
⊢ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) y))
        (Functor.obj.{v, v, u, u} (ihom x) y ◁ id y) (comp x y y) =
    𝟙 (Functor.obj.{v, v, u, u} (ihom x) y)
have a : uncurry
    (Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) y))
        (Functor.obj.{v, v, u, u} (ihom x) y ◁ id y) (comp x y y)) =
  uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
Tactic: apply uncurry_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
⊢ uncurry
      (Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) y))
          (Functor.obj.{v, v, u, u} (ihom x) y ◁ id y) (comp x y y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
have a : NatTrans.app (ihom.ev x) y ≫
    Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (𝟭 C) y)) ≫
      Functor.obj.{v, v, u, u} (𝟭 C) y ◁ id y ≫ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
  uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
Tactic: rw [uncurry_natural_left, uncurry_natural_left, comp_eq, uncurry_curry, compTranspose_eq,
    associator_inv_naturality_right_assoc, ← rightUnitor_tensor_inv_assoc,
    whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc, ← uncurry_id_eq_ev y y]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
⊢ NatTrans.app (ihom.ev x) y ≫
      Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (𝟭 C) y)) ≫
        Functor.obj.{v, v, u, u} (𝟭 C) y ◁ id y ≫ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
have a : NatTrans.app (ihom.ev x) y ≫ Iso.inv (ρ_ y) ≫ y ◁ id y ≫ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
  uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
Tactic: simp only [Functor.id_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
⊢ NatTrans.app (ihom.ev x) y ≫ Iso.inv (ρ_ y) ≫ y ◁ id y ≫ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
have a : NatTrans.app (ihom.ev x) y ≫ Iso.inv (ρ_ y) ≫ uncurry (id y ≫ 𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
  uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
Tactic: rw [← uncurry_natural_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
w x y z : C
inst_2 : Closed.{v, u} w
inst_3 : Closed.{v, u} x
inst_4 : Closed.{v, u} y
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ⟶
      Functor.obj.{v, v, u, u} (ihom w) z)
    (Iso.inv
        (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
          (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      comp w x y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ comp w y z)
    (Functor.obj.{v, v, u, u} (ihom w) x ◁ comp x y z ≫ comp w x z)
have a : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) w
      (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
    z)
  (uncurry
    (Iso.inv
        (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
          (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      comp w x y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ comp w y z))
  (uncurry (Functor.obj.{v, v, u, u} (ihom w) x ◁ comp x y z ≫ comp w x z))
Tactic: apply uncurry_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
w x y z : C
inst_2 : Closed.{v, u} w
inst_3 : Closed.{v, u} x
inst_4 : Closed.{v, u} y
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
      z)
    (uncurry
      (Iso.inv
          (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
            (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
        comp w x y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ comp w y z))
    (uncurry (Functor.obj.{v, v, u, u} (ihom w) x ◁ comp x y z ≫ comp w x z))
have a : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) w
      (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
    z)
  (w ◁
      Iso.inv
        (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
          (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
    CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) y) (Functor.obj.{v, v, u, u} (ihom y) z)))
      (w ◁ curry (compTranspose w x y) ▷ Functor.obj.{v, v, u, u} (ihom y) z) (uncurry (curry (compTranspose w y z))))
  (CategoryStruct.comp (Y :=
    tensorObj.{v, u} (𝒞 := inst) w
      (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) z)))
    (w ◁ Functor.obj.{v, v, u, u} (ihom w) x ◁ curry (compTranspose x y z)) (uncurry (curry (compTranspose w x z))))
Tactic: simp only [uncurry_natural_left, comp_eq]