-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem diagonalSucc_hom_single (f : Gⁿ⁺¹) (a : k) :
    (diagonalSucc k G n).hom.hom (single f a) =
      single (f 0) 1 ⊗ₜ single (fun i => (f (Fin.castSucc i))⁻¹ * f i.succ) a

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ModuleCat.Hom.hom
        (𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom))
      (single ((Equiv.refl (G × (Fin n → G))) (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)).1 1 ⊗ₜ[k]
        single ((Equiv.refl (G × (Fin n → G))) (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)).2 a) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a

Tactic:
rfl

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ModuleCat.Hom.hom
        (𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom))
      (↑(finsuppTensorFinsupp' k G (Fin n → G)).symm ((lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a

Tactic:
erw [lmapDomain_apply, mapDomain_single, LinearEquiv.coe_toLinearMap, finsuppTensorFinsupp',
  LinearEquiv.trans_symm, LinearEquiv.trans_apply, lcongr_symm, Equiv.refl_symm]

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ModuleCat.Hom.hom
        (𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom))
      ((finsuppTensorFinsupp k k k k G (Fin n → G)).symm
        ((lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k).symm)
          (single ((actionDiagonalSucc G n).hom.hom f) a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ConcreteCategory.hom (diagonalSucc k G n).hom.hom) (single f a) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a

Tactic:
dsimp [diagonalSucc]

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ModuleCat.Hom.hom
        (𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom))
      (↑(finsuppTensorFinsupp' k G (Fin n → G)).symm ((lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ModuleCat.Hom.hom
        (𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom))
      ((finsuppTensorFinsupp k k k k G (Fin n → G)).symm
        ((lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k).symm)
          (single ((actionDiagonalSucc G n).hom.hom f) a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a

Tactic:
erw [lcongr_single]

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ModuleCat.Hom.hom
        (𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom))
      ((finsuppTensorFinsupp k k k k G (Fin n → G)).symm
        (single ((Equiv.refl (G × (Fin n → G))) ((actionDiagonalSucc G n).hom.hom f))
          ((TensorProduct.lid k k).symm a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ModuleCat.Hom.hom
        (𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom))
      ((finsuppTensorFinsupp k k k k G (Fin n → G)).symm
        (single ((Equiv.refl (G × (Fin n → G))) ((actionDiagonalSucc G n).hom.hom f))
          ((TensorProduct.lid k k).symm a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a

Tactic:
rw [TensorProduct.lid_symm_apply, actionDiagonalSucc_hom_apply, finsuppTensorFinsupp_symm_single]

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ (ModuleCat.Hom.hom
        (𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom))
      (single ((Equiv.refl (G × (Fin n → G))) (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)).1 1 ⊗ₜ[k]
        single ((Equiv.refl (G × (Fin n → G))) (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)).2 a) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a