-- Module: Mathlib.CategoryTheory.Monoidal.Grp
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)) η)
rw₅ 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)) η)
⊢ μ ≫ 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:
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]

Premises used: CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc, CategoryTheory.MonObj.lift_comp_one_left, CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.CategoryStruct.comp, CategoryTheory.GrpObj.lift_comp_inv_left, CategoryTheory.SemiCartesianMonoidalCategory.fst