awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f g h : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
have this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
    (μ ▷ B ≫ μ) =
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
    (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)
Tactic: have := lift (lift f g) h ≫= mul_assoc B
-- 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
A B : C
inst_2 : MonObj B
f g h : A ⟶ B
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (μ ▷ B ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
have rwa : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B)
        (lift (lift f g) h) (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)),
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
Tactic: rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this
Cleared hypotheses: this
-- 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
A B : C
inst_2 : MonObj B
f g h : A ⟶ B
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (μ ▷ B ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
        CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B)
          (lift (lift f g) h) (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
have rwa₁ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B (tensorObj.{v, u_1} (𝒞 := inst) B B))
        (lift f (lift g h)) (B ◁ μ ≫ μ)),
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
Tactic: rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this
Cleared hypotheses: this
-- 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
A B : C
inst_2 : MonObj B
f g h : A ⟶ B
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (μ ▷ B ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
        CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B)
          (lift (lift f g) h) (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
        CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B (tensorObj.{v, u_1} (𝒞 := inst) B B))
          (lift f (lift g h)) (B ◁ μ ≫ μ)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
have rwa₂ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ),
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
Tactic: rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
g : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g
have this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) B) (lift f g) (η ▷ B ≫ μ) =
  lift f g ≫ Iso.hom (λ_ B)
Tactic: have := lift f g ≫= one_mul B
-- 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
A B : C
inst_2 : MonObj B
f : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
g : A ⟶ B
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) B) (lift f g)
      (η ▷ B ≫ μ) =
    lift f g ≫ Iso.hom (λ_ B)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g
have rwa : ∀ (this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = lift f g ≫ Iso.hom (λ_ B)),
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g
Tactic: rwa [lift_whiskerRight_assoc, lift_leftUnitor_hom] at this
Cleared hypotheses: this
-- 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
A B : C
inst_2 : MonObj B
f : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
g : A ⟶ B
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) B) (lift f g)
      (η ▷ B ≫ μ) =
    lift f g ≫ Iso.hom (λ_ B)
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = lift f g ≫ Iso.hom (λ_ B)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g
have rwa₁ : ∀ (this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g),
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g
Tactic: rwa [lift_whiskerRight_assoc, lift_leftUnitor_hom] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f : A ⟶ B
g : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f
have this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f g) (B ◁ η ≫ μ) =
  lift f g ≫ Iso.hom (ρ_ B)
Tactic: have := lift f g ≫= mul_one B
-- 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
A B : C
inst_2 : MonObj B
f : A ⟶ B
g : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f g)
      (B ◁ η ≫ μ) =
    lift f g ≫ Iso.hom (ρ_ B)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f
have rwa : ∀ (this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = lift f g ≫ Iso.hom (ρ_ B)),
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f
Tactic: rwa [lift_whiskerLeft_assoc, lift_rightUnitor_hom] at this
Cleared hypotheses: this
-- 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
A B : C
inst_2 : MonObj B
f : A ⟶ B
g : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f g)
      (B ◁ η ≫ μ) =
    lift f g ≫ Iso.hom (ρ_ B)
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = lift f g ≫ Iso.hom (ρ_ B)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f
have rwa₁ : ∀ (this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f),
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f
Tactic: rwa [lift_whiskerLeft_assoc, lift_rightUnitor_hom] at this
Cleared hypotheses: this
-- 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_1 N O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M : Mon.{v, u_1} C
f : M ⟶ (𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory)
⊢ f =
    (fun (M : Mon.{v, u_1} C) ↦
        ({ hom := toUnit M.X, isMonHom_hom := ⋯ } : M.Hom ((𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory))))
      M
have w : f.hom =
  Hom.hom
    ((fun (M : Mon.{v, u_1} C) ↦
        ({ hom := toUnit M.X, isMonHom_hom := sorry } : M.Hom ((𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory))))
      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_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
⊢ Eq (α := tensorObj (𝒞 := instCategory) M N ⟶ M) { hom := fst M.X N.X, isMonHom_hom := ⋯ }
    (M ◁
        IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯)
          N ≫
      Iso.hom (ρ_ M))
have w : Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ M.X) (Hom.hom { hom := fst M.X N.X, isMonHom_hom := sorry })
  (Hom.hom
    (M ◁
        IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := sorry }) sorry)
          N ≫
      Iso.hom (ρ_ 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_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ M.X) (Hom.hom { hom := fst M.X N.X, isMonHom_hom := ⋯ })
    (Hom.hom
      (M ◁
          IsTerminal.from
            (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯) N ≫
        Iso.hom (ρ_ M)))
have w : Eq.{v + 1} (α :=
  tensorObj.{v, u_1} (𝒞 := inst) M.X N.X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M.X (tensorUnit.{v, u_1} C (𝒞 := inst)))
  (M.X ◁ IsTerminal.from isTerminalTensorUnit N.X)
  (M.X ◁
    Hom.hom
      (IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := sorry }) sorry)
        N))
Tactic: simp [fst_def]
-- 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_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
⊢ Eq (α := tensorObj (𝒞 := instCategory) M N ⟶ N) { hom := snd M.X N.X, isMonHom_hom := ⋯ }
    (IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯)
          M ▷
        N ≫
      Iso.hom (λ_ N))
have w : Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ N.X) (Hom.hom { hom := snd M.X N.X, isMonHom_hom := sorry })
  (Hom.hom
    (IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := sorry }) sorry)
          M ▷
        N ≫
      Iso.hom (λ_ N)))
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_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ N.X) (Hom.hom { hom := snd M.X N.X, isMonHom_hom := ⋯ })
    (Hom.hom
      (IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯)
            M ▷
          N ≫
        Iso.hom (λ_ N)))
have w : Eq.{v + 1} (α :=
  tensorObj.{v, u_1} (𝒞 := inst) M.X N.X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) N.X)
  (IsTerminal.from isTerminalTensorUnit M.X ▷ N.X)
  (Hom.hom
      (IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := sorry }) sorry)
        M) ▷
    N.X)
Tactic: simp [snd_def]
-- 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
⊢ f₁ * f₂ * f₃ = f₁ * (f₂ * f₃)
have change : 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 f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
Tactic: change lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift f₁ (lift 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₁ f₂ f₃ : X ⟶ 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) 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 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 ≫ μ)
Tactic: trans lift (lift f₁ 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) 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 ≫ μ)
⊢ 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 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 M)
    (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
Tactic: trans lift (lift f₁ 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) 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) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
    (lift (lift f₁ f₂) f₃) ((μ ⊗ₘ 𝟙 M) ≫ μ)
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
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) ≫ μ)
⊢ 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₃ ≫ 𝟙 M)) μ
Tactic: rw [← tensorHom_id, lift_map_assoc, Category.comp_id]