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
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
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)
⊢ 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))) ≫
    Iso.hom (ρ_ (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)))
        (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]
-- 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
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)
rw₃ :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (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)))
          (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)
⊢ 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))) ≫
    Iso.hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      curry' f ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))
          (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]
-- 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
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)
rw₃ :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (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)))
          (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)
rw₄ :
  curry' (f ≫ g) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        curry' f ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))
            (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)
⊢ 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₅ : 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))) ≫
    Iso.hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ curry' f ≫ 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.Cartesian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) A I ⟶ I) (snd A I) (uncurry (t.to (A ⟹ I)))
have rw : Eq (α := I ⟶ A ⟹ I) (curry (snd A I)) (t.to (A ⟹ I))
Tactic: rw [← curry_eq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Cartesian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
⊢ snd A I ≫ t.to (tensorObj.{v, u} (𝒞 := inst) A I) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) A I)
have this : Eq (α := tensorObj.{v, u} (𝒞 := inst) A I ⟶ I) (snd A I) (uncurry (t.to (A ⟹ I)))
Tactic: have : snd A I = uncurry (t.to _) := by
      rw [← curry_eq_iff]
      apply t.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Cartesian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
this : Eq (α := tensorObj.{v, u} (𝒞 := inst) A I ⟶ I) (snd A I) (uncurry (t.to (A ⟹ I)))
⊢ snd A I ≫ t.to (tensorObj.{v, u} (𝒞 := inst) A I) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) A I)
have rw : Eq (α := I ⟶ A ⟹ tensorObj.{v, u} (𝒞 := inst) A I)
  (t.to (A ⟹ I) ≫ Functor.map (ihom A) (t.to (tensorObj.{v, u} (𝒞 := inst) A I)))
  (curry (𝟙 (tensorObj.{v, u} (𝒞 := inst) A I)))
Tactic: rw [this, ← uncurry_natural_right, ← eq_curry_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Cartesian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
inst_3 : BraidedCategory.{v, u} C
I : C
t : IsInitial.{v, u} I
inst_4 : MonoidalClosed.{v, u} C
⊢ CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) default (curry (Iso.hom (mulZero t) ≫ t.to B)) = 𝟙 (I ⟹ B)
have rw : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) I (I ⟹ B)) (Iso.inv (mulZero t))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) I (tensorUnit.{v, u} C (𝒞 := inst))) (I ◁ default)
      (Iso.hom (mulZero t) ≫ t.to B)) =
  Iso.inv (mulZero t) ≫ uncurry (𝟙 (I ⟹ B))
Tactic: rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mulZero t).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Cartesian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
⊢ Mono f
have rw : Mono (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A I) (lift (𝟙 A) f) (Iso.hom (zeroMul t)))
Tactic: rw [← lift_snd (𝟙 A) f, ← zeroMul_hom t]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Cartesian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
⊢ IsIso f
have this : Mono f
Tactic: haveI : Mono f := by
    rw [← lift_snd (𝟙 A) f, ← zeroMul_hom t]
    exact mono_comp _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Cartesian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
this : Mono f
⊢ IsIso f
have this₁ : IsSplitEpi f
Tactic: haveI : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Cartesian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
I B : C
t : IsInitial.{v, u} I
inst_2 : MonoidalClosed.{v, u} C
Z : C
g h : Z ⟶ I
h_1 : g ≫ t.to B = h ≫ t.to B
⊢ g = h
have this : IsIso g
Tactic: haveI := strict_initial t g
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Cartesian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
I B : C
t : IsInitial.{v, u} I
inst_2 : MonoidalClosed.{v, u} C
Z : C
g h : Z ⟶ I
h_1 : g ≫ t.to B = h ≫ t.to B
this : IsIso g
⊢ g = h
have this₁ : IsIso h
Tactic: haveI := strict_initial t h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Enrichment (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ Eq (α :=
    Quiver.Hom (V := C) (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Y₁)
      (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Y₂))
    (eHomWhiskerLeft C X g) (Functor.map (ihom X) g)
have change : 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₁ ◁ curry' g) (comp X Y₁ Y₂) =
  Functor.map (ihom X) g
Tactic: change (ρ_ _).inv ≫ _ ◁ curry' g ≫ comp X Y₁ Y₂ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Enrichment (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y₁ Y₂ : C
g : Y₁ ⟶ 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₁ ◁ curry' g) (comp X Y₁ Y₂) =
    Functor.map (ihom X) g
have rw : CategoryStruct.comp (Y :=
    tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y₁) (tensorUnit.{v, u} C (𝒞 := inst)))
    (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) =
  Functor.map (ihom X) g
Tactic: rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Enrichment (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
rw :
  CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y₁) (tensorUnit.{v, u} C (𝒞 := inst)))
      (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) =
    Functor.map (ihom X) g
⊢ 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₁ ◁ curry' g) (comp X Y₁ Y₂) =
    Functor.map (ihom X) g
have rw₁ : Eq (α := Functor.obj.{v, v, u, u} (ihom X) Y₁ ⟶ Functor.obj.{v, v, u, u} (ihom X) Y₂) (Functor.map (ihom X) g)
  (Functor.map (ihom X) g)
Tactic: rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Enrichment (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ Eq (α :=
    Quiver.Hom (V := C) (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X₂ Y)
      (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X₁ Y))
    (eHomWhiskerRight C f Y) (NatTrans.app (pre f) Y)
have change : Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y)
  (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)) ≫ curry' f ▷ Functor.obj.{v, v, u, u} (ihom X₂) Y ≫ comp X₁ X₂ Y)
  (NatTrans.app (pre f) Y)
Tactic: change (λ_ _).inv ≫ curry' f ▷ _ ≫ comp X₁ X₂ Y = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Enrichment (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y)
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)) ≫
      curry' f ▷ Functor.obj.{v, v, u, u} (ihom X₂) Y ≫ comp X₁ X₂ Y)
    (NatTrans.app (pre f) Y)
have rw : Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y)
  (CategoryStruct.comp (Y :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (Functor.obj.{v, v, u, u} (ihom X₂) Y))
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)))
    (Iso.hom (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)) ≫ NatTrans.app (pre f) Y))
  (NatTrans.app (pre f) Y)
Tactic: rw [curry'_whiskerRight_comp, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Enrichment (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
rw :
  Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (Functor.obj.{v, v, u, u} (ihom X₂) Y))
      (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)))
      (Iso.hom (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)) ≫ NatTrans.app (pre f) Y))
    (NatTrans.app (pre f) Y)
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y)
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)) ≫
      curry' f ▷ Functor.obj.{v, v, u, u} (ihom X₂) Y ≫ comp X₁ X₂ Y)
    (NatTrans.app (pre f) Y)
have rw₁ : Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y) (NatTrans.app (pre f) Y)
  (NatTrans.app (pre f) Y)
Tactic: rw [curry'_whiskerRight_comp, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
h : L ⊣ F
A : C
inst_4 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) L
inst_5 : F.Full
inst_6 : F.Faithful
B : D
⊢ IsIso (X := (tensorLeft (F.obj A) ⋙ L).obj B) (Y := (L ⋙ tensorLeft A).obj B)
    (NatTrans.app (natTrans (frobeniusMorphism F h A)) B)
have dsimp : IsIso (X := L.obj (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) B)) (Y := tensorObj.{v, u} (𝒞 := inst) A (L.obj B))
  (prodComparison L (F.obj A) B ≫ h.counit.app A ▷ L.obj B)
Tactic: dsimp [frobeniusMorphism]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B))
    (CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((F ⋙ ihom (F.obj A)).obj B))
      (F.obj A ◁ NatTrans.app (natTrans (expComparison F A)) B) (NatTrans.app (ihom.ev (F.obj A)) (F.obj B)))
    (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)) ≫ F.map (NatTrans.app (ihom.ev A) B))
have h : (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B)) =
    (Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) ((ihom A ⋙ F).obj B) ⟶
      Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B)) →
  tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) =
      (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).obj (Functor.obj.{v, v, u, u} (ihom A) B) →
    F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)) =
        (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (ihom A) B) →
      Eq (α :=
        tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) ⟶
          F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)))
        (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)))
        (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (ihom A) B))
Tactic: convert! mateEquiv_counit _ _ (prodComparisonNatIso F A).inv B using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1 :
  (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B)) =
    (Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) ((ihom A ⋙ F).obj B) ⟶
      Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B))
e_3 :
  tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) =
    (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).obj (Functor.obj.{v, v, u, u} (ihom A) B)
e_4 :
  F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)) =
    (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (ihom A) B)
⊢ Eq (α :=
    tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) ⟶
      F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)))
    (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)))
    (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (ihom A) B))
have h : CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)))
    (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B))
    (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (ihom A) B)) =
  𝟙 (F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)))
Tactic: apply IsIso.inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ Eq (α := F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶ (F ⋙ ihom (F.obj A)).obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v, v, u, u} (tensorLeft A ⋙ ihom A) B))
      (F.map (NatTrans.app (ihom.coev A) B))
      (NatTrans.app (natTrans (expComparison F A)) (tensorObj.{v, u} (𝒞 := inst) A B)))
    (NatTrans.app (ihom.coev (F.obj A)) (F.obj B) ≫ Functor.map (ihom (F.obj A)) (inv (prodComparison F A B)))
have h : (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶ (F ⋙ ihom (F.obj A)).obj (tensorObj.{v, u} (𝒞 := inst) A B)) =
    (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶
      (F ⋙ ihom (F.obj A)).obj (Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A) B)) →
  Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A) ⋙ ihom (F.obj A)) (F.obj B) =
      Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A) ⋙ ihom (F.obj A))
        (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B)) →
    Functor.obj.{v, v, u', u'} (ihom (F.obj A)) (F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) =
        Functor.obj.{v, v, u', u'} (ihom (F.obj A))
          ((Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (𝟭 C) B)) →
      Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B) =
          Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A))
            (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B)) →
        F.obj (tensorObj.{v, u} (𝒞 := inst) A B) =
            (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (𝟭 C) B) →
          Eq (α :=
            Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
            (inv (prodComparison F A B))
            (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (𝟭 C) B))
Tactic: convert! unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B using 3