awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
rw :
  (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷
        U ≫
      ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₁ :
  f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷ U ≫
        ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₂ :
  f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      ((Y₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
⊢ (f.f ⊗ₘ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ (f.f ⊗ₘ g.f)
have rw₃ : ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
    U ◁ f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
      U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
  ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
    U ◁
      (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
Tactic: rw [tensorHom_def, comp_whiskerRight_assoc, whiskerLeft_comm, whiskerRight_comm_assoc,
      MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
rw :
  (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷
        U ≫
      ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₁ :
  f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷ U ≫
        ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₂ :
  f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      ((Y₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₃ :
  ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
⊢ (f.f ⊗ₘ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ (f.f ⊗ₘ g.f)
have rw₄ : ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
    U ◁ f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
      U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
  ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
    U ◁ f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
      U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f
Tactic: rw [tensorHom_def, comp_whiskerRight_assoc, whiskerLeft_comm, whiskerRight_comm_assoc,
      MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ tensorHom f g = whiskerRight f X₂ ≫ Y₁.whiskerLeft g
have w : (tensorHom f g).f = (whiskerRight f X₂ ≫ Y₁.whiskerLeft g).f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : Center.{v₁, u₁} C
⊢ Hom.f (Iso.inv (α_ X Y Z)) =
    Iso.inv
      (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
have hom_inv_id : Iso.hom
      (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
    Hom.f (Iso.inv (α_ X Y Z)) =
  𝟙
    ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
          Z).fst
      (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
Tactic: apply Iso.inv_ext'
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : Center.{v₁, u₁} C
⊢ Iso.hom
        (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
      Hom.f (Iso.inv (α_ X Y Z)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
            Z).fst
        (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
have hom_inv_id : Hom.f
    (𝟙
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
        Z)) =
  𝟙
    ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
          Z).fst
      (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
Tactic: rw [← associator_hom_f, ← comp_f, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
⊢ Hom.f (Iso.inv (λ_ X)) = Iso.inv (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
have hom_inv_id : Iso.hom (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫ Hom.f (Iso.inv (λ_ X)) =
  𝟙
    ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X).fst (β :=
      fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
Tactic: apply Iso.inv_ext'
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
⊢ Iso.hom (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫ Hom.f (Iso.inv (λ_ X)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
have hom_inv_id : Hom.f (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X)) =
  𝟙
    ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X).fst (β :=
      fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
Tactic: rw [← leftUnitor_hom_f, ← comp_f, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
⊢ Hom.f (Iso.inv (ρ_ X)) = Iso.inv (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
have hom_inv_id : Iso.hom (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫ Hom.f (Iso.inv (ρ_ X)) =
  𝟙
    ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))).fst (β :=
      fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
Tactic: apply Iso.inv_ext'
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
⊢ Iso.hom (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫ Hom.f (Iso.inv (ρ_ X)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
have hom_inv_id : Hom.f (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)))) =
  𝟙
    ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))).fst (β :=
      fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
Tactic: rw [← rightUnitor_hom_f, ← comp_f, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Center.{v₁, u₁} C
f : A ⟶ B
i : IsIso f.f
⊢ IsIso f
have change : IsIso (isoMk f).hom
Tactic: change IsIso (isoMk f).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
U : C
⊢ Iso.hom (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷
        U ≫
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y X).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
          U).hom =
    ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
          U).hom ≫
      U ◁
        Iso.hom
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
have dsimp : Iso.hom (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷
      U ≫
    Iso.hom
        (α_ (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          U) ≫
      Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        Iso.inv
            (α_ (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
              (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
              (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) =
  (Iso.hom
        (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          U) ≫
      X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        Iso.inv
            (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
              (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
    U ◁
      Iso.hom
        (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} 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
A X : C
inst_2 : Closed.{v, u} A
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (𝟭 C) X ⟶
      Functor.obj.{v, v, u, u} (ihom A) (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (𝟭 C) X)))
    (curry (𝟙 (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (𝟭 C) X)))) (NatTrans.app (ihom.coev A) X)
have rw : NatTrans.app (ihom.coev A) (Functor.obj.{v, v, u, u} (𝟭 C) X) ≫
    𝟙 (Functor.obj.{v, v, u, u} (ihom A) (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (𝟭 C) X))) =
  NatTrans.app (ihom.coev A) X
Tactic: rw [curry_eq, (ihom A).map_id (A ⊗ _)]
-- 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 Y Y' : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Y'
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) Y) ⟶ Y') (uncurry (Functor.map (ihom A) g))
    (NatTrans.app (ihom.ev A) Y ≫ g)
have a : Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y')
  (curry (uncurry (Functor.map (ihom A) g))) (curry (NatTrans.app (ihom.ev A) Y ≫ g))
Tactic: apply curry_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
A Y Y' : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Y'
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y')
    (curry (uncurry (Functor.map (ihom A) g))) (curry (NatTrans.app (ihom.ev A) Y ≫ g))
have a : Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
  (curry (NatTrans.app (ihom.ev A) Y ≫ g))
Tactic: rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_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 Y Y' : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Y'
a :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y ≫ g))
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y')
    (curry (uncurry (Functor.map (ihom A) g))) (curry (NatTrans.app (ihom.ev A) Y ≫ g))
have a₁ : Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
  (curry (NatTrans.app (ihom.ev A) Y) ≫ Functor.map (ihom A) g)
Tactic: rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_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 Y Y' : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Y'
a :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y ≫ g))
a₁ :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y) ≫ Functor.map (ihom A) g)
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y')
    (curry (uncurry (Functor.map (ihom A) g))) (curry (NatTrans.app (ihom.ev A) Y ≫ g))
have a₂ : Functor.map (ihom A) g = curry (uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom A) Y))) ≫ Functor.map (ihom A) g
Tactic: rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_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 Y Y' : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Y'
a :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y ≫ g))
a₁ :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y) ≫ Functor.map (ihom A) g)
a₂ : Functor.map (ihom A) g = curry (uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom A) Y))) ≫ Functor.map (ihom A) g
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y')
    (curry (uncurry (Functor.map (ihom A) g))) (curry (NatTrans.app (ihom.ev A) Y ≫ g))
have a₃ : Functor.map (ihom A) g = 𝟙 (Functor.obj.{v, v, u, u} (ihom A) Y) ≫ Functor.map (ihom A) g
Tactic: rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_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 Y Y' : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Y'
a :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y ≫ g))
a₁ :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y) ≫ Functor.map (ihom A) g)
a₂ : Functor.map (ihom A) g = curry (uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom A) Y))) ≫ Functor.map (ihom A) g
a₃ : Functor.map (ihom A) g = 𝟙 (Functor.obj.{v, v, u, u} (ihom A) Y) ≫ Functor.map (ihom A) g
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y')
    (curry (uncurry (Functor.map (ihom A) g))) (curry (NatTrans.app (ihom.ev A) Y ≫ g))
have a₄ : Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
  (Functor.map (ihom A) g)
Tactic: rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_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 : 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
⊢ 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 : uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) 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
⊢ 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 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
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
⊢ 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 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
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
⊢ 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)
    (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
Tactic: rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc,
    id_tensor_pre_app_comp_ev, whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app]