-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem actionDiagonalSucc_inv_apply {G : Type u} [Group G] {n : ℕ} (g : G) (f : Fin n → G) :
    (actionDiagonalSucc G n).inv.hom (g, f) = (g • Fin.partialProd f : Fin (n + 1) → G)

Proof state:
case succ.h.refine_2
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), (actionDiagonalSucc G n).inv.hom (g, f) = g • partialProd f
f : Fin (n + 1) → G
g : G
x : Fin (n + 1 + 1)
i : Fin (n + 1)
⊢ Fin.cons
      (g,
          (Limits.BinaryFan.mk
                  ((ChosenFiniteProducts.product
                              (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj
                                PUnit.unit)
                              (((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).obj
                                PUnit.unit)).cone.π.app
                      { as := Limits.WalkingPair.left } ≫
                    ((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).map g)
                  ((ChosenFiniteProducts.product
                              (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj
                                PUnit.unit)
                              (((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).obj
                                PUnit.unit)).cone.π.app
                      { as := Limits.WalkingPair.right } ≫
                    ((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).map g)).fst
              ((Fin.insertNthEquiv (fun x => G) 0).symm f) •
            partialProd
              ((Limits.BinaryFan.mk
                    ((ChosenFiniteProducts.product
                                (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj
                                  PUnit.unit)
                                (((functorCategoryEquivalence (Type u) G).symm.inverse.obj
                                      { V := Fin n → G, ρ := 1 }).obj
                                  PUnit.unit)).cone.π.app
                        { as := Limits.WalkingPair.left } ≫
                      ((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).map g)
                    ((ChosenFiniteProducts.product
                                (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj
                                  PUnit.unit)
                                (((functorCategoryEquivalence (Type u) G).symm.inverse.obj
                                      { V := Fin n → G, ρ := 1 }).obj
                                  PUnit.unit)).cone.π.app
                        { as := Limits.WalkingPair.right } ≫
                      ((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).map g)).snd
                ((Fin.insertNthEquiv (fun x => G) 0).symm f))).1
      (g,
          (Limits.BinaryFan.mk
                  ((ChosenFiniteProducts.product
                              (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj
                                PUnit.unit)
                              (((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).obj
                                PUnit.unit)).cone.π.app
                      { as := Limits.WalkingPair.left } ≫
                    ((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).map g)
                  ((ChosenFiniteProducts.product
                              (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj
                                PUnit.unit)
                              (((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).obj
                                PUnit.unit)).cone.π.app
                      { as := Limits.WalkingPair.right } ≫
                    ((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).map g)).fst
              ((Fin.insertNthEquiv (fun x => G) 0).symm f) •
            partialProd
              ((Limits.BinaryFan.mk
                    ((ChosenFiniteProducts.product
                                (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj
                                  PUnit.unit)
                                (((functorCategoryEquivalence (Type u) G).symm.inverse.obj
                                      { V := Fin n → G, ρ := 1 }).obj
                                  PUnit.unit)).cone.π.app
                        { as := Limits.WalkingPair.left } ≫
                      ((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).map g)
                    ((ChosenFiniteProducts.product
                                (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj
                                  PUnit.unit)
                                (((functorCategoryEquivalence (Type u) G).symm.inverse.obj
                                      { V := Fin n → G, ρ := 1 }).obj
                                  PUnit.unit)).cone.π.app
                        { as := Limits.WalkingPair.right } ≫
                      ((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).map g)).snd
                ((Fin.insertNthEquiv (fun x => G) 0).symm f))).2
      i.succ =
    g * partialProd f i.succ

Tactic:
simp only [Fin.cons_succ, Pi.smul_apply, smul_eq_mul, Fin.partialProd_succ', ← mul_assoc]

Result:
case succ.h.refine_2
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), (actionDiagonalSucc G n).inv.hom (g, f) = g • partialProd f
f : Fin (n + 1) → G
g : G
x : Fin (n + 1 + 1)
i : Fin (n + 1)
⊢ (Limits.BinaryFan.mk
            ((ChosenFiniteProducts.product
                        (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj PUnit.unit)
                        (((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).obj
                          PUnit.unit)).cone.π.app
                { as := Limits.WalkingPair.left } ≫
              ((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).map g)
            ((ChosenFiniteProducts.product
                        (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj PUnit.unit)
                        (((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).obj
                          PUnit.unit)).cone.π.app
                { as := Limits.WalkingPair.right } ≫
              ((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).map g)).fst
        ((Fin.insertNthEquiv (fun x => G) 0).symm f) *
      partialProd
        ((Limits.BinaryFan.mk
              ((ChosenFiniteProducts.product
                          (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj PUnit.unit)
                          (((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).obj
                            PUnit.unit)).cone.π.app
                  { as := Limits.WalkingPair.left } ≫
                ((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).map g)
              ((ChosenFiniteProducts.product
                          (((functorCategoryEquivalence (Type u) G).symm.inverse.obj (leftRegular G)).obj PUnit.unit)
                          (((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).obj
                            PUnit.unit)).cone.π.app
                  { as := Limits.WalkingPair.right } ≫
                ((functorCategoryEquivalence (Type u) G).symm.inverse.obj { V := Fin n → G, ρ := 1 }).map g)).snd
          ((Fin.insertNthEquiv (fun x => G) 0).symm f))
        i =
    g * f 0 * partialProd (Fin.tail f) i