awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) ((μ ⊗ₘ 𝟙 M) ≫ μ)
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) (f₃ ≫ 𝟙 M)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ)
have rw₂ : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ
Tactic: rw [← tensorHom_id, lift_map_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
have trans : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M) (lift (lift f₁ f₂) f₃)
    (μ ▷ M ≫ μ) =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)
Tactic: trans lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
trans :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
have trans₁ : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (lift f₁ (lift f₂ f₃))
    (M ◁ μ ≫ μ) =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
Tactic: trans lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)
have rw : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M) (lift (lift f₁ f₂) f₃)
    (Iso.hom (α_ M M M) ≫ M ◁ μ ≫ μ) =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)
Tactic: rw [MonObj.mul_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (Iso.hom (α_ M M M) ≫ M ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)
have simp_rw : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ M ◁ μ) μ =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ))
    μ
Tactic: simp_rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ M ◁ μ)
      μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
        (lift f₁ (lift f₂ f₃)) (M ◁ μ))
      μ
have e_a : Eq (α := X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
  (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (lift f₁ (lift f₂ f₃))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ Eq (α := X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (lift f₁ (lift f₂ f₃))
have e_a : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M)) =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift f₁ (lift f₂ f₃)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
e_a :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M)) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M))
⊢ Eq (α := X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (lift f₁ (lift f₂ f₃))
have e_a₁ : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (fst M M) =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)))
    (fst M M)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
e_a :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M)) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M))
e_a₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (fst M M) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
        (lift f₁ (lift f₂ f₃)) (snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)))
      (fst M M)
⊢ Eq (α := X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (lift f₁ (lift f₂ f₃))
have e_a₂ : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (snd M M) =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)))
    (snd M M)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
have rw : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (lift f₁ (lift f₂ f₃))
    ((𝟙 M ⊗ₘ μ) ≫ μ) =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
Tactic: rw [← id_tensorHom, lift_map_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) ((𝟙 M ⊗ₘ μ) ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
have rw₁ : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift (f₁ ≫ 𝟙 M) (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
Tactic: rw [← id_tensorHom, lift_map_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) ((𝟙 M ⊗ₘ μ) ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (f₁ ≫ 𝟙 M) (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
have rw₂ : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
Tactic: rw [← id_tensorHom, lift_map_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : X ⟶ M
⊢ 1 * f = f
have change : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η) f) μ =
  f
Tactic: change lift (toUnit _ ≫ η) f ≫ μ = f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η) f) μ =
    f
have rw : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) M) (lift (toUnit X) f)
    (snd (tensorUnit.{v, u_1} C (𝒞 := inst)) M) =
  f
Tactic: rw [← Category.comp_id f, ← lift_map_assoc, tensorHom_id, MonObj.one_mul,
      Category.comp_id, leftUnitor_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : X ⟶ M
⊢ f * 1 = f
have change : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
    (lift f (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η)) μ =
  f
Tactic: change lift f (toUnit _ ≫ η) ≫ μ = f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η)) μ =
    f
have rw : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f (toUnit X))
    (fst M (tensorUnit.{v, u_1} C (𝒞 := inst))) =
  f
Tactic: rw [← Category.comp_id f, ← lift_map_assoc, id_tensorHom, MonObj.mul_one,
      Category.comp_id, rightUnitor_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} N.X
f : M ⟶ N
n : ℕ
⊢ (f ^ n).hom = f.hom ^ n
have zero : (HPow.hPow (β := ℕ) f 0).hom = HPow.hPow (β := ℕ) f.hom 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} N.X
f : M ⟶ N
n : ℕ
zero : (HPow.hPow (β := ℕ) f 0).hom = HPow.hPow (β := ℕ) f.hom 0
⊢ (f ^ n).hom = f.hom ^ n
have succ : ∀ (n : ℕ), (f ^ n).hom = f.hom ^ n → (f ^ (n + 1)).hom = f.hom ^ (n + 1)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
⊢ Eq (α := unop Y₂ ⟶ M) (φ.unop ≫ 1) 1
have change : Eq (α := unop Y₂ ⟶ M) (φ.unop ≫ CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop X)) η)
  (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
Tactic: change φ.unop ≫ toUnit _ ≫ η = toUnit _ ≫ η
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
⊢ Eq (α := unop Y₂ ⟶ M) (φ.unop ≫ CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop X)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
have rw : Eq (α := unop Y₂ ⟶ M) (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (φ.unop ≫ toUnit (unop X)) η)
  (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
Tactic: rw [← Category.assoc, toUnit_unique (φ.unop ≫ toUnit _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
rw :
  Eq (α := unop Y₂ ⟶ M) (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (φ.unop ≫ toUnit (unop X)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
⊢ Eq (α := unop Y₂ ⟶ M) (φ.unop ≫ CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop X)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
have rw₁ : Eq.{v + 1} (α := unop Y₂ ⟶ M) (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
  (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
Tactic: rw [← Category.assoc, toUnit_unique (φ.unop ≫ toUnit _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
rw :
  Eq (α := unop Y₂ ⟶ M) (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (φ.unop ≫ toUnit (unop X)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
rw₁ :
  Eq.{v + 1} (α := unop Y₂ ⟶ M) (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
⊢ Eq (α := unop Y₂ ⟶ M) (φ.unop ≫ CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop X)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
have rw₂ : unop Y₂ ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
Tactic: rw [← Category.assoc, toUnit_unique (φ.unop ≫ toUnit _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
f₁ f₂ : unop X ⟶ M
⊢ φ.unop ≫ (f₁ * f₂) = φ.unop ≫ f₁ * φ.unop ≫ f₂
have change : φ.unop ≫ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (φ.unop ≫ f₁) (φ.unop ≫ f₂)) μ
Tactic: change φ.unop ≫ lift f₁ f₂ ≫ μ = lift (φ.unop ≫ f₁) (φ.unop ≫ f₂) ≫ μ
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
f₁ f₂ : unop X ⟶ M
⊢ φ.unop ≫ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (φ.unop ≫ f₁) (φ.unop ≫ f₂)) μ
have rw : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (φ.unop ≫ lift f₁ f₂) μ =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (φ.unop ≫ f₁) (φ.unop ≫ f₂)) μ
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
⊢ ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst_2
have H : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M) μ μ
Tactic: ext