awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
| tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M ≫
      Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M))
have a : Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)
Tactic: rw [← leftUnitor_monoidal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
⊢ tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M ≫
        Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ =
    (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
have slice_lhs : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M) ⟶
    M)
  ((Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ μ)
  ((Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ)
Tactic: slice_lhs 1 3 => rw [← leftUnitor_monoidal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
⊢ (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        (μ ⊗ₘ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      Iso.hom (ρ_ M) =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ μ
have rw : (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⊗ₘ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        (μ ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
    Iso.hom (ρ_ M) =
  (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
Tactic: rw [← Category.id_comp μ, ← Category.comp_id (λ_ (𝟙_ C)).hom, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
⊢ (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⊗ₘ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
          (μ ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      Iso.hom (ρ_ M) =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
have simp : (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
    Iso.hom (ρ_ M) =
  (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
Tactic: simp only [tensorHom_id, id_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
| μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ M)
have a : Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ
Tactic: rw [rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
⊢ (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      Iso.hom (ρ_ M) =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
have slice_lhs : tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ =
  (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
Tactic: slice_lhs 3 4 => rw [rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
| tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M))
have a : Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)
Tactic: rw [← rightUnitor_monoidal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
⊢ tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
have slice_lhs : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
    M)
  ((Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ μ)
  ((Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ)
Tactic: slice_lhs 1 3 => rw [← rightUnitor_monoidal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W) (η ≫ (f ⊗ₘ g)) η
have dsimp : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
  ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g))
  (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: dsimp [tensorObj.one_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
| (η ⊗ₘ η) ≫ (f ⊗ₘ g)
have a : η ⊗ₘ η
Tactic: rw [tensorHom_comp_tensorHom, one_hom, one_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g))
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
  ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g))
  (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, one_hom, one_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
slice_lhs :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g))
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g))
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs₁ : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
  (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
  (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, one_hom, one_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    (μ ≫ (f ⊗ₘ g)) (((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ μ)
have dsimp : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
  ((tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g)) (((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ tensorμ Y W Y W ≫ (μ ⊗ₘ μ))
Tactic: dsimp [tensorObj.mul_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
| ((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ tensorμ Y W Y W
have a : tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)
Tactic: rw [tensorμ_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g)) (((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ tensorμ Y W Y W ≫ (μ ⊗ₘ μ))
have slice_rhs : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
  ((tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g)) ((tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ))
Tactic: slice_rhs 1 2 => rw [tensorμ_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
| (μ ⊗ₘ μ) ≫ (f ⊗ₘ g)
have a : ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g) ≫ (μ ⊗ₘ μ)
Tactic: rw [tensorHom_comp_tensorHom, mul_hom, mul_hom, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g)) ((tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ))
have slice_lhs : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
  (tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g) ≫ (μ ⊗ₘ μ)) ((tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ))
Tactic: slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, mul_hom, mul_hom, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y X) (η ≫ Iso.hom (β_ X Y)) η
have simp : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
  (η ⊗ₘ η)
Tactic: simp only [tensorObj.one_def, Category.assoc, BraidedCategory.braiding_naturality,
    braiding_tensorUnit_right, Iso.cancel_iso_inv_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
⊢ f = { hom := η, isMonHom_hom := ⋯ }
have w : f.hom = Hom.hom { hom := η, isMonHom_hom := sorry }
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
⊢ f.hom = Hom.hom { hom := η, isMonHom_hom := ⋯ }
have w : 𝟙 (Mon.X.{v₁, u₁} (trivial C)) ≫ f.hom = Hom.hom { hom := η, isMonHom_hom := sorry }
Tactic: rw [← Category.id_comp f.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
⊢ 𝟙 (Mon.X.{v₁, u₁} (trivial C)) ≫ f.hom = Hom.hom { hom := η, isMonHom_hom := ⋯ }
have w : 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ f.hom = η
Tactic: dsimp only [trivial_X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
⊢ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ f.hom = η
have w : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A.X) (η ≫ f.hom) η
Tactic: rw [← trivial_mon_one, IsMonHom.one_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
w : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A.X) (η ≫ f.hom) η
⊢ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ f.hom = η
have w₁ : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A.X) η η
Tactic: rw [← trivial_mon_one, IsMonHom.one_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Mon.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α := tensorObj (𝒞 := instCategory) X₁ X₂ ⟶ tensorObj (𝒞 := instCategory) Y₁ Y₂) (f ⊗ₘ g) (f ▷ X₂ ≫ Y₁ ◁ g)
have w : Eq (α := (tensorObj (𝒞 := instCategory) X₁ X₂).X ⟶ (tensorObj (𝒞 := instCategory) Y₁ Y₂).X) (Hom.hom (f ⊗ₘ g))
  (Hom.hom (f ▷ X₂ ≫ Y₁ ◁ g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (μ ≫ Iso.hom (β_ X Y)) ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫ μ)
have dsimp : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  ((tensorμ X Y X Y ≫ (μ ⊗ₘ μ)) ≫ Iso.hom (β_ X Y))
  ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫ tensorμ Y X Y X ≫ (μ ⊗ₘ μ))
Tactic: dsimp [tensorObj.mul_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    ((tensorμ X Y X Y ≫ (μ ⊗ₘ μ)) ≫ Iso.hom (β_ X Y))
    ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫ tensorμ Y X Y X ≫ (μ ⊗ₘ μ))
have simp : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  (Iso.hom (α_ X Y (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
    X ◁ Iso.inv (α_ Y X Y) ≫
      X ◁ Iso.hom (β_ Y X) ▷ Y ≫
        X ◁ Iso.hom (β_ X Y) ▷ Y ≫
          Iso.inv (α_ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) Y) ≫
            Iso.inv (α_ X Y X) ▷ Y ≫
              Iso.hom (β_ X Y) ▷ X ▷ Y ≫
                Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y) ≫
                  Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
                    Y ◁ X ◁ Iso.hom (β_ X Y) ≫
                      Y ◁ Iso.inv (α_ X Y X) ≫
                        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
                          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
  ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
      Y ◁ Iso.inv (α_ X Y X) ≫
        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
Tactic: simp only [tensorμ, Category.assoc, BraidedCategory.braiding_naturality,
    BraidedCategory.braiding_tensor_right_hom, BraidedCategory.braiding_tensor_left_hom,
    comp_whiskerRight, whisker_assoc, whiskerLeft_comp, pentagon_assoc,
    pentagon_inv_hom_hom_hom_inv_assoc, Iso.inv_hom_id_assoc, whiskerLeft_hom_inv_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
| X ◁ Iso.hom (β_ Y X) ▷ Y ≫ X ◁ Iso.hom (β_ X Y) ▷ Y
have a : X ◁ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) ▷ Y
Tactic: rw [← whiskerLeft_comp, ← comp_whiskerRight, SymmetricCategory.symmetry]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (Iso.hom (α_ X Y (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      X ◁ Iso.inv (α_ Y X Y) ≫
        X ◁ Iso.hom (β_ Y X) ▷ Y ≫
          X ◁ Iso.hom (β_ X Y) ▷ Y ≫
            Iso.inv (α_ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) Y) ≫
              Iso.inv (α_ X Y X) ▷ Y ≫
                Iso.hom (β_ X Y) ▷ X ▷ Y ≫
                  Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y) ≫
                    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
                      Y ◁ X ◁ Iso.hom (β_ X Y) ≫
                        Y ◁ Iso.inv (α_ X Y X) ≫
                          Y ◁ Iso.hom (β_ X Y) ▷ X ≫
                            Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
    ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
      Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
        Y ◁ Iso.inv (α_ X Y X) ≫
          Y ◁ Iso.hom (β_ X Y) ▷ X ≫
            Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
have slice_lhs : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
  (Iso.hom (α_ X Y (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
    X ◁ Iso.inv (α_ Y X Y) ≫
      ((((((((((X ◁ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) ▷ Y ≫
                            Iso.inv (α_ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) Y)) ≫
                          Iso.inv (α_ X Y X) ▷ Y) ≫
                        Iso.hom (β_ X Y) ▷ X ▷ Y) ≫
                      Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) X Y)) ≫
                    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))) ≫
                  Y ◁ X ◁ Iso.hom (β_ X Y)) ≫
                Y ◁ Iso.inv (α_ X Y X)) ≫
              Y ◁ Iso.hom (β_ X Y) ▷ X) ≫
            Y ◁ Iso.hom (α_ Y X X)) ≫
          Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X))) ≫
        (μ ⊗ₘ μ))
  ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫
    Iso.hom (α_ Y X (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) ≫
      Y ◁ Iso.inv (α_ X Y X) ≫
        Y ◁ Iso.hom (β_ X Y) ▷ X ≫
          Y ◁ Iso.hom (α_ Y X X) ≫ Iso.inv (α_ Y Y (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) ≫ (μ ⊗ₘ μ))
Tactic: slice_lhs 3 4 =>
    -- We use symmetry here:
    rw [← whiskerLeft_comp, ← comp_whiskerRight, SymmetricCategory.symmetry]