awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f g h : A ⟶ B
⊢ f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ ↔
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f g h : A ⟶ B
refine_1 :
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ →
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h
refine_2 :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h →
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ
⊢ f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ ↔
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
g h : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift g (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ)) μ =
    h

Tactic:
simp [← lift_lift_assoc]

Premises used: CategoryTheory.MonObj.lift_lift_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f g : A ⟶ B
⊢ f =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (g ≫ @inv _ _ inst_1 _ _) (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ)) μ

Tactic:
simp [← lift_lift_assoc]

Premises used: CategoryTheory.MonObj.lift_lift_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f g h : A ⟶ B
rw :
  h = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) g) μ ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
rw₂ rw₃ :
  g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) g) μ = h ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ

Tactic:
rw [eq_comm, eq_lift_inv_left, eq_comm]

Premises used: eq_comm, CategoryTheory.GrpObj.eq_lift_inv_left
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f g h : A ⟶ B
⊢ f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ ↔
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f g h : A ⟶ B
refine_1 :
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ →
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g
refine_2 :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g →
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ
⊢ f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ ↔
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
g h : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ) h) μ =
    g

Tactic:
simp [lift_lift_assoc]

Premises used: CategoryTheory.MonObj.lift_lift_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f h : A ⟶ B
⊢ f =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ) (h ≫ @inv _ _ inst_1 _ _)) μ

Tactic:
simp [lift_lift_assoc]

Premises used: CategoryTheory.MonObj.lift_lift_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f g h : A ⟶ B
rw :
  h = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (g ≫ @inv _ _ inst_1 _ _)) μ ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ = f ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
rw₂ rw₃ :
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (g ≫ @inv _ _ inst_1 _ _)) μ = h ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ

Tactic:
rw [eq_comm, eq_lift_inv_right, eq_comm]

Premises used: eq_comm, CategoryTheory.GrpObj.eq_lift_inv_right
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f g i : A ⟶ B
h :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f i) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ
rwa :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ) (i ≫ @inv _ _ inst_1 _ _))
          μ),
    f = g
rwa₁ :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift g (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift i (i ≫ @inv _ _ inst_1 _ _)) μ))
          μ),
    f = g
rwa₂ :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift g (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)) μ),
    f = g
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : f = g), f = g
⊢ f = g

Tactic:
rwa [← eq_lift_inv_right, lift_lift_assoc, lift_comp_inv_right, lift_comp_one_right] at h

Premises used: CategoryTheory.MonObj.lift_comp_one_right, CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.GrpObj.eq_lift_inv_right, CategoryTheory.GrpObj.lift_comp_inv_right
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
apply :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ)
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (𝟙 A)

Tactic:
apply lift_left_mul_ext ι[A]

Premises used: CategoryTheory.GrpObj.inv, CategoryTheory.GrpObj.lift_left_mul_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
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)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
rw₁ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (@inv _ _ inst_1 _ _ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
rw₂ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (@inv _ _ inst_1 _ _ ≫
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) μ)
rw₃ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _ ≫ 𝟙 A)) μ)
rw₄ rw₅ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
⊢ Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ)

Tactic:
rw [right_inv, ← comp_toUnit_assoc ι, ← left_inv, comp_lift_assoc, Category.comp_id]

Premises used: CategoryTheory.GrpObj.inv, CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc, CategoryTheory.Category.comp_id, CategoryTheory.GrpObj.left_inv, CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc, CategoryTheory.GrpObj.right_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G X_1 : C
inst_2 : GrpObj G
A B G' X : C
inst_3 : AddGrpObj G'
e : G' ≅ X
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X)
      (lift (e.inv ≫ @AddGrpObj.neg _ _ inst_1 _ _ ≫ e.hom) (𝟙 X)) AddMonObj.add =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) AddMonObj.zero

Tactic:
simp +instances [AddMonObj.ofIso]

Premises used: CategoryTheory.AddMonObj.ofIso
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G X_1 : C
inst_2 : GrpObj G
A B G' X : C
inst_3 : AddGrpObj G'
e : G' ≅ X
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X)
      (lift (𝟙 X) (e.inv ≫ @AddGrpObj.neg _ _ inst_1 _ _ ≫ e.hom)) AddMonObj.add =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) AddMonObj.zero

Tactic:
simp +instances [AddMonObj.ofIso]

Premises used: CategoryTheory.AddMonObj.ofIso
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G X : C
inst_2 : GrpObj G
A B : C
e : G ≅ X
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (e.inv ≫ @inv _ _ inst_1 _ _ ≫ e.hom) (𝟙 X)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η

Tactic:
simp +instances [MonObj.ofIso]

Premises used: CategoryTheory.MonObj.ofIso
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G X : C
inst_2 : GrpObj G
A B : C
e : G ≅ X
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (𝟙 X) (e.inv ≫ @inv _ _ inst_1 _ _ ≫ e.hom)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η

Tactic:
simp +instances [MonObj.ofIso]

Premises used: CategoryTheory.MonObj.ofIso
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G X : C
inst_2 : GrpObj G
A_1 B A : C
inst_3 : GrpObj A
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (𝟙 A)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
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)
rw₃ rw₄ : Eq.{v₁ + 1} (α := A ⟶ A) (𝟙 A) (𝟙 A)
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (CategoryTheory.inv (@inv _ _ inst_1 _ _)) (@inv _ _ inst_1 _ _)

Tactic:
rw [eq_comm, ← CategoryTheory.inv_comp_eq_id, IsIso.inv_inv, inv_comp_inv]

Premises used: CategoryTheory.IsIso.inv_inv, eq_comm, CategoryTheory.inv_comp_eq_id, CategoryTheory.GrpObj.inv_comp_inv
-- 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
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 _ _) ≫ μ) μ) μ)
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (μ ≫ @inv _ _ inst_1 _ _)
    (Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)

Tactic:
apply lift_left_mul_ext μ

Premises used: CategoryTheory.GrpObj.lift_left_mul_ext, CategoryTheory.MonObj.mul
-- 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
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 _ _) ≫ μ) μ) μ)
⊢ 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:
nth_rw 2 [← Category.comp_id μ]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.MonObj.mul
-- 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 _ _) μ) μ))
      μ)
⊢ 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:
rw [← comp_lift, Category.assoc, left_inv, ← Category.assoc (β_ A A).hom,
    ← lift_snd_fst, lift_map, lift_lift_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.CartesianMonoidalCategory.comp_lift, CategoryTheory.GrpObj.left_inv, CategoryTheory.BraidedCategory.braiding, CategoryTheory.CartesianMonoidalCategory.lift_map, CategoryTheory.Iso.hom, CategoryTheory.CartesianMonoidalCategory.lift_snd_fst
-- 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
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) ≫ μ)) μ))
      μ
⊢ 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:
nth_rw 2 [← Category.id_comp μ]

Premises used: CategoryTheory.MonObj.mul, CategoryTheory.Category.id_comp
-- 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) ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
    (Iso.hom (β_ A A) ≫ Iso.hom (β_ A A) ≫ (@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
rw₁ rw₂ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ μ)
    ((@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 _ _)

Tactic:
rw [mul_inv A, SymmetricCategory.symmetry_assoc]

Premises used: CategoryTheory.SymmetricCategory.symmetry_assoc, CategoryTheory.GrpObj.mul_inv
-- 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
G : C
inst_3 : GrpObj G
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) G G ⟶ G) (μ ≫ @inv _ _ inst_1 _ _)
    ((@inv _ _ inst_1 _ _ ⊗ₘ @inv _ _ inst_1 _ _) ≫ Iso.hom (β_ G G) ≫ μ)

Tactic:
simp [tensorHom_inv_inv_mul]

Premises used: CategoryTheory.GrpObj.tensorHom_inv_inv_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G X : C
inst_2 : GrpObj G
A_1 B A : C
inst_3 : GrpObj A
f : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (toUnit A ≫ f)) μ ≫
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (toUnit A ≫ f ≫ @inv _ _ inst_1 _ _))
        μ =
    𝟙 A

Tactic:
simp [comp_lift_assoc, lift_lift_assoc, ← comp_lift]

Premises used: CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.CartesianMonoidalCategory.comp_lift, CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G X : C
inst_2 : GrpObj G
A_1 B A : C
inst_3 : GrpObj A
f : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (toUnit A ≫ f ≫ @inv _ _ inst_1 _ _)) μ ≫
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (toUnit A ≫ f)) μ =
    𝟙 A

Tactic:
simp [comp_lift_assoc, lift_lift_assoc, ← comp_lift]

Premises used: CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.CartesianMonoidalCategory.comp_lift, CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
w : Eq.{v₁ + 1} (α := A ⟶ A) (Iso.hom (mulRight η)) (Iso.hom (Iso.refl A))
⊢ Eq.{v₁ + 1} (α := A ≅ A) (mulRight η) (Iso.refl A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
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) (Iso.hom (mulRight η)) (Iso.hom (Iso.refl A))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ⟶ A) (μ ▷ A ≫ μ)
    ((Iso.hom (α_ A A A) ≫ A ◁ μ) ≫ μ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
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))
      (snd A A) =
    s.fst ≫ snd A A

Tactic:
simp