-- 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
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
⊢ (actionDiagonalSucc G (n + 1)).inv.hom (g, f) = g • partialProd f

Tactic:
funext x

Result:
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)
⊢ (actionDiagonalSucc G (n + 1)).inv.hom (g, f) x = (g • partialProd f) x

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.consEquiv fun a => G)
      (g,
        (actionDiagonalSucc G n).inv.hom
          ((leftRegular G ⊗ { V := Fin n → G, ρ := 1 }).ρ g ((Fin.insertNthEquiv (fun x => G) 0).symm f)))
      x =
    g * partialProd f x

Tactic:
erw [hn, Fin.consEquiv_apply]

Result:
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

Proof state:
case succ
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), (actionDiagonalSucc G (n + 1)).inv.hom (g, f) = g • partialProd f

Tactic:
intro g

Result:
case succ
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
⊢ (actionDiagonalSucc G (n + 1)).inv.hom (g, f) = g • partialProd f

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

Tactic:
revert g

Result:
G : Type u
inst✝ : Group G
n : ℕ
f : Fin n → G
⊢ ∀ (g : G), (actionDiagonalSucc G n).inv.hom (g, f) = g • partialProd f