-- 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)
⊢ (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

Tactic:
rfl

Result:
no goals

Proof state:
case zero
G : Type u
inst✝ : Group G
f : Fin 0 → G
g : G
⊢ (actionDiagonalSucc G 0).inv.hom (g, f) = g • partialProd f

Tactic:
funext (x : Fin 1)

Result:
case zero.h
G : Type u
inst✝ : Group G
f : Fin 0 → G
g : G
x : Fin 1
⊢ (actionDiagonalSucc G 0).inv.hom (g, f) x = (g • partialProd f) x

Proof state:
case zero
G : Type u
inst✝ : Group G
f : Fin 0 → G
⊢ ∀ (g : G), (actionDiagonalSucc G 0).inv.hom (g, f) = g • partialProd f

Tactic:
intro g

Result:
case zero
G : Type u
inst✝ : Group G
f : Fin 0 → G
g : G
⊢ (actionDiagonalSucc G 0).inv.hom (g, f) = g • partialProd f