-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem diagonalHomEquiv_symm_apply (f : (Fin n → G) → A) (x : Fin (n + 1) → G) :
    ((diagonalHomEquiv n A).symm f).hom (Finsupp.single x 1) =
      A.ρ (x 0) (f fun i : Fin n => (x (Fin.castSucc i))⁻¹ * x i.succ)

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
x : Fin (n + 1) → G
⊢ (ConcreteCategory.hom
        ((((Linear.homCongr k (diagonalSucc k G n ≪≫ (Representation.ofMulAction k G G).repOfTprodIso 1)
                        (Iso.refl A)).trans
                    ((MonoidalClosed.linearHomEquivComm (of (Representation.ofMulAction k G G)) (of 1) A).trans
                      ((ihom (of 1)).obj A).leftRegularHomEquiv)).trans
                (llift (↑A.V) k k (Fin n → G)).symm).symm
            f).hom)
      (single x 1) =
    (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)

Tactic:
simp only [LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
  leftRegularHomEquiv_symm_apply, Linear.homCongr_symm_apply, Iso.trans_hom, Iso.refl_inv,
  Category.comp_id, Action.comp_hom, MonoidalClosed.linearHomEquivComm_symm_hom,
  ModuleCat.hom_comp, LinearMap.comp_apply]

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
x : Fin (n + 1) → G
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom
          ((TensorProduct.uncurry k (G →₀ k)
              ↑(((Action.functorCategoryEquivalence (ModuleCat k) G).symm.inverse.obj
                      (trivial k G ((Fin n → G) →₀ k))).obj
                  PUnit.unit)
              ↑A.V)
            (ModuleCat.Hom.hom (((ihom (of 1)).obj A).leftRegularHom ((llift (↑A.V) k k (Fin n → G)) f)).hom))))
      ((ModuleCat.Hom.hom ((Representation.ofMulAction k G G).repOfTprodIso 1).hom.hom)
        ((ModuleCat.Hom.hom (diagonalSucc k G n).hom.hom) (single x 1))) =
    (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
x : Fin (n + 1) → G
⊢ (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom) (single x 1) =
    (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)

Tactic:
unfold diagonalHomEquiv

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
x : Fin (n + 1) → G
⊢ (ConcreteCategory.hom
        ((((Linear.homCongr k (diagonalSucc k G n ≪≫ (Representation.ofMulAction k G G).repOfTprodIso 1)
                        (Iso.refl A)).trans
                    ((MonoidalClosed.linearHomEquivComm (of (Representation.ofMulAction k G G)) (of 1) A).trans
                      ((ihom (of 1)).obj A).leftRegularHomEquiv)).trans
                (llift (↑A.V) k k (Fin n → G)).symm).symm
            f).hom)
      (single x 1) =
    (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
x : Fin (n + 1) → G
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom
          ((TensorProduct.uncurry k (G →₀ k)
              ↑(((Action.functorCategoryEquivalence (ModuleCat k) G).symm.inverse.obj
                      (trivial k G ((Fin n → G) →₀ k))).obj
                  PUnit.unit)
              ↑A.V)
            (ModuleCat.Hom.hom (((ihom (of 1)).obj A).leftRegularHom ((llift (↑A.V) k k (Fin n → G)) f)).hom))))
      ((ModuleCat.Hom.hom ((Representation.ofMulAction k G G).repOfTprodIso 1).hom.hom)
        ((ModuleCat.Hom.hom (diagonalSucc k G n).hom.hom) (single x 1))) =
    (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)

Tactic:
rw [diagonalSucc_hom_single]

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
x : Fin (n + 1) → G
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom
          ((TensorProduct.uncurry k (G →₀ k)
              ↑(((Action.functorCategoryEquivalence (ModuleCat k) G).symm.inverse.obj
                      (trivial k G ((Fin n → G) →₀ k))).obj
                  PUnit.unit)
              ↑A.V)
            (ModuleCat.Hom.hom (((ihom (of 1)).obj A).leftRegularHom ((llift (↑A.V) k k (Fin n → G)) f)).hom))))
      ((ModuleCat.Hom.hom ((Representation.ofMulAction k G G).repOfTprodIso 1).hom.hom)
        (single (x 0) 1 ⊗ₜ[k] single (fun i => (x i.castSucc)⁻¹ * x i.succ) 1)) =
    (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)