awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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)
⊢ 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)
have 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)
Tactic: induction x using Fin.cases
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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 (α := 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)
have 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
Tactic: simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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
⊢ 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)
have 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
Tactic: simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
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))
have zero : ∀ (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: induction n with
  | zero => exact Prod.ext rfl (funext fun x => Fin.elim0 x)
  | succ n hn =>
    refine Prod.ext rfl (funext fun x => ?_)
    induction x using Fin.cases
    <;> simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]
    <;> rfl
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
f : Fin (n + 1) → G
zero :
  ∀ (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))
⊢ 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))
have succ : ∀ (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: induction n with
  | zero => exact Prod.ext rfl (funext fun x => Fin.elim0 x)
  | succ n hn =>
    refine Prod.ext rfl (funext fun x => ?_)
    induction x using Fin.cases
    <;> simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]
    <;> rfl
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
g : G
f : Fin 0 → G
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G 0))) :
        (a : (leftRegular G).V ⊗ (Fin 0 → G)) → (diagonal G (0 + 1)).V)
      (g, f) =
    g • Fin.partialProd f
have zero : ∀ (x : Fin 1),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G 0))) :
        (a : (leftRegular G).V ⊗ (Fin 0 → G)) → (diagonal G (0 + 1)).V)
      (g, f) x =
    (g • Fin.partialProd f) x
Tactic: funext (x : Fin 1)
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) =
    g • Fin.partialProd f
have succ : ∀ (x : Fin (n + 1 + 1)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) x =
    (g • Fin.partialProd f) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) 0 =
    (g • Fin.partialProd f) 0
have succ : (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
      (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
    (g, f) 0 =
  g
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
x : Fin (n + 1 + 1)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) x =
    (g • Fin.partialProd f) x
have succ : (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
      (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
    (g, f) 0 =
  (g • Fin.partialProd f) 0
Tactic: induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using congrFun (hn (g * f 0) (Fin.tail f)) i
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
x : Fin (n + 1 + 1)
succ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) 0 =
    (g • Fin.partialProd f) 0
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) x =
    (g • Fin.partialProd f) x
have succ₁ : ∀ (i : Fin (n + 1)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) i.succ =
    (g • Fin.partialProd f) i.succ
Tactic: induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using congrFun (hn (g * f 0) (Fin.tail f)) i
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
g : G
f : Fin n → G
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
        (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
      (g, f) =
    g • Fin.partialProd f
have zero : ∀ (g : G) (f : Fin 0 → G),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G 0))) :
        (a : (leftRegular G).V ⊗ (Fin 0 → G)) → (diagonal G (0 + 1)).V)
      (g, f) =
    g • Fin.partialProd f
Tactic: induction n generalizing g with
  | zero =>
    funext (x : Fin 1)
    simp [diagonalSuccIsoTensorTrivial, diagonalOneIsoLeftRegular, Subsingleton.elim x 0,
      ofMulAction_V, types_tensorObj_def, types_tensorUnit_def]
  | succ n hn =>
    funext x
    induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using congrFun (hn (g * f 0) (Fin.tail f)) i
Cleared hypotheses: n, g, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
g : G
f : Fin n → G
zero :
  ∀ (g : G) (f : Fin 0 → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G 0))) :
          (a : (leftRegular G).V ⊗ (Fin 0 → G)) → (diagonal G (0 + 1)).V)
        (g, f) =
      g • Fin.partialProd f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
        (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
      (g, f) =
    g • Fin.partialProd f
have succ : ∀ (n : ℕ)
  (hn :
    ∀ (g : G) (f : Fin n → G),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
            (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
          (g, f) =
        g • Fin.partialProd f)
  (g : G) (f : Fin (n + 1) → G),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) =
    g • Fin.partialProd f
Tactic: induction n generalizing g with
  | zero =>
    funext (x : Fin 1)
    simp [diagonalSuccIsoTensorTrivial, diagonalOneIsoLeftRegular, Subsingleton.elim x 0,
      ofMulAction_V, types_tensorObj_def, types_tensorUnit_def]
  | succ n hn =>
    funext x
    induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using congrFun (hn (g * f 0) (Fin.tail f)) i
Cleared hypotheses: n, g, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
g : G
⊢ Eq.{v_2 + 1} (α :=
    Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) ⟶
      Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
    (CategoryStruct.comp (Y :=
        Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
        ((ρ ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) : (a : G) → End (𝟙_ (Action W G)).V) g) (ε F) :
      Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) ⟶
        Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
    (CategoryStruct.comp (Y := Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        (ε F)
        (((ρ (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) :
              MonoidHom.{u_2, v_2} G
                (End (Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))))) :
            (a : G) → End ((F.mapAction G).obj (𝟙_ (Action V G))).V)
          g) :
      Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) ⟶
        Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
have dsimp : 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) ≫ ε F = ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
Tactic: dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
g : G
⊢ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) ≫ ε F = ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
have rw : Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F)
  (ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
Tactic: rw [Category.id_comp, F.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
g : G
rw :
  Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F)
    (ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
⊢ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) ≫ ε F = ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
have rw₁ : Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F)
  (ε F ≫ 𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
Tactic: rw [Category.id_comp, F.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
g : G
rw :
  Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F)
    (ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
rw₁ :
  Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F)
    (ε F ≫ 𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
⊢ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) ≫ ε F = ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
have rw₂ : Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F) (ε F)
Tactic: rw [Category.id_comp, F.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
x_1 : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    tensorObj (𝒞 := instCategory) (obj (F.mapAction G) X) (obj (F.mapAction G) x_1) ⟶
      obj (F.mapAction G) (tensorObj (𝒞 := instCategory) Y x_1))
    (map (F.mapAction G) x ▷ obj (F.mapAction G) x_1 ≫ { hom := μ F Y.V x_1.V, comm := ⋯ })
    ({ hom := μ F X.V x_1.V, comm := ⋯ } ≫ map (F.mapAction G) (x ▷ x_1))
have h : Eq (α :=
  (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) X) (obj (F.mapAction G) x_1)).V ⟶
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) Y x_1)).V)
  (Hom.hom (map (F.mapAction G) x ▷ obj (F.mapAction G) x_1 ≫ { hom := μ F Y.V x_1.V, comm := sorry }))
  (Hom.hom ({ hom := μ F X.V x_1.V, comm := sorry } ≫ map (F.mapAction G) (x ▷ x_1)))
Tactic: ext