awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : G.Monoidal
inst_8 : (F ⋙ G).Monoidal
X Y : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
      (Iso.inv (μIso (F ⋙ G) X Y)))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
        (G.map (μ F X Y)))
      (Iso.inv (μIso (F ⋙ G) X Y)))
have h_fst : Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj X)
  (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
      (Iso.inv (μIso (F ⋙ G) X Y)))
    (fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
  (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
        (G.map (μ F X Y)))
      (Iso.inv (μIso (F ⋙ G) X Y)))
    (fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : G.Monoidal
inst_8 : (F ⋙ G).Monoidal
X Y : C
h_fst :
  Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
          (μ G (F.obj X) (F.obj Y)) (G.map (μ F X Y)))
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
      (Iso.inv (μIso (F ⋙ G) X Y)))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
        (G.map (μ F X Y)))
      (Iso.inv (μIso (F ⋙ G) X Y)))
have h_snd : Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj Y)
  (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
      (Iso.inv (μIso (F ⋙ G) X Y)))
    (snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
  (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
        (G.map (μ F X Y)))
      (Iso.inv (μIso (F ⋙ G) X Y)))
    (snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F)
    (Iso.inv (preservesTerminalIso F))
have change : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (Iso.symm (εIso F)))
  (Iso.inv (preservesTerminalIso F))
Tactic: change (εIso F).symm.inv = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (Iso.symm (εIso F))) (Iso.inv (preservesTerminalIso F))
have e_self : Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≅ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (Iso.symm (εIso F))
  (preservesTerminalIso F)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y)
    (Iso.inv (prodComparisonIso F X Y))
have change : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (Iso.inv (Iso.symm (μIso F X Y))) (Iso.inv (prodComparisonIso F X Y))
Tactic: change (μIso F X Y).symm.inv = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (Iso.inv (Iso.symm (μIso F X Y))) (Iso.inv (prodComparisonIso F X Y))
have e_self : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≅ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
  (Iso.symm (μIso F X Y)) (prodComparisonIso F X Y)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≅ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (Iso.symm (μIso F X Y)) (prodComparisonIso F X Y)
have e_self : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
  (Iso.hom (Iso.symm (μIso F X Y))) (Iso.hom (prodComparisonIso F X Y))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
inst_6 : BraidedCategory.{v₁, u₁} C
inst_7 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : PreservesFiniteProducts F
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ F X Y ≫ F.map (Iso.hom (β_ X Y))) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
    (Iso.inv (Monoidal.μIso F Y X)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
    (Iso.inv (Monoidal.μIso F Y X)))
Tactic: rw [← cancel_mono (Monoidal.μIso _ _ _).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
inst_6 : BraidedCategory.{v₁, u₁} C
inst_7 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : PreservesFiniteProducts F
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
      (Iso.inv (Monoidal.μIso F Y X)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
      (Iso.inv (Monoidal.μIso F Y X)))
have h_fst : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj Y)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
      (Iso.inv (Monoidal.μIso F Y X)))
    (fst (F.obj Y) (F.obj X)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
      (Iso.inv (Monoidal.μIso F Y X)))
    (fst (F.obj Y) (F.obj X)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
inst_6 : BraidedCategory.{v₁, u₁} C
inst_7 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : PreservesFiniteProducts F
X Y : C
h_fst :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
        (Iso.inv (Monoidal.μIso F Y X)))
      (fst (F.obj Y) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
        (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X) (Iso.inv (Monoidal.μIso F Y X)))
      (fst (F.obj Y) (F.obj X)))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
      (Iso.inv (Monoidal.μIso F Y X)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
      (Iso.inv (Monoidal.μIso F Y X)))
have h_snd : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
      (Iso.inv (Monoidal.μIso F Y X)))
    (snd (F.obj Y) (F.obj X)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
      (Iso.inv (Monoidal.μIso F Y X)))
    (snd (F.obj Y) (F.obj X)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
    (Iso.inv (Functor.Monoidal.μIso G X Y)))
Tactic: rw [← cancel_mono (Functor.Monoidal.μIso _ _ _).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
      (Iso.inv (Functor.Monoidal.μIso G X Y)))
have rw : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (Iso.inv (Functor.Monoidal.μIso F X Y))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (Iso.inv (Functor.Monoidal.μIso F X Y))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
      (Iso.inv (Functor.Monoidal.μIso G X Y))))
Tactic: rw [← cancel_epi (Functor.Monoidal.μIso _ _ _).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
        (Iso.inv (Functor.Monoidal.μIso G X Y))))
have h_fst : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ G.obj X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
    (fst (G.obj X) (G.obj Y)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
        (Iso.inv (Functor.Monoidal.μIso G X Y))))
    (fst (G.obj X) (G.obj Y)))
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
h_fst :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ G.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
          (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (fst (G.obj X) (G.obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
          (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (fst (G.obj X) (G.obj Y)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
        (Iso.inv (Functor.Monoidal.μIso G X Y))))
have h_snd : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ G.obj Y)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
    (snd (G.obj X) (G.obj Y)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
        (Iso.inv (Functor.Monoidal.μIso G X Y))))
    (snd (G.obj X) (G.obj Y)))
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Cat (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C
⊢ Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
      ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x) =
    x
have h_map : autoParam
  (∀ (X Y : (↑chosenTerminal : Type u_1)) (f : X ⟶ Y),
    Functor.map
        (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
          ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
        f =
      eqToHom sorry ≫ x.map f ≫ eqToHom sorry)
  Functor.ext._auto_1
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Cat (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C
h_map :
  autoParam
    (∀ (X Y : (↑chosenTerminal : Type u_1)) (f : X ⟶ Y),
      Functor.map
          (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
            ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
          f =
        eqToHom ⋯ ≫ x.map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
⊢ Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
      ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x) =
    x
have h_obj : ∀ (X : (↑chosenTerminal : Type u_1)),
  Functor.obj.{u_2, v, u_1, u}
      (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
        ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
      X =
    x.obj X
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Cat (goal)
Goal:
X Y : Cat
x : BinaryFan X Y
x_1 : x.pt ⟶ of ((↑X : Type u_2) × (↑Y : Type u_2))
h1 : x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2)) = x.fst
h2 : x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2)) = x.snd
x_2 x_3 : (↑x.pt : Type u_2)
x_4 : x_2 ⟶ x_3
⊢ HEq (x_1.toFunctor.map x_4) (β :=
    Quiver.Hom (V := (↑(of ((↑X : Type u_2) × (↑Y : Type u_2))) : Type u_2))
      (Functor.obj (Hom.toFunctor ((fun (S : BinaryFan X Y) ↦ (S.fst.toFunctor.prod' S.snd.toFunctor).toCatHom) x)) x_2)
      (Functor.obj (Hom.toFunctor ((fun (S : BinaryFan X Y) ↦ (S.fst.toFunctor.prod' S.snd.toFunctor).toCatHom) x))
        x_3))
    (Functor.map (Hom.toFunctor ((fun (S : BinaryFan X Y) ↦ (S.fst.toFunctor.prod' S.snd.toFunctor).toCatHom) x)) x_4)
have dsimp : x_1.toFunctor.map x_4 ≍ Prod.mkHom (x.fst.toFunctor.map x_4) (x.snd.toFunctor.map x_4)
Tactic: dsimp