awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ x_1.toFunctor.map x_4 ≍ Prod.mkHom (x.fst.toFunctor.map x_4) (x.snd.toFunctor.map x_4)
have rw : x_1.toFunctor.map x_4 ≍
  Prod.mkHom ((x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2))).toFunctor.map x_4)
    ((x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2))).toFunctor.map x_4)
Tactic: rw [← h1, ← h2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
G : CommGrp.{v, u} C
H I : (Grp.{v, u} C)ᵒᵖ
f : H ⟶ I
⊢ Eq (α := unop I ⟶ G.toGrp) (f.unop ≫ 1) 1
have h : Eq (α := (unop I).toMon.X ⟶ G.toGrp.toMon.X) (Mon.Hom.hom (InducedCategory.Hom.hom (f.unop ≫ 1)))
  (Mon.Hom.hom (InducedCategory.Hom.hom 1))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
G : CommGrp.{v, u} C
H I : (Grp.{v, u} C)ᵒᵖ
f : H ⟶ I
g h : unop H ⟶ G.toGrp
⊢ f.unop ≫ (g * h) = f.unop ≫ g * f.unop ≫ h
have h₁ : (f.unop ≫ (g * h)).hom.hom = (f.unop ≫ g * f.unop ≫ h).hom.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
X₁ X₂ : CommGrp.{v, u} C
ψ : X₁ ⟶ X₂
Y : (Grp.{v, u} C)ᵒᵖ
⊢ Eq (α := unop Y ⟶ X₂.toGrp) (1 ≫ ψ.hom) 1
have h : Eq (α := (unop Y).toMon.X ⟶ X₂.toGrp.toMon.X) (Mon.Hom.hom (InducedCategory.Hom.hom (1 ≫ ψ.hom)))
  (Mon.Hom.hom (InducedCategory.Hom.hom 1))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
X₁ X₂ : CommGrp.{v, u} C
ψ : X₁ ⟶ X₂
Y : (Grp.{v, u} C)ᵒᵖ
f g : unop Y ⟶ X₁.toGrp
⊢ (f * g) ≫ ψ.hom = f ≫ ψ.hom * g ≫ ψ.hom
have h : ((f * g) ≫ ψ.hom).hom.hom = (f ≫ ψ.hom * g ≫ ψ.hom).hom.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : ComonObj A
⊢ Eq.{v + 1} (α := A ⟶ tensorObj.{v, u} (𝒞 := inst) A A) Δ (lift (𝟙 A) (𝟙 A))
have h_fst : Eq.{v + 1} (α := A ⟶ A) (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) Δ (fst A A))
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) (lift (𝟙 A) (𝟙 A)) (fst A A))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : ComonObj A
h_fst :
  Eq.{v + 1} (α := A ⟶ A) (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) Δ (fst A A))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) (lift (𝟙 A) (𝟙 A)) (fst A A))
⊢ Eq.{v + 1} (α := A ⟶ tensorObj.{v, u} (𝒞 := inst) A A) Δ (lift (𝟙 A) (𝟙 A))
have h_snd : Eq.{v + 1} (α := A ⟶ A) (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) Δ (snd A A))
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) (lift (𝟙 A) (𝟙 A)) (snd A A))
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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
⊢ Eq (α := tensorObj (𝒞 := category) X Y ⟶ X) { app := fun (x : J) ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
    (X ◁
        IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
          Y ≫
      Iso.hom (ρ_ X))
have w : ∀ (x : J),
  Eq (α := (tensorObj (𝒞 := category) X Y).obj x ⟶ X.obj x)
    (NatTrans.app { app := fun (x : J) ↦ fst (X.obj x) (Y.obj x), naturality := sorry } x)
    (NatTrans.app
      (X ◁
          IsTerminal.from
            (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
              fun (x : J) ↦
              isLimitChangeEmptyCone C isTerminalTensorUnit
                (mapCone (obj (evaluation J C) x)
                  (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
                (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
            Y ≫
        Iso.hom (ρ_ X))
      x)
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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
⊢ Eq (α := (tensorObj (𝒞 := category) X Y).obj x ⟶ X.obj x)
    (NatTrans.app { app := fun (x : J) ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ } x)
    (NatTrans.app
      (X ◁
          IsTerminal.from
            (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
              fun (x : J) ↦
              isLimitChangeEmptyCone C isTerminalTensorUnit
                (mapCone (obj (evaluation J C) x)
                  (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
                (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
            Y ≫
        Iso.hom (ρ_ X))
      x)
have w : Eq.{v_2 + 1} (α :=
  tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (Y.obj x) ⟶
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
  (X.obj x ◁ IsTerminal.from isTerminalTensorUnit (Y.obj x))
  (X.obj x ◁
    NatTrans.app
      (IsTerminal.from
        (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
          fun (x : J) ↦
          isLimitChangeEmptyCone C isTerminalTensorUnit
            (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
            (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
        Y)
      x)
Tactic: simp only [Monoidal.tensorObj_obj, fst_def, asEmptyCone_pt, NatTrans.comp_app,
      Monoidal.tensorUnit_obj, Monoidal.whiskerLeft_app, Monoidal.rightUnitor_hom_app,
      Iso.cancel_iso_hom_right]
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
⊢ Eq.{v_2 + 1} (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (Y.obj x) ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
    (X.obj x ◁ IsTerminal.from isTerminalTensorUnit (Y.obj x))
    (X.obj x ◁
      NatTrans.app
        (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
          Y)
        x)
have w : Eq.{v_2 + 1} (α := Y.obj x ⟶ tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (IsTerminal.from isTerminalTensorUnit (Y.obj x))
  (NatTrans.app
    (IsTerminal.from
      (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
        fun (x : J) ↦
        isLimitChangeEmptyCone C isTerminalTensorUnit
          (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
          (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
      Y)
    x)
Tactic: congr
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
⊢ Eq (α := tensorObj (𝒞 := category) X Y ⟶ Y) { app := fun (x : J) ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }
    (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
          X ▷
        Y ≫
      Iso.hom (λ_ Y))
have w : ∀ (x : J),
  Eq (α := (tensorObj (𝒞 := category) X Y).obj x ⟶ Y.obj x)
    (NatTrans.app { app := fun (x : J) ↦ snd (X.obj x) (Y.obj x), naturality := sorry } x)
    (NatTrans.app
      (IsTerminal.from
            (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
              fun (x : J) ↦
              isLimitChangeEmptyCone C isTerminalTensorUnit
                (mapCone (obj (evaluation J C) x)
                  (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
                (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
            X ▷
          Y ≫
        Iso.hom (λ_ Y))
      x)
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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
⊢ Eq (α := (tensorObj (𝒞 := category) X Y).obj x ⟶ Y.obj x)
    (NatTrans.app { app := fun (x : J) ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ } x)
    (NatTrans.app
      (IsTerminal.from
            (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
              fun (x : J) ↦
              isLimitChangeEmptyCone C isTerminalTensorUnit
                (mapCone (obj (evaluation J C) x)
                  (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
                (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
            X ▷
          Y ≫
        Iso.hom (λ_ Y))
      x)
have w : Eq.{v_2 + 1} (α :=
  tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (Y.obj x) ⟶
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (Y.obj x))
  (IsTerminal.from isTerminalTensorUnit (X.obj x) ▷ Y.obj x)
  (NatTrans.app
      (IsTerminal.from
        (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
          fun (x : J) ↦
          isLimitChangeEmptyCone C isTerminalTensorUnit
            (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
            (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
        X)
      x ▷
    Y.obj x)
Tactic: simp only [Monoidal.tensorObj_obj, snd_def, asEmptyCone_pt, NatTrans.comp_app,
      Monoidal.tensorUnit_obj, Monoidal.whiskerRight_app, Monoidal.leftUnitor_hom_app,
      Iso.cancel_iso_hom_right]
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
⊢ Eq.{v_2 + 1} (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (Y.obj x) ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (Y.obj x))
    (IsTerminal.from isTerminalTensorUnit (X.obj x) ▷ Y.obj x)
    (NatTrans.app
        (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
          X)
        x ▷
      Y.obj x)
have w : Eq.{v_2 + 1} (α := X.obj x ⟶ tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (IsTerminal.from isTerminalTensorUnit (X.obj x))
  (NatTrans.app
    (IsTerminal.from
      (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
        fun (x : J) ↦
        isLimitChangeEmptyCone C isTerminalTensorUnit
          (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
          (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
      X)
    x)
Tactic: congr
-- 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
⊢ Eq (α := F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).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) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
    (NatTrans.app (Iso.inv (λ_ F)) j :
      F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
    (Iso.hom (λ_ (F.obj j))) =
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
    (Iso.inv (λ_ (F.obj j))) (Iso.hom (λ_ (F.obj j)))
Tactic: rw [← cancel_mono ((λ_ (F.obj j)).hom), Iso.inv_hom_id, ← leftUnitor_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) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (Iso.hom (λ_ (F.obj j))) =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (Iso.inv (λ_ (F.obj j))) (Iso.hom (λ_ (F.obj j)))
⊢ Eq (α := F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).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) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
    (NatTrans.app (Iso.inv (λ_ F)) j :
      F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
    (Iso.hom (λ_ (F.obj j))) =
  𝟙 (F.obj j)
Tactic: rw [← cancel_mono ((λ_ (F.obj j)).hom), Iso.inv_hom_id, ← leftUnitor_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) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (Iso.hom (λ_ (F.obj j))) =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (Iso.inv (λ_ (F.obj j))) (Iso.hom (λ_ (F.obj j)))
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (Iso.hom (λ_ (F.obj j))) =
    𝟙 (F.obj j)
⊢ Eq (α := F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).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) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
    (NatTrans.app (Iso.inv (λ_ F)) j :
      F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
    (NatTrans.app (Iso.hom (λ_ F)) j) =
  𝟙 (F.obj j)
Tactic: rw [← cancel_mono ((λ_ (F.obj j)).hom), Iso.inv_hom_id, ← leftUnitor_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) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (Iso.hom (λ_ (F.obj j))) =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (Iso.inv (λ_ (F.obj j))) (Iso.hom (λ_ (F.obj j)))
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (Iso.hom (λ_ (F.obj j))) =
    𝟙 (F.obj j)
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (NatTrans.app (Iso.hom (λ_ F)) j) =
    𝟙 (F.obj j)
⊢ Eq (α := F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).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, ← leftUnitor_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
⊢ 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)
    (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)))
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)))
⊢ 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)
    (Iso.hom (ρ_ (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]