awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
    (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } } ▷
        limit F ≫
      (Functor.obj (C :=
              Cone (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) F))
              (Cone.postcompose (Iso.hom (λ_ F)))
              {
                pt :=
                  tensorObj.{v, u} (𝒞 := inst_1)
                    (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (limit F),
                π :=
                  {
                    app := fun (j : J) ↦
                      limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j ⊗ₘ limit.π F j,
                    naturality := ⋯ :
                    NatTrans
                      (Functor.obj (Functor.const J)
                        (tensorObj.{v, u} (𝒞 := inst_1)
                          (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
                          (limit F)))
                      (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))
                        F) } :
                Cone
                  (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))
                    F) }).π.app
        j)
have dsimp : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
  (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
  (CategoryStruct.comp (Y :=
    tensorObj.{v, u} (𝒞 := inst_1)
      (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (limit F))
    (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
        { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
          π :=
            { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := sorry :
              NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } } ▷
      limit F)
    ((limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j ⊗ₘ limit.π F j) ≫ Iso.hom (λ_ (F.obj j))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst_1)
        (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (limit F))
      (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } } ▷
        limit F)
      ((limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j ⊗ₘ limit.π F j) ≫ Iso.hom (λ_ (F.obj j))))
have simp : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
  (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
    (CategoryStruct.comp (Y := limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
        (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := sorry :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
        (limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) ▷
      limit F)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j))
Tactic: simp only [tensorHom_def, id_whiskerLeft, Category.assoc,
        Iso.inv_hom_id, Category.comp_id, ← comp_whiskerRight_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
      (CategoryStruct.comp (Y := limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
          (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          (limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) ▷
        limit F)
      (Iso.hom (λ_ (limit F)) ≫ limit.π F j))
have erw : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
  (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
    (NatTrans.app
        (Cone.π
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := sorry :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
        j ▷
      limit F)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j))
Tactic: erw [limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
      (NatTrans.app
          (Cone.π
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          j ▷
        limit F)
      (Iso.hom (λ_ (limit F)) ≫ limit.π F j))
have rw : Iso.hom (λ_ (limit F)) ≫ limit.π F j =
  𝟙 (tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F)) ≫
    Iso.hom (λ_ (limit F)) ≫ limit.π F j
Tactic: rw [id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
rw :
  Iso.hom (λ_ (limit F)) ≫ limit.π F j =
    𝟙 (tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F)) ≫
      Iso.hom (λ_ (limit F)) ≫ limit.π F j
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
      (NatTrans.app
          (Cone.π
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          j ▷
        limit F)
      (Iso.hom (λ_ (limit F)) ≫ limit.π F j))
have rw₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
  (Iso.hom (λ_ (limit F)) ≫ limit.π F j) (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
Tactic: rw [id_whiskerRight, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (limit F ◁
        limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } } ≫
      (Functor.obj (C :=
              Cone (tensorObj (𝒞 := Functor.category) F ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))))
              (Cone.postcompose (Iso.hom (ρ_ F)))
              {
                pt :=
                  tensorObj.{v, u} (𝒞 := inst_1) (limit F)
                    (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))),
                π :=
                  {
                    app := fun (j : J) ↦
                      limit.π F j ⊗ₘ limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j,
                    naturality := ⋯ :
                    NatTrans
                      (Functor.obj (Functor.const J)
                        (tensorObj.{v, u} (𝒞 := inst_1) (limit F)
                          (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))))
                      (tensorObj (𝒞 := Functor.category) F
                        ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) } :
                Cone
                  (tensorObj (𝒞 := Functor.category) F
                    ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) }).π.app
        j)
have dsimp : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
  (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
  (CategoryStruct.comp (Y :=
    tensorObj.{v, u} (𝒞 := inst_1) (limit F)
      (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))))
    (limit F ◁
      limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
        { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
          π :=
            { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := sorry :
              NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
    ((limit.π F j ⊗ₘ limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) ≫ Iso.hom (ρ_ (F.obj j))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst_1) (limit F)
        (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))))
      (limit F ◁
        limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
      ((limit.π F j ⊗ₘ limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) ≫ Iso.hom (ρ_ (F.obj j))))
have simp : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
  (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
    (limit F ◁
      CategoryStruct.comp (Y := limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
        (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := sorry :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
        (limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j))
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))
Tactic: simp only [tensorHom_def, ← whisker_exchange, whiskerRight_id, Category.assoc, Iso.inv_hom_id,
        Category.comp_id, ← whiskerLeft_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
      (limit F ◁
        CategoryStruct.comp (Y := limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
          (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          (limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j))
      (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))
have erw : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
  (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
    (limit F ◁
      NatTrans.app
        (Cone.π
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := sorry :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
        j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))
Tactic: erw [limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
      (limit F ◁
        NatTrans.app
          (Cone.π
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          j)
      (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))
have rw : Iso.hom (ρ_ (limit F)) ≫ limit.π F j =
  𝟙 (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1))) ≫
    Iso.hom (ρ_ (limit F)) ≫ limit.π F j
Tactic: rw [whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
rw :
  Iso.hom (ρ_ (limit F)) ≫ limit.π F j =
    𝟙 (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1))) ≫
      Iso.hom (ρ_ (limit F)) ≫ limit.π F j
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
      (limit F ◁
        NatTrans.app
          (Cone.π
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          j)
      (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))
have rw₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
  (Iso.hom (ρ_ (limit F)) ≫ limit.π F j) (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
Tactic: rw [whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Cokernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst_4 : HasBinaryCoproduct.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)
⊢ Eq (α :=
    coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
    (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)) 0
have h₁ : Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂ ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
  (CategoryStruct.comp (Y :=
    coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inl
    (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)))
  (CategoryStruct.comp (Y :=
    coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inl 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Cokernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst_4 : HasBinaryCoproduct.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)
h₁ :
  Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂ ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inl
      (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)))
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inl 0)
⊢ Eq (α :=
    coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
    (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)) 0
have h₂ : Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂ ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
  (CategoryStruct.comp (Y :=
    coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inr
    (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)))
  (CategoryStruct.comp (Y :=
    coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inr 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Colimits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst_2 : Category.{v_2, u_2} J
inst_3 : Category.{v_3, u_3} J₁
inst_4 : Category.{v_4, u_4} J₂
F₁ F₂ : Functor.{v_2, v_1, u_2, u_1} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst_5 : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst_6 : IsSifted.{v_2, u_2} J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ IsColimit (F := tensorObj (𝒞 := Functor.category) F₁ F₂) (c₁.tensor c₂)
have refine_1 : Functor.diag J ⋙ externalProduct F₁ F₂ ≅ tensorObj (𝒞 := Functor.category) F₁ F₂
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    ((Functor.Final.isColimitWhiskerEquiv (Functor.diag J) _).2 (hc₁.tensor₂ hc₂))