awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : Functor.{v₁, v₁, u₁, u₂} C D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) B :
        (a : (reflector i).obj (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) ⟶ B) → A ⊗ i.obj (L.obj (A ⟹ i.obj B)) ⟶ i.obj B)
      (CategoryStruct.comp (Y := (reflector i).obj (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)))
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) (L.obj A) (L.obj (i.obj (L.obj (A ⟹ i.obj B)))))
          (prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))))
          (L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))))
        ((Equiv.symm (ir.homEquiv (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)) B) :
            (a : (ihom A ⋙ tensorLeft A).obj (i.obj B) ⟶ i.obj B) →
              (reflector i).obj ((ihom A ⋙ tensorLeft A).obj (i.obj B)) ⟶ B)
          (NatTrans.app (ihom.ev A) (i.obj B)))))
⊢ i.essImage (A ⟹ i.obj B)
have this : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
Tactic: have : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B) := by
    dsimp
    rw [← curry_natural_left, curry_eq_iff, uncurry_id_eq_ev, ← ir.homEquiv_naturality_left,
      ir.homEquiv_apply_eq, Category.assoc, Category.assoc,
      prodComparison_natural_whiskerLeft_assoc, ← whiskerLeft_comp_assoc,
      ir.left_triangle_components, whiskerLeft_id, Category.id_comp]
    apply IsIso.hom_inv_id_assoc
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : Functor.{v₁, v₁, u₁, u₂} C D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) A (i.obj (L.obj (A ⟹ i.obj B)))) B :
        (a : (reflector i).obj (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) ⟶ B) → A ⊗ i.obj (L.obj (A ⟹ i.obj B)) ⟶ i.obj B)
      (CategoryStruct.comp (Y := (reflector i).obj (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)))
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) (L.obj A) (L.obj (i.obj (L.obj (A ⟹ i.obj B)))))
          (prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))))
          (L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))))
        ((Equiv.symm (ir.homEquiv (Functor.obj.{v₁, v₁, u₁, u₁} (ihom A ⋙ tensorLeft A) (i.obj B)) B) :
            (a : (ihom A ⋙ tensorLeft A).obj (i.obj B) ⟶ i.obj B) →
              (reflector i).obj ((ihom A ⋙ tensorLeft A).obj (i.obj B)) ⟶ B)
          (NatTrans.app (ihom.ev A) (i.obj B)))))
this : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
⊢ i.essImage (A ⟹ i.obj B)
have this₁ : IsSplitMono (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (A ⟹ i.obj B)) (η.app (A ⟹ i.obj B))
Tactic: haveI : IsSplitMono (η.app (A ⟹ i.obj B)) := IsSplitMono.mk' ⟨_, this⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
⊢ tensorLeft B ⊣ i.essImage.lift (i ⋙ ihom (i.obj B)) ⋯ ⋙ l
have comm1 : i ⋙ tensorLeft (i.obj B) ≅ tensorLeft B ⋙ i
Tactic: apply (ihom.adjunction (i.obj B)).restrictFullyFaithful i.fullyFaithfulOfReflective
          i.fullyFaithfulOfReflective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
comm1 : i ⋙ tensorLeft (i.obj B) ≅ tensorLeft B ⋙ i
⊢ tensorLeft B ⊣ i.essImage.lift (i ⋙ ihom (i.obj B)) ⋯ ⋙ l
have comm2 : i ⋙ ihom (i.obj B) ≅ (i.essImage.lift (i ⋙ ihom (i.obj B)) sorry ⋙ l) ⋙ i
Tactic: apply (ihom.adjunction (i.obj B)).restrictFullyFaithful i.fullyFaithfulOfReflective
          i.fullyFaithfulOfReflective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
⊢ i ⋙ tensorLeft (i.obj B) ≅ tensorLeft B ⋙ i
have comm1 : tensorLeft B ⋙ i ≅ i ⋙ tensorLeft (i.obj B)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
⊢ tensorLeft B ⋙ i ≅ i ⋙ tensorLeft (i.obj B)
have comm1 : (X : D) → (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X
Tactic: refine NatIso.ofComponents (fun X => ?_) (fun f => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B : D
comm1 : (X : D) → (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X
⊢ tensorLeft B ⋙ i ≅ i ⋙ tensorLeft (i.obj B)
have comm1₁ : ∀ {X Y : D} (f : X ⟶ Y),
  (tensorLeft B ⋙ i).map f ≫
      Iso.hom
        ((fun (X : D) ↦
            (asIso (prodComparison i B X) :
              i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj X)))
          Y) =
    Iso.hom
        ((fun (X : D) ↦
            (asIso (prodComparison i B X) :
              i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj X)))
          X) ≫
      (i ⋙ tensorLeft (i.obj B)).map f
Tactic: refine NatIso.ofComponents (fun X => ?_) (fun f => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B X : D
⊢ (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X
have this : Limits.PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
Tactic: haveI :=
              Adjunction.rightAdjoint_preservesLimits.{0, 0} (reflectorAdjunction i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B X Y : D
f : X ⟶ Y
⊢ (tensorLeft B ⋙ i).map f ≫
      Iso.hom
        ((fun (X : D) ↦
            (asIso (prodComparison i B X) :
              i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj X)))
          Y) =
    Iso.hom
        ((fun (X : D) ↦
            (asIso (prodComparison i B X) :
              i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ≅ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj X)))
          X) ≫
      (i ⋙ tensorLeft (i.obj B)).map f
have comm1 : Eq (α := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj Y))
  (i.map (B ◁ f) ≫ prodComparison i B Y) (prodComparison i B X ≫ i.obj B ◁ i.map f)
Tactic: dsimp [asIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
l : Functor.{v₁, v₁, u₁, u₂} i.EssImageSubcategory D
φ : l ⋙ i ≅ i.essImage.ι
B X Y : D
f : X ⟶ Y
⊢ Eq (α := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj Y))
    (i.map (B ◁ f) ≫ prodComparison i B Y) (prodComparison i B X ≫ i.obj B ◁ i.map f)
have comm1 : Eq (α := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) B X) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj B) (i.obj Y))
  (prodComparison i B X ≫ i.obj B ◁ i.map f) (prodComparison i B X ≫ i.obj B ◁ i.map f)
Tactic: rw [prodComparison_natural_whiskerLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
⊢ Eq (α :=
    (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ⟶
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
    ((Equiv.symm
            (Adjunction.homEquiv (reflectorAdjunction i) (tensorObj.{v₁, u₁} (𝒞 := inst) A B)
              (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))) :
          (a : A ⊗ B ⟶ i.obj ((reflector i).obj A ⊗ (reflector i).obj B)) →
            (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj A ⊗ (reflector i).obj B)
        (Iso.hom (β_ A B) ≫
          uncurry
            (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ≫
              curry
                (Iso.hom (β_ B (i.obj ((reflector i).obj A))) ≫
                  uncurry
                    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B ≫
                      curry (Iso.inv (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B))))))) :
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ⟶
        tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
    (prodComparison (reflector i) A B :
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ⟶
        tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
have rw : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
  (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
  (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
    CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
      (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
Tactic: rw [uncurry_natural_left, uncurry_curry, uncurry_natural_left, uncurry_curry,
    ← BraidedCategory.braiding_naturality_left_assoc, SymmetricCategory.symmetry_assoc,
    ← MonoidalCategory.whisker_exchange_assoc, ← tensorHom_def'_assoc,
    Adjunction.homEquiv_symm_apply, ← Adjunction.eq_unit_comp_map_iff, Iso.comp_inv_eq,
    Category.assoc, prodComparisonIso_hom i ((reflector i).obj A) ((reflector i).obj B)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
      NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
        (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
have h_fst : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj A))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
      NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
    (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
        (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
    (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
h_fst :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj A))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
        NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
      (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
        CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
          (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
      (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
      NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
        (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
have h_snd : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj B))
  ((NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
      NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B) ≫
    snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
        (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
    (snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj A))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
        NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
      (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
        CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
          (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
      (fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
have h_fst : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj A))
  (fst A B ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A)
  (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
    i.map ((reflector i).map (fst A B)))
Tactic: rw [tensorHom_fst, Category.assoc, Category.assoc, prodComparison_fst, ← i.map_comp,
    prodComparison_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj B))
    ((NatTrans.app (Adjunction.unit (reflectorAdjunction i)) A ⊗ₘ
        NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
        CategoryStruct.comp (Y := i.obj (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)))
          (i.map (prodComparison (reflector i) A B)) (prodComparison i ((reflector i).obj A) ((reflector i).obj B)))
      (snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))))
have h_snd : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj B))
  (snd A B ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
  (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
    i.map ((reflector i).map (snd A B)))
Tactic: rw [tensorHom_snd, Category.assoc, Category.assoc, prodComparison_snd, ← i.map_comp,
    prodComparison_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
      (prodComparison (reflector i) A B)
      ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
          (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
            (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
        (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)))) =
    𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
have rw : Eq (α :=
  tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
    (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
  ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
        (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
          (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
        (prodComparison (reflector i) A B)
        ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
            (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
              (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
          (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))))) :
    tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
  ((bijection i A B ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) :
        (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj (A ⊗ B)) →
          (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj (A ⊗ B))
      (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))) :
    tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
Tactic: rw [← (bijection i _ _ _).injective.eq_iff, bijection_natural, ← bijection_symm_apply_id,
        Equiv.apply_symm_apply, Category.id_comp]