awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
inst_3 : BraidedCategory.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
g : G
⊢ Eq.{v_1 + 1} (α := (tensorObj (𝒞 := instCategory) X Y).V ⟶ (tensorObj (𝒞 := instCategory) Y X).V)
    (((tensorObj (𝒞 := instCategory) X Y).ρ : (a : G) → End (X ⊗ Y).V) g ≫ Iso.hom (β_ X.V Y.V) :
      (tensorObj (𝒞 := instCategory) X Y).V ⟶ (tensorObj (𝒞 := instCategory) Y X).V)
    (Iso.hom (β_ X.V Y.V) ≫ ((tensorObj (𝒞 := instCategory) Y X).ρ : (a : G) → End (Y ⊗ X).V) g :
      (tensorObj (𝒞 := instCategory) X Y).V ⟶ (tensorObj (𝒞 := instCategory) Y X).V)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
inst_3 : BraidedCategory.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
⊢ Eq (α := (tensorObj (𝒞 := instCategory) X Y).V ⟶ (tensorObj (𝒞 := instCategory) Y X).V) (Hom.hom (Iso.hom (β_ X Y)))
    (Iso.hom (β_ X.V Y.V))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
inst_3 : BraidedCategory.{v_1, u_1} V
X Y : Action.{v_1, u_1, u_2} V G
⊢ Eq (α := (tensorObj (𝒞 := instCategory) Y X).V ⟶ (tensorObj (𝒞 := instCategory) X Y).V) (Hom.hom (Iso.inv (β_ X Y)))
    (Iso.inv (β_ X.V Y.V))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
      ((𝟙_ (CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)) (𝒞 := Functor.category))
      (Functor.obj functor ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
    (ε functor) (𝟙 ((𝟙_ (CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)) (𝒞 := Functor.category)))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
      (Functor.obj functor ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
      ((𝟙_ (CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)) (𝒞 := Functor.category)))
    (η functor) (𝟙 (Functor.obj functor ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
A B : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    tensorObj (𝒞 := Functor.category) (Functor.obj functor A) (Functor.obj functor B) ⟶
      Functor.obj functor (tensorObj (𝒞 := instCategory) A B))
    (μ functor A B) (𝟙 (tensorObj (𝒞 := Functor.category) (Functor.obj functor A) (Functor.obj functor B)))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.id, CategoryTheory.Monoidal.FunctorCategory.tensorObj, rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
A B : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    Functor.obj functor (tensorObj (𝒞 := instCategory) A B) ⟶
      tensorObj (𝒞 := Functor.category) (Functor.obj functor A) (Functor.obj functor B))
    (δ functor A B) (𝟙 (Functor.obj functor (tensorObj (𝒞 := instCategory) A B)))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.id, CategoryTheory.Monoidal.FunctorCategory.tensorObj, rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_3 : Group H
inst_4 : RightRigidCategory.{v_1, u_1} V
⊢ RightRigidCategory (CategoryTheory.Functor.{u_3, v_1, 0, u_1} (SingleObj H) V)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_3 : Group H
inst_4 : LeftRigidCategory.{v_1, u_1} V
⊢ LeftRigidCategory (CategoryTheory.Functor.{u_3, v_1, 0, u_1} (SingleObj H) V)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_3 : Group H
inst_4 : RigidCategory.{v_1, u_1} V
⊢ RigidCategory (CategoryTheory.Functor.{u_3, v_1, 0, u_1} (SingleObj H) V)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_2 : Group H
X : Action.{v_1, u_1, u_3} V H
inst_3 : RightRigidCategory.{v_1, u_1} V
⊢ (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V =
    @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_2 : Group H
X : Action.{v_1, u_1, u_3} V H
inst_3 : LeftRigidCategory.{v_1, u_1} V
⊢ (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V =
    @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_2 : Group H
X : Action.{v_1, u_1, u_3} V H
inst_3 : RightRigidCategory.{v_1, u_1} V
h : H
rw :
  Eq.{v_1 + 1} (α := End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    (((@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End Xᘁ.V) h :
      End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    ((X.ρ : (a : H) → End X.V) (inv h)ᘁ :
      @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _)
x y : SingleObj H
⊢ Eq.{v_1 + 1} (α := End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    (((@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End Xᘁ.V) h :
      End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    ((X.ρ : (a : H) → End X.V) h⁻¹ᘁ :
      @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _)

Tactic:
rw [← SingleObj.inv_as_inv]

Premises used: CategoryTheory.SingleObj.inv_as_inv
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_2 : Group H
X : Action.{v_1, u_1, u_3} V H
inst_3 : LeftRigidCategory.{v_1, u_1} V
h : H
rw :
  Eq.{v_1 + 1} (α := End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (((@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End (ᘁX).V) h :
      End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (ᘁ(X.ρ : (a : H) → End X.V) (inv h) :
      @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _)
x y : SingleObj H
⊢ Eq.{v_1 + 1} (α := End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (((@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End (ᘁX).V) h :
      End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (ᘁ(X.ρ : (a : H) → End X.V) h⁻¹ :
      @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _)

Tactic:
rw [← SingleObj.inv_as_inv]

Premises used: CategoryTheory.SingleObj.inv_as_inv
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
X : Action (Type u) G
x : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V
⊢ ((fun (g : Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V))) ↦
          ((g.1,
              (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                  (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                g.2) :
            Action.V (leftRegular G) × X.V))
        ((fun (g : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V) ↦
            ((g.1,
                (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                    (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                  g.2) :
              Action.V (leftRegular G) × Action.V (trivial G X.V)))
          x)).2 =
    x.2

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
X : Action (Type u) G
x : Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V))
⊢ ((fun (g : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V) ↦
          ((g.1,
              (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                  (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                g.2) :
            Action.V (leftRegular G) × Action.V (trivial G X.V)))
        ((fun (g : Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V))) ↦
            ((g.1,
                (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                    (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                  g.2) :
              Action.V (leftRegular G) × X.V))
          x)).2 =
    x.2

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
X : Action (Type u) G
x : G
x_1 : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V
⊢ Eq (α := X.V)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1.1⁻¹) : (a : X.V) → X.V) x_1.2 :
      X.V)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((1 : (a : G) → End X.V) x) : (a : X.V) → X.V)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1.1⁻¹) : (a : X.V) → X.V)
            x_1.2 :
          X.V) :
      X.V)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
f : Fin (HAdd.hAdd (α := ℕ) 0 1) → G
⊢ Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin 0 → G))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G 0))) :
          (a : (diagonal G (0 + 1)).V) → (leftRegular G).V ⊗ (Fin 0 → G))
        f :
      tensorObj (𝒞 := types) (V (leftRegular G)) (Fin 0 → G))
    ((f 0, fun (i : Fin 0) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin 0) → G))

Tactic:
Prod.ext rfl (funext fun x => Fin.elim0 x)

Premises used: funext, Prod.ext, rfl, Fin.elim0
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
f : Fin (HAdd.hAdd (α := ℕ) 0 1) → G
⊢ Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin 0 → G))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G 0))) :
          (a : (diagonal G (0 + 1)).V) → (leftRegular G).V ⊗ (Fin 0 → G))
        f :
      tensorObj (𝒞 := types) (V (leftRegular G)) (Fin 0 → G))
    ((f 0, fun (i : Fin 0) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin 0) → G))

Tactic:
exact Prod.ext rfl (funext fun x => Fin.elim0 x)

Premises used: funext, Prod.ext, rfl, Fin.elim0
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
f : Fin (n + 1 + 1) → G
⊢ Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin (n + 1) → G))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
          (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
        f :
      tensorObj (𝒞 := types) (V (leftRegular G)) (Fin (n + 1) → G))
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin (n + 1)) → G))

Tactic:
Prod.ext rfl (funext fun x => ?_)

Premises used: funext, Prod.ext, rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
f : Fin (n + 1 + 1) → G
succ :
  ∀ (x : Fin (n + 1)),
    Eq (α := G)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
              (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
            f).2
        x)
      ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 x)
⊢ Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin (n + 1) → G))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
          (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
        f :
      tensorObj (𝒞 := types) (V (leftRegular G)) (Fin (n + 1) → G))
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin (n + 1)) → G))

Tactic:
refine Prod.ext rfl (funext fun x => ?_)

Premises used: funext, Prod.ext, rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
succ :
  Eq (α := G)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
            (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
          f).2
      0)
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 0)
succ₁ :
  ∀ (i : Fin n),
    Eq (α := G)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
              (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
            f).2
        i.succ)
      ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 i.succ)
⊢ Eq (α := G)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
            (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
          f).2
      x)
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 x)

Tactic:
induction x using Fin.cases
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
f : Fin (n + 1 + 1) → G
succ :
  ∀
    (hn :
      ∀ (f : Fin (n + 1) → G),
        Eq (α := V (leftRegular G) × (Fin n → G))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
                (a : (diagonal G (n + 1)).V) → (leftRegular G).V × (Fin n → G))
              f :
            V (leftRegular G) × (Fin n → G))
          ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))),
    ((Fin.consEquiv.{u} (n := n) fun (x : Fin (n + 1)) ↦ G : G × ((i : Fin n) → G) ≃ ((i : Fin (n + 1)) → G)) :
          (a : (leftRegular G).V × (Fin n → G)) → Fin (n + 1) → G)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                ((ρ (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G (Fin n → G))) :
                    (a : G) → End ((leftRegular G).V × (Fin n → G)))
                  ((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                          (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                        f).1⁻¹) :
              (a : (leftRegular G).V × (Fin n → G)) → (leftRegular G).V × (Fin n → G))
            (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                      (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                    f).2
                0,
              fun (i : Fin n) ↦
              HMul.hMul (α := G)
                (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                          (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                        f).2
                    i.castSucc)⁻¹
                (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                        (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                      f).2
                  i.succ)) :
          V (leftRegular G) × (Fin n → G))
        0 =
      (f 0)⁻¹ * f 1
⊢ Eq (α := G)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
            (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
          f).2
      0)
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 0)

Tactic:
simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]

Premises used: Action.diagonalSuccIsoTensorTrivial, CategoryTheory.types_tensorObj_def
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
f : Fin (n + 1 + 1) → G
i : Fin n
succ :
  ∀
    (hn :
      ∀ (f : Fin (n + 1) → G),
        Eq (α := V (leftRegular G) × (Fin n → G))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
                (a : (diagonal G (n + 1)).V) → (leftRegular G).V × (Fin n → G))
              f :
            V (leftRegular G) × (Fin n → G))
          ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))),
    ((Fin.consEquiv.{u} (n := n) fun (x : Fin (n + 1)) ↦ G : G × ((i : Fin n) → G) ≃ ((i : Fin (n + 1)) → G)) :
          (a : (leftRegular G).V × (Fin n → G)) → Fin (n + 1) → G)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                ((ρ (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G (Fin n → G))) :
                    (a : G) → End ((leftRegular G).V × (Fin n → G)))
                  ((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                          (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                        f).1⁻¹) :
              (a : (leftRegular G).V × (Fin n → G)) → (leftRegular G).V × (Fin n → G))
            (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                      (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                    f).2
                0,
              fun (i : Fin n) ↦
              HMul.hMul (α := G)
                (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                          (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                        f).2
                    i.castSucc)⁻¹
                (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                        (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                      f).2
                  i.succ)) :
          V (leftRegular G) × (Fin n → G))
        i.succ =
      (f i.castSucc.succ)⁻¹ * f i.succ.succ
⊢ Eq (α := G)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
            (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
          f).2
      i.succ)
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 i.succ)

Tactic:
simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]

Premises used: Action.diagonalSuccIsoTensorTrivial, CategoryTheory.types_tensorObj_def