-- 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
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)
⊢ 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
      x =
    g * partialProd f x

Tactic:
refine Fin.cases ?_ (fun i => ?_) x

Result:
case succ.h.refine_1
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)
⊢ 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
      0 =
    g * partialProd f 0

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