awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
j : J
rw :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (NatTrans.app (Iso.inv (ρ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
      (Iso.hom (ρ_ (F.obj j))) =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (Iso.inv (ρ_ (F.obj j))) (Iso.hom (ρ_ (F.obj j)))
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (NatTrans.app (Iso.inv (ρ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
      (Iso.hom (ρ_ (F.obj j))) =
    𝟙 (F.obj j)
⊢ Eq (α := F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
    (NatTrans.app (Iso.inv (ρ_ F)) j) (Iso.inv (ρ_ (F.obj j)))
have rw₂ : CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
    (NatTrans.app (Iso.inv (ρ_ F)) j :
      F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
    (NatTrans.app (Iso.hom (ρ_ F)) j) =
  𝟙 (F.obj j)
Tactic: rw [← cancel_mono ((ρ_ (F.obj j)).hom), Iso.inv_hom_id, ← rightUnitor_hom_app,
    Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
j : J
rw :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (NatTrans.app (Iso.inv (ρ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
      (Iso.hom (ρ_ (F.obj j))) =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (Iso.inv (ρ_ (F.obj j))) (Iso.hom (ρ_ (F.obj j)))
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (NatTrans.app (Iso.inv (ρ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
      (Iso.hom (ρ_ (F.obj j))) =
    𝟙 (F.obj j)
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (NatTrans.app (Iso.inv (ρ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
      (NatTrans.app (Iso.hom (ρ_ F)) j) =
    𝟙 (F.obj j)
⊢ Eq (α := F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
    (NatTrans.app (Iso.inv (ρ_ F)) j) (Iso.inv (ρ_ (F.obj j)))
have rw₃ : Eq.{v_2 + 1} (α := F.obj j ⟶ F.obj j) (𝟙 (F.obj j)) (𝟙 (F.obj j))
Tactic: rw [← cancel_mono ((ρ_ (F.obj j)).hom), Iso.inv_hom_id, ← rightUnitor_hom_app,
    Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} J C
j : J
⊢ Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) F₁ F₂) F₃).obj j)
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j) (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
have rw : Eq (α :=
  (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₁.obj j) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₂.obj j) (F₃.obj j)))
  (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
  (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
Tactic: rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} J C
j : J
rw :
  Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₁.obj j) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₂.obj j) (F₃.obj j)))
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
    (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
⊢ Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) F₁ F₂) F₃).obj j)
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j) (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
have rw₁ : NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) =
  𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j)
Tactic: rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} J C
j : J
rw :
  Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₁.obj j) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₂.obj j) (F₃.obj j)))
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
    (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
rw₁ :
  NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) =
    𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j)
⊢ Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) F₁ F₂) F₃).obj j)
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j) (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
have rw₂ : NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ NatTrans.app (Iso.hom (α_ F₁ F₂ F₃)) j =
  𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j)
Tactic: rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} J C
j : J
rw :
  Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₁.obj j) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₂.obj j) (F₃.obj j)))
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
    (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
rw₁ :
  NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) =
    𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j)
rw₂ :
  NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ NatTrans.app (Iso.hom (α_ F₁ F₂ F₃)) j =
    𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j)
⊢ Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) F₁ F₂) F₃).obj j)
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j) (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
have rw₃ : Eq.{v_2 + 1} (α :=
  (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₁.obj j) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₂.obj j) (F₃.obj j)))
  (𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j))
  (𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j))
Tactic: rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
K : Type u_5
inst_6 : Category.{v_5, u_5} K
inst_7 : HasColimitsOfShape.{v_5, u_5, v_2, u_2} K C
inst_8 : ∀ (X : C), PreservesColimitsOfShape.{v_5, u_5, v_2, v_2, u_2, u_2} K (tensorLeft X)
F : Functor.{v_1, v_2, u_1, u_2} J C
⊢ PreservesColimitsOfShape K (tensorLeft F)
have x : ∀ (k : J), PreservesColimitsOfShape K (tensorLeft F ⋙ obj (evaluation J C) k)
Tactic: apply preservesColimitsOfShape_of_evaluation
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
K : Type u_5
inst_6 : Category.{v_5, u_5} K
inst_7 : HasColimitsOfShape.{v_5, u_5, v_2, u_2} K C
inst_8 : ∀ (X : C), PreservesColimitsOfShape.{v_5, u_5, v_2, v_2, u_2, u_2} K (tensorLeft X)
F : Functor.{v_1, v_2, u_1, u_2} J C
k : J
⊢ PreservesColimitsOfShape K (tensorLeft F ⋙ obj (evaluation J C) k)
have x : ∀ (this : tensorLeft F ⋙ obj (evaluation J C) k ≅ obj (evaluation J C) k ⋙ tensorLeft (F.obj k)),
  PreservesColimitsOfShape K (tensorLeft F ⋙ obj (evaluation J C) k)
Tactic: haveI : tensorLeft F ⋙ (evaluation J C).obj k ≅ (evaluation J C).obj k ⋙ tensorLeft (F.obj k) :=
    NatIso.ofComponents (fun _ ↦ Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_3, v_2, u_3, u_2} D C
H : Functor.{v_2, v_4, u_2, u_4} C E
inst_6 : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ (tensorObj (𝒞 := category) F G ⋙ H).map f ≫
      Iso.hom
        ((fun (X : D) ↦
            (prodComparisonIso H (F.obj X) (G.obj X) :
              H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ≅
                tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj X)) (H.obj (G.obj X))))
          Y) =
    Iso.hom
        ((fun (X : D) ↦
            (prodComparisonIso H (F.obj X) (G.obj X) :
              H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ≅
                tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj X)) (H.obj (G.obj X))))
          X) ≫
      (tensorObj (𝒞 := category) (F ⋙ H) (G ⋙ H)).map f
have dsimp : Eq (α :=
  H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶
    tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
  (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
  (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_3, v_2, u_3, u_2} D C
H : Functor.{v_2, v_4, u_2, u_4} C E
inst_6 : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ Eq (α :=
    H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶
      tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
    (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
have h_fst : Eq (α := H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶ H.obj (F.obj Y))
  (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
    (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
    (fst (H.obj (F.obj Y)) (H.obj (G.obj Y))))
  (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
    (fst (H.obj (F.obj Y)) (H.obj (G.obj Y))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_3, v_2, u_3, u_2} D C
H : Functor.{v_2, v_4, u_2, u_4} C E
inst_6 : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
h_fst :
  Eq (α := H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶ H.obj (F.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
      (fst (H.obj (F.obj Y)) (H.obj (G.obj Y))))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
      (fst (H.obj (F.obj Y)) (H.obj (G.obj Y))))
⊢ Eq (α :=
    H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶
      tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
    (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
have h_snd : Eq (α := H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶ H.obj (G.obj Y))
  (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
    (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
    (snd (H.obj (F.obj Y)) (H.obj (G.obj Y))))
  (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
    (snd (H.obj (F.obj Y)) (H.obj (G.obj Y))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_2, v, u_2, v + 1} Cᵒᵖ (Type v)
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y
⊢ Eq.{v + 1} (α := (tensorObj (𝒞 := category) F G).obj (Opposite.op I))
    (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
            Equiv.{v_2 + 1, v + 1} (I ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
              ((tensorObj (𝒞 := category) F G).obj (Opposite.op I))) :
          (a : I ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op I))
        (f ≫ g) :
      (tensorObj (𝒞 := category) F G).obj (Opposite.op I))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := category) F G).map f.op) :
          (a : (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op W))) →
            (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op I)))
        (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
                Equiv.{v_2 + 1, v + 1} (W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
                  ((tensorObj (𝒞 := category) F G).obj (Opposite.op W))) :
              (a : W ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op W))
            g :
          (tensorObj (𝒞 := category) F G).obj (Opposite.op W)) :
      (fun (X : Type v) ↦ X) ((tensorObj (𝒞 := category) F G).obj (Opposite.op I)))
have refine_1 : Eq.{v + 1} (α := F.obj (Opposite.op I))
  (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
          Equiv.{v_2 + 1, v + 1} (I ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
            ((tensorObj (𝒞 := category) F G).obj (Opposite.op I))) :
        (a : I ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op I))
      (f ≫ g)).1
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := category) F G).map f.op) :
        (a : (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op W))) →
          (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op I)))
      (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
              Equiv.{v_2 + 1, v + 1} (W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
                ((tensorObj (𝒞 := category) F G).obj (Opposite.op W))) :
            (a : W ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op W))
          g :
        (tensorObj (𝒞 := category) F G).obj (Opposite.op W))).1
Tactic: refine Prod.ext ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_2, v, u_2, v + 1} Cᵒᵖ (Type v)
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y
⊢ Eq.{v + 1} (α := F.obj (Opposite.op I))
    (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
            Equiv.{v_2 + 1, v + 1} (I ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
              ((tensorObj (𝒞 := category) F G).obj (Opposite.op I))) :
          (a : I ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op I))
        (f ≫ g)).1
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := category) F G).map f.op) :
          (a : (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op W))) →
            (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op I)))
        (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
                Equiv.{v_2 + 1, v + 1} (W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
                  ((tensorObj (𝒞 := category) F G).obj (Opposite.op W))) :
              (a : W ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op W))
            g :
          (tensorObj (𝒞 := category) F G).obj (Opposite.op W))).1
have refine_1 : Eq.{v + 1} (α := F.obj (Opposite.op I))
  (((h₁.homEquiv : Equiv.{v_2 + 1, v + 1} (I ⟶ X) (F.obj (Opposite.op I))) : (a : I ⟶ X) → F.obj (Opposite.op I))
      ((f ≫ g) ≫ fst X Y) :
    F.obj (Opposite.op I))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (Opposite.op W))) → (fun (X : Type v) ↦ X) (F.obj (Opposite.op I)))
      (((h₁.homEquiv : Equiv.{v_2 + 1, v + 1} (W ⟶ X) (F.obj (Opposite.op W))) : (a : W ⟶ X) → F.obj (Opposite.op W))
          (g ≫ fst X Y) :
        F.obj (Opposite.op W)) :
    (fun (X : Type v) ↦ X) (F.obj (Opposite.op I)))
Tactic: change h₁.homEquiv ((f ≫ g) ≫ fst X Y) = F.map f.op (h₁.homEquiv (g ≫ fst X Y))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory (goal)
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_2, v, u_2, v + 1} Cᵒᵖ (Type v)
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y
⊢ Eq.{v + 1} (α := G.obj (Opposite.op I))
    (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
            Equiv.{v_2 + 1, v + 1} (I ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
              ((tensorObj (𝒞 := category) F G).obj (Opposite.op I))) :
          (a : I ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op I))
        (f ≫ g)).2
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := category) F G).map f.op) :
          (a : (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op W))) →
            (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op I)))
        (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
                Equiv.{v_2 + 1, v + 1} (W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
                  ((tensorObj (𝒞 := category) F G).obj (Opposite.op W))) :
              (a : W ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op W))
            g :
          (tensorObj (𝒞 := category) F G).obj (Opposite.op W))).2
have refine_2 : Eq.{v + 1} (α := G.obj (Opposite.op I))
  (((h₂.homEquiv : Equiv.{v_2 + 1, v + 1} (I ⟶ Y) (G.obj (Opposite.op I))) : (a : I ⟶ Y) → G.obj (Opposite.op I))
      ((f ≫ g) ≫ snd X Y) :
    G.obj (Opposite.op I))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
        (a : (fun (X : Type v) ↦ X) (G.obj (Opposite.op W))) → (fun (X : Type v) ↦ X) (G.obj (Opposite.op I)))
      (((h₂.homEquiv : Equiv.{v_2 + 1, v + 1} (W ⟶ Y) (G.obj (Opposite.op W))) : (a : W ⟶ Y) → G.obj (Opposite.op W))
          (g ≫ snd X Y) :
        G.obj (Opposite.op W)) :
    (fun (X : Type v) ↦ X) (G.obj (Opposite.op I)))
Tactic: change h₂.homEquiv ((f ≫ g) ≫ snd X Y) = G.map f.op (h₂.homEquiv (g ≫ snd X Y))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
f : X ⟶ G
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (f ≫ lift (@GrpObj.inv _ _ inst_1 _ _) (𝟙 G)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit X) η
have rw : f ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (@GrpObj.inv _ _ inst_1 _ _) (𝟙 G)) μ =
  CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit X) η
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
⊢ ofRepresentableBy G (yonedaGrpObj G) (yonedaGrpObjRepresentableBy G) = inst_2
have H : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G) μ μ
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G) μ μ
have H : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (fst G G) (snd G G)) μ) μ
Tactic: change lift (fst G G) (snd G G) ≫ μ = μ