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
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)
    (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))))
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) (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)) (compTranspose w x z))
Tactic: rw [uncurry_curry, uncurry_curry]
-- 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)
    (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) (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)) (compTranspose 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
            (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
              NatTrans.app (ihom.ev w) x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ NatTrans.app (ihom.ev x) y) ▷
          Functor.obj.{v, v, u, u} (ihom y) z)
      (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
        NatTrans.app (ihom.ev w) y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ NatTrans.app (ihom.ev 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
          (Iso.inv (α_ x (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
            NatTrans.app (ihom.ev x) y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ NatTrans.app (ihom.ev y) z))
    (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) z)) ≫
      NatTrans.app (ihom.ev w) x ▷ Functor.obj.{v, v, u, u} (ihom x) z ≫ NatTrans.app (ihom.ev x) z))
Tactic: simp only [compTranspose_eq]
-- 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 : C
inst_2 : Closed.{v, u} X
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) X) (curry (Iso.hom (ρ_ X) ≫ 𝟙 X))
    (id X)
have rw : Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) X) (curry (Iso.hom (ρ_ X))) (id X)
Tactic: rw [Category.comp_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
X Y : C
inst_2 : Closed.{v, u} X
f : X ⟶ Y
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y)) (X ◁ curry' f)
      (NatTrans.app (ihom.ev X) Y))
    (Iso.hom (ρ_ X) ≫ f)
have dsimp : Eq (α := tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶ Y)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))
    (X ◁ curry (Iso.hom (ρ_ X) ≫ f)) (NatTrans.app (ihom.ev X) Y))
  (Iso.hom (ρ_ X) ≫ f)
Tactic: dsimp [curry']
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (Functor.obj.{v, v, u, u} (ihom Y) Z) ⟶
      Functor.obj.{v, v, u, u} (ihom X) Z)
    (curry' f ▷ Functor.obj.{v, v, u, u} (ihom Y) Z ≫ comp X Y Z)
    (Iso.hom (λ_ (Functor.obj.{v, v, u, u} (ihom Y) Z)) ≫ NatTrans.app (pre f) Z)
have rw : Eq (α := Functor.obj.{v, v, u, u} (ihom Y) Z ⟶ Functor.obj.{v, v, u, u} (ihom X) Z)
  (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom Y) Z)) ≫ curry' f ▷ Functor.obj.{v, v, u, u} (ihom Y) Z ≫ comp X Y Z)
  (NatTrans.app (pre f) Z)
Tactic: rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id_assoc]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : X ⟶ Y
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom Y) Z ⟶ Functor.obj.{v, v, u, u} (ihom X) Z)
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom Y) Z)) ≫ curry' f ▷ Functor.obj.{v, v, u, u} (ihom Y) Z ≫ comp X Y Z)
    (NatTrans.app (pre f) Z)
have a : uncurry
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom Y) Z)) ≫ curry' f ▷ Functor.obj.{v, v, u, u} (ihom Y) Z ≫ comp X Y Z) =
  uncurry (NatTrans.app (pre f) 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
X Y Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
⊢ CategoryStruct.comp (Y :=
      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 X) Y ◁ curry' f) (comp X Y Z) =
    Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) f
have rw : 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) Z))
      (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' f) (comp X Y Z) =
  Functor.map (ihom X) f
Tactic: rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id_assoc]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
⊢ 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) Z))
        (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' f) (comp X Y Z) =
    Functor.map (ihom X) f
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) Z))
        (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' f) (comp X Y Z)) =
  uncurry (Functor.map (ihom X) f)
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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
⊢ 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) Z))
          (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' f) (comp X Y Z)) =
    uncurry (Functor.map (ihom X) f)
have a : X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
    Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
          (Functor.obj.{v, v, u, u} (𝟭 C) Y ◁ curry' f) (NatTrans.app (ihom.ev Y) Z) =
  NatTrans.app (ihom.ev X) Y ≫ f
Tactic: rw [uncurry_ihom_map, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry,
    compTranspose_eq, associator_inv_naturality_right_assoc, whisker_exchange_assoc]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
⊢ X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
            (Functor.obj.{v, v, u, u} (𝟭 C) Y ◁ curry' f) (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f
have a : X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
    Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (Functor.obj.{v, v, u, u} (ihom Y) Z)) (Y ◁ curry' f)
          (NatTrans.app (ihom.ev Y) Z) =
  NatTrans.app (ihom.ev X) Y ≫ f
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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
⊢ X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (Functor.obj.{v, v, u, u} (ihom Y) Z)) (Y ◁ curry' f)
            (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f
have a : X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
    Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
  NatTrans.app (ihom.ev X) Y ≫ f
Tactic: rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv,
    MonoidalCategory.whiskerRight_id_assoc, Category.assoc,
    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
a :
  X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
    NatTrans.app (ihom.ev X) Y ≫ f
⊢ X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (Functor.obj.{v, v, u, u} (ihom Y) Z)) (Y ◁ curry' f)
            (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f
have a₁ : (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
      Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
    Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
  NatTrans.app (ihom.ev X) Y ≫ f
Tactic: rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv,
    MonoidalCategory.whiskerRight_id_assoc, Category.assoc,
    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
a :
  X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
    NatTrans.app (ihom.ev X) Y ≫ f
a₁ :
  (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
        Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
    NatTrans.app (ihom.ev X) Y ≫ f
⊢ X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (Functor.obj.{v, v, u, u} (ihom Y) Z)) (Y ◁ curry' f)
            (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f
have a₂ : (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
      Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
    Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
        NatTrans.app (ihom.ev X) Y ≫
          CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (Iso.inv (ρ_ Y))
            (Iso.hom (ρ_ Y) ≫ f) =
  NatTrans.app (ihom.ev X) Y ≫ f
Tactic: rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv,
    MonoidalCategory.whiskerRight_id_assoc, Category.assoc,
    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
a :
  X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
    NatTrans.app (ihom.ev X) Y ≫ f
a₁ :
  (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
        Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
    NatTrans.app (ihom.ev X) Y ≫ f
a₂ :
  (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
        Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
          NatTrans.app (ihom.ev X) Y ≫
            CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (Iso.inv (ρ_ Y))
              (Iso.hom (ρ_ Y) ≫ f) =
    NatTrans.app (ihom.ev X) Y ≫ f
⊢ X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (Functor.obj.{v, v, u, u} (ihom Y) Z)) (Y ◁ curry' f)
            (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f
have a₃ : Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
    Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
          NatTrans.app (ihom.ev X) Y ≫
            CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (Iso.inv (ρ_ Y))
              (Iso.hom (ρ_ Y) ≫ f) =
  NatTrans.app (ihom.ev X) Y ≫ f
Tactic: rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv,
    MonoidalCategory.whiskerRight_id_assoc, Category.assoc,
    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry' (f ≫ g))
    (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
        (curry' f ⊗ₘ curry' g) (comp X Y Z))
have rw : curry' (f ≫ g) =
  Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
    curry' f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
      CategoryStruct.comp (Y :=
        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 X) Y ◁ curry' g) (comp X Y Z)
Tactic: rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id,
    Category.assoc, Category.assoc, Iso.inv_hom_id_assoc, ← unitors_equal,
    Iso.inv_hom_id_assoc, curry'_ihom_map]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : X ⟶ Y
g : Y ⟶ Z
rw :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      curry' f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        CategoryStruct.comp (Y :=
          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 X) Y ◁ curry' g) (comp X Y Z)
⊢ Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry' (f ≫ g))
    (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
        (curry' f ⊗ₘ curry' g) (comp X Y Z))
have rw₁ : curry' (f ≫ g) =
  Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
    curry' f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
      Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) g
Tactic: rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id,
    Category.assoc, Category.assoc, Iso.inv_hom_id_assoc, ← unitors_equal,
    Iso.inv_hom_id_assoc, curry'_ihom_map]
-- 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : X ⟶ Y
g : Y ⟶ Z
rw :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      curry' f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        CategoryStruct.comp (Y :=
          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 X) Y ◁ curry' g) (comp X Y Z)
rw₁ :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      curry' f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) g
⊢ Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry' (f ≫ g))
    (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
        (curry' f ⊗ₘ curry' g) (comp X Y Z))
have rw₂ : curry' (f ≫ g) =
  Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
    CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))
      (Iso.hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ curry' f ≫ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)))
      (Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) g)
Tactic: rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id,
    Category.assoc, Category.assoc, Iso.inv_hom_id_assoc, ← unitors_equal,
    Iso.inv_hom_id_assoc, curry'_ihom_map]