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

Tactic:
dsimp [actionDiagonalSucc]

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.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

Proof state:
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) 0 = g

Tactic:
rfl

Result:
no goals

Proof state:
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

Tactic:
simp only [Subsingleton.elim x 0, Pi.smul_apply, Fin.partialProd_zero, smul_eq_mul, mul_one]

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) 0 = g

Proof state:
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

Tactic:
simp only [Fin.insertNth_zero, Fin.cons_zero, Fin.partialProd_zero, mul_one]

Result:
no goals