awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
    (CategoryStruct.comp (Y := (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))))
        (prodComparison (reflector i) A B) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
    (𝟙 (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)) :
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
        tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
have rw : Eq (α :=
  tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
    tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
  ((bijection i A B (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)) :
        (a : (reflector i).obj (A ⊗ B) ⟶ (reflector i).obj A ⊗ (reflector i).obj B) →
          (reflector i).obj A ⊗ (reflector i).obj B ⟶ (reflector i).obj A ⊗ (reflector i).obj B)
      (𝟙 ((reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B)) ≫ prodComparison (reflector i) A B) :
    tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
  (𝟙 (tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B)) :
    tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶
      tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B))
Tactic: rw [← bijection_natural, Category.id_comp, ← bijection_symm_apply_id,
        Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) (ihomUncurry x y z)
      (ihomCurry x y z) =
    𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))
have a : uncurry
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) (ihomUncurry x y z)
      (ihomCurry x y z)) =
  uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
Tactic: apply uncurry_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ uncurry
      (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)
        (ihomUncurry x y z) (ihomCurry x y z)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
have a : uncurry
    (uncurry
      (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)
        (ihomUncurry x y z) (ihomCurry x y z))) =
  uncurry (uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))))
Tactic: apply uncurry_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ uncurry
      (uncurry
        (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)
          (ihomUncurry x y z) (ihomCurry x y z))) =
    uncurry (uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))))
have a : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) x
      (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
    z)
  (CategoryStruct.comp (Y :=
    tensorObj.{v, u} (𝒞 := inst) x
      (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)))
    (x ◁ y ◁ ihomUncurry x y z)
    (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
      NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z))
  (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
Tactic: simp only [uncurry_natural_left, uncurry_uncurry_ihomCurry, Functor.id_obj, uncurry_id_eq_ev]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)))
      (x ◁ y ◁ ihomUncurry x y z)
      (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
        NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z))
    (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
have a : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) x
      (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
    z)
  (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
    Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
      x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z)
  (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
Tactic: rw [associator_inv_naturality_right_assoc, ← dsimp% uncurry_eq, uncurry_ihomUncurry]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
      z)
    (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
      Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z)
    (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
have a : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) x
      (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
    z)
  (x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z)
  (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)) (ihomCurry x y z)
      (ihomUncurry x y z) =
    𝟙 (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)
have a : uncurry
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))
      (ihomCurry x y z) (ihomUncurry x y z)) =
  uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z))
Tactic: apply uncurry_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ uncurry
      (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))
        (ihomCurry x y z) (ihomUncurry x y z)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z))
have a : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
      (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
    z)
  (CategoryStruct.comp (Y :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
      (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
    (tensorObj.{v, u} (𝒞 := inst) x y ◁ ihomCurry x y z)
    (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
      x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z))
  (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)
Tactic: rw [uncurry_natural_left, uncurry_id_eq_ev, uncurry_ihomUncurry]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (tensorObj.{v, u} (𝒞 := inst) x y ◁ ihomCurry x y z)
      (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z))
    (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)
have a : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
      (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
    z)
  (CategoryStruct.comp (Y :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
      (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
    (tensorObj.{v, u} (𝒞 := inst) x y ◁ ihomCurry x y z)
    (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
      x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z))
  (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (tensorObj.{v, u} (𝒞 := inst) x y ◁ ihomCurry x y z)
      (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z))
    (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)
have a : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
      (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
    z)
  (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) x (Functor.obj.{v, v, u, u} (ihom x) z))
      (x ◁
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
          (y ◁ ihomCurry x y z) (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (NatTrans.app (ihom.ev x) z))
  (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)
Tactic: rw [associator_naturality_right_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Types (hypothesis)
Goal:
C_1 : Type v₂
inst : Category.{v₁, v₂} C_1
C : Type v₁
inst_1 : SmallCategory C
F : C ⥤ Type v₁
⊢ Closed F
have this : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
Tactic: haveI : ∀ X : Type v₁, PreservesColimits (tensorLeft X) := by infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Types (hypothesis)
Goal:
C_1 : Type v₂
inst : Category.{v₁, v₂} C_1
C : Type v₁
inst_1 : SmallCategory C
F : C ⥤ Type v₁
this_1 : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
this : PreservesColimits (tensorLeft F) := ⋯
⊢ Closed F
have this₁ : Functor.IsLeftAdjoint (tensorLeft F)
Tactic: have := Presheaf.isLeftAdjoint_of_preservesColimits.{v₁} (tensorLeft F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Zero (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
⊢ Unique (X ⟶ Y)
have this : HasInitial.{v, u} C
Tactic: haveI : HasInitial C := HasZeroObject.hasInitial
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
this : HasInitial.{v, u} C
⊢ Unique (X ⟶ Y)
have apply : initial.{v, u} C ≅ tensorUnit.{v, u} C (𝒞 := inst)
Tactic: apply uniqueHomsetOfInitialIsoUnit _ X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
this : HasInitial.{v, u} C
⊢ initial.{v, u} C ≅ tensorUnit.{v, u} C (𝒞 := inst)
have refine_1 : Eq.{v + 1} (α := initial.{v, u} C ⟶ initial.{v, u} C)
  (CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) default (CategoryStruct.comp (Y := 0) default default))
  (𝟙 (initial.{v, u} C))
Tactic: refine ⟨default, (default : 𝟙_ C ⟶ 0) ≫ default, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
this : HasInitial.{v, u} C
refine_1 :
  Eq.{v + 1} (α := initial.{v, u} C ⟶ initial.{v, u} C)
    (CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) default (CategoryStruct.comp (Y := 0) default default))
    (𝟙 (initial.{v, u} C))
⊢ initial.{v, u} C ≅ tensorUnit.{v, u} C (𝒞 := inst)
have refine_2 : Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ tensorUnit.{v, u} C (𝒞 := inst))
  (CategoryStruct.comp (Y := initial.{v, u} C) (CategoryStruct.comp (Y := 0) default default) default)
  (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)))
Tactic: refine ⟨default, (default : 𝟙_ C ⟶ 0) ≫ default, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommComon_ (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
inst_1 : MonoidalCategory.{v₁, u₁} C_1
inst_2 : BraidedCategory.{v₁, u₁} C_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_1, u_1} C
inst_5 : SymmetricCategory.{v_1, u_1} C
A B : C
inst_6 : ComonObj A
inst_7 : ComonObj B
inst_8 : IsCommComonObj.{v_1, u_1} A
inst_9 : IsCommComonObj.{v_1, u_1} B
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_3) A B ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_3) (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B)
        (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B))
    (Δ ≫ Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B) (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B))) Δ
have rw : Eq.{v_1 + 1} (α :=
  tensorObj.{v_1, u_1} (𝒞 := inst_3) A B ⟶
    tensorObj.{v_1, u_1} (𝒞 := inst_3) (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B)
      (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B))
  ((Δ ⊗ₘ Δ) ≫ (Iso.hom (β_ A A) ⊗ₘ Iso.hom (β_ B B)) ≫ tensorμ A A B B) ((Δ ⊗ₘ Δ) ≫ tensorμ A A B B)
Tactic: rw [Comon.tensorObj_comul, Category.assoc, SymmetricCategory.tensorμ_braid_swap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommGrp_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
A : CommGrp.{v₁, u₁} C
⊢ Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (Grp.X (obj F.mapGrp A.toGrp)) (Grp.X (obj F.mapGrp A.toGrp)) ⟶
      Grp.X (obj F.mapGrp A.toGrp))
    (Iso.hom (β_ (Grp.X (obj F.mapGrp A.toGrp)) (Grp.X (obj F.mapGrp A.toGrp))) ≫ μ) μ
have dsimp : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
  (Iso.hom (β_ (F.obj A.X) (F.obj A.X)) ≫
    CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommGrp_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
A : CommGrp.{v₁, u₁} C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (Iso.hom (β_ (F.obj A.X) (F.obj A.X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
    (F.map (Iso.hom (β_ A.X A.X)) ≫ F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommGrp_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
A : CommGrp.{v₁, u₁} C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
      (F.map (Iso.hom (β_ A.X A.X)) ≫ F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (Iso.hom (β_ (F.obj A.X) (F.obj A.X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
have rw₁ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
    (F.map (Iso.hom (β_ A.X A.X) ≫ μ)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommGrp_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
A : CommGrp.{v₁, u₁} C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
      (F.map (Iso.hom (β_ A.X A.X)) ≫ F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
rw₁ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
      (F.map (Iso.hom (β_ A.X A.X) ≫ μ)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (Iso.hom (β_ (F.obj A.X) (F.obj A.X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
have rw₂ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]