awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
rw : Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _) (CategoryTheory.inv (@inv _ _ inst_1 _ _))
rw₁ :
  Eq.{v₁ + 1} (α := A ⟶ A) (CategoryTheory.inv (CategoryTheory.inv (@inv _ _ inst_1 _ _)) ≫ @inv _ _ inst_1 _ _) (𝟙 A)
rw₂ : Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (𝟙 A)
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (CategoryTheory.inv (@inv _ _ inst_1 _ _)) (@inv _ _ inst_1 _ _)
have rw₃ : Eq.{v₁ + 1} (α := A ⟶ A) (𝟙 A) (𝟙 A)
Tactic: rw [eq_comm, ← CategoryTheory.inv_comp_eq_id, IsIso.inv_inv, inv_comp_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (μ ≫ @inv _ _ inst_1 _ _)
    (Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
have apply : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (μ ≫ @inv _ _ inst_1 _ _) μ) μ)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ) μ) μ)
Tactic: apply lift_left_mul_ext μ
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (μ ≫ @inv _ _ inst_1 _ _) μ) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ) μ) μ)
have nth_rw : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (μ ≫ @inv _ _ inst_1 _ _) (μ ≫ 𝟙 A)) μ)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ) μ) μ)
Tactic: nth_rw 2 [← Category.comp_id μ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (μ ≫ @inv _ _ inst_1 _ _) (μ ≫ 𝟙 A)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ) μ) μ)
have rw : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (snd A A ≫ @inv _ _ inst_1 _ _)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (fst A A ≫ @inv _ _ inst_1 _ _) μ) μ))
    μ)
Tactic: rw [← comp_lift, Category.assoc, left_inv, ← Category.assoc (β_ A A).hom,
    ← lift_snd_fst, lift_map, lift_lift_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (fst A A ≫ @inv _ _ inst_1 _ _) μ) μ))
      μ)
have nth_rw : μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (snd A A ≫ @inv _ _ inst_1 _ _)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        (lift (fst A A ≫ @inv _ _ inst_1 _ _) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫ μ)) μ))
    μ
Tactic: nth_rw 2 [← Category.id_comp μ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
⊢ μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫ μ)) μ))
      μ
have rw : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (snd A A ≫ @inv _ _ inst_1 _ _)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        (lift (fst A A ≫ @inv _ _ inst_1 _ _)
          (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (fst A A) (snd A A)) μ))
        μ))
    μ)
Tactic: rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left,
    lift_comp_inv_left, comp_toUnit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _)
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (fst A A) (snd A A)) μ))
          μ))
      μ)
⊢ μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫ μ)) μ))
      μ
have rw₁ : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (snd A A ≫ @inv _ _ inst_1 _ _)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        (lift
          (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
            (lift (fst A A ≫ @inv _ _ inst_1 _ _) (fst A A)) μ)
          (snd A A))
        μ))
    μ)
Tactic: rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left,
    lift_comp_inv_left, comp_toUnit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _)
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (fst A A) (snd A A)) μ))
          μ))
      μ)
rw₁ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
              (lift (fst A A ≫ @inv _ _ inst_1 _ _) (fst A A)) μ)
            (snd A A))
          μ))
      μ)
⊢ μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫ μ)) μ))
      μ
have rw₂ : μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (snd A A ≫ @inv _ _ inst_1 _ _)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        (lift
          (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) η)
          (snd A A))
        μ))
    μ
Tactic: rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left,
    lift_comp_inv_left, comp_toUnit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _)
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (fst A A) (snd A A)) μ))
          μ))
      μ)
rw₁ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
              (lift (fst A A ≫ @inv _ _ inst_1 _ _) (fst A A)) μ)
            (snd A A))
          μ))
      μ)
rw₂ :
  μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift
            (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
              η)
            (snd A A))
          μ))
      μ
⊢ μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫ μ)) μ))
      μ
have rw₃ : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (snd A A ≫ @inv _ _ inst_1 _ _) (snd A A)) μ)
Tactic: rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left,
    lift_comp_inv_left, comp_toUnit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _)
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (fst A A) (snd A A)) μ))
          μ))
      μ)
rw₁ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
              (lift (fst A A ≫ @inv _ _ inst_1 _ _) (fst A A)) μ)
            (snd A A))
          μ))
      μ)
rw₂ :
  μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift
            (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
              η)
            (snd A A))
          μ))
      μ
rw₃ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (snd A A ≫ @inv _ _ inst_1 _ _) (snd A A)) μ)
⊢ μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫ μ)) μ))
      μ
have rw₄ : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) η)
Tactic: rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left,
    lift_comp_inv_left, comp_toUnit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _)
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (fst A A) (snd A A)) μ))
          μ))
      μ)
rw₁ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift
            (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
              (lift (fst A A ≫ @inv _ _ inst_1 _ _) (fst A A)) μ)
            (snd A A))
          μ))
      μ)
rw₂ :
  μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift
            (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
              η)
            (snd A A))
          μ))
      μ
rw₃ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (snd A A ≫ @inv _ _ inst_1 _ _) (snd A A)) μ)
rw₄ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) η)
⊢ μ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (snd A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (fst A A ≫ @inv _ _ inst_1 _ _) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫ μ)) μ))
      μ
have rw₅ : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) η)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) η)
Tactic: rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left,
    lift_comp_inv_left, comp_toUnit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
    (Iso.hom (β_ A A) ≫ μ ≫ @inv _ _ inst_1 _ _)
have rw : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
  (Iso.hom (β_ A A) ≫ Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
Tactic: rw [mul_inv A, SymmetricCategory.symmetry_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
    (Iso.hom (β_ A A) ≫ Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
    (Iso.hom (β_ A A) ≫ μ ≫ @inv _ _ inst_1 _ _)
have rw₁ : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
  ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
Tactic: rw [mul_inv A, SymmetricCategory.symmetry_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
⊢ Eq.{v₁ + 1} (α := A ≅ A) (mulRight η) (Iso.refl A)
have w : Eq.{v₁ + 1} (α := A ⟶ A) (Iso.hom (mulRight η)) (Iso.hom (Iso.refl A))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
⊢ ∀
    (s :
      PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        μ μ),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
        ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s)
        (μ ▷ A) =
      s.fst
have refine : ∀
  (s :
    PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ
      μ),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
        ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s)
        (μ ▷ A))
      (fst A A) =
    s.fst ≫ fst A A
Tactic: refine fun s => CartesianMonoidalCategory.hom_ext _ _ ?_ (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
        ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s)
        (μ ▷ A))
      (fst A A) =
    s.fst ≫ fst A A
have simp : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (s.snd ≫ fst A A)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
    μ =
  s.fst ≫ fst A A
Tactic: simp only [lift_whiskerRight, lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
      μ =
    s.fst ≫ fst A A
have rw : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        (lift (s.snd ≫ fst A A) (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _)) μ)
      (s.fst ≫ fst A A))
    μ =
  s.fst ≫ fst A A
Tactic: rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_left]