-- Mathlib/RepresentationTheory/GroupCohomology/Basic.lean
theorem d_eq :
    d n A =
      ((diagonalHomEquiv n A).toModuleIso.inv ≫
        (linearYonedaObjResolution A).d n (n + 1) ≫
          (diagonalHomEquiv (n + 1) A).toModuleIso.hom).hom

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ d n A =
    ModuleCat.Hom.hom
      ((diagonalHomEquiv n A).toModuleIso.inv ≫
        (linearYonedaObjResolution A).d n (n + 1) ≫ (diagonalHomEquiv (n + 1) A).toModuleIso.hom)

Tactic:
ext f g

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g =
    (ModuleCat.Hom.hom
        ((diagonalHomEquiv n A).toModuleIso.inv ≫
          (linearYonedaObjResolution A).d n (n + 1) ≫ (diagonalHomEquiv (n + 1) A).toModuleIso.hom))
      f g

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g = (diagonalHomEquiv (n + 1) A) ((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g

Tactic:
rw [diagonalHomEquiv_apply, Action.comp_hom, ConcreteCategory.comp_apply, resolution.d_eq]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g =
    (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
      ((ConcreteCategory.hom (ModuleCat.ofHom (resolution.d k G (n + 1)))) (Finsupp.single (Fin.partialProd g) 1))

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 => x1 * x2) g) =
    (A.ρ (g 0))
        (f fun i =>
          (Fin.partialProd g i.castSucc.castSucc * g i.castSucc)⁻¹ * (Fin.partialProd g i.succ.castSucc * g i.succ)) +
      ∑ i : Fin (n + 1),
        (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
          ((-1) ^ ↑i.succ • Finsupp.single (Fin.partialProd g ∘ i.succ.succAbove) 1)

Tactic:
rcongr x

Result:
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
x : Fin n
⊢ g x.succ = (Fin.partialProd g x.castSucc.castSucc * g x.castSucc)⁻¹ * (Fin.partialProd g x.succ.castSucc * g x.succ)

case h.h.e_a.e_f.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
x : Fin (n + 1)
⊢ (-1) ^ (↑x + 1) • f (x.contractNth (fun x1 x2 => x1 * x2) g) =
    (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
      ((-1) ^ ↑x.succ • Finsupp.single (Fin.partialProd g ∘ x.succ.succAbove) 1)

Proof state:
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
x : Fin n
⊢ g x.succ = (Fin.partialProd g x.castSucc.castSucc * g x.castSucc)⁻¹ * (Fin.partialProd g x.succ.castSucc * g x.succ)

Tactic:
have := Fin.partialProd_right_inv g (Fin.castSucc x)

Result:
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
x : Fin n
this : (Fin.partialProd g x.castSucc.castSucc)⁻¹ * Fin.partialProd g x.castSucc.succ = g x.castSucc
⊢ g x.succ = (Fin.partialProd g x.castSucc.castSucc * g x.castSucc)⁻¹ * (Fin.partialProd g x.succ.castSucc * g x.succ)

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 => x1 * x2) g) =
    (A.ρ ((Fin.partialProd g ∘ Fin.succ) 0))
        (f fun i => ((Fin.partialProd g ∘ Fin.succ) i.castSucc)⁻¹ * (Fin.partialProd g ∘ Fin.succ) i.succ) +
      ∑ i : Fin (n + 1),
        (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
          ((-1) ^ ↑i.succ • Finsupp.single (Fin.partialProd g ∘ i.succ.succAbove) 1)

Tactic:
simp_rw [Function.comp_apply, Fin.partialProd_succ, Fin.castSucc_zero,
  Fin.partialProd_zero, one_mul]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 => x1 * x2) g) =
    (A.ρ (g 0))
        (f fun i =>
          (Fin.partialProd g i.castSucc.castSucc * g i.castSucc)⁻¹ * (Fin.partialProd g i.succ.castSucc * g i.succ)) +
      ∑ i : Fin (n + 1),
        (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
          ((-1) ^ ↑i.succ • Finsupp.single (Fin.partialProd g ∘ i.succ.succAbove) 1)

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g =
    (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
      ((ConcreteCategory.hom (ModuleCat.ofHom (resolution.d k G (n + 1)))) (Finsupp.single (Fin.partialProd g) 1))

Tactic:
erw [resolution.d_of (Fin.partialProd g)]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g =
    (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
      (∑ p : Fin (n + 1 + 1), Finsupp.single (Fin.partialProd g ∘ p.succAbove) ((-1) ^ ↑p))

Proof state:
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
x : Fin n
this : (Fin.partialProd g x.castSucc.castSucc)⁻¹ * Fin.partialProd g x.castSucc.succ = g x.castSucc
⊢ g x.succ =
    (g x.castSucc)⁻¹ * (Fin.partialProd g x.castSucc.castSucc)⁻¹ * (Fin.partialProd g x.castSucc.succ * g x.succ)

Tactic:
rw [mul_assoc, ← mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left]

Result:
no goals

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g =
    ∑ x : Fin (n + 1 + 1),
      (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
        ((-1) ^ ↑x • Finsupp.single (Fin.partialProd g ∘ x.succAbove) 1)

Tactic:
erw [d_apply, @Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul,
  Fin.succAbove_zero, diagonalHomEquiv_symm_apply f (Fin.partialProd g ∘ @Fin.succ (n + 1))]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 => x1 * x2) g) =
    (A.ρ ((Fin.partialProd g ∘ Fin.succ) 0))
        (f fun i => ((Fin.partialProd g ∘ Fin.succ) i.castSucc)⁻¹ * (Fin.partialProd g ∘ Fin.succ) i.succ) +
      ∑ i : Fin (n + 1),
        (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
          ((-1) ^ ↑i.succ • Finsupp.single (Fin.partialProd g ∘ i.succ.succAbove) 1)

Proof state:
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
x : Fin n
this : (Fin.partialProd g x.castSucc.castSucc)⁻¹ * Fin.partialProd g x.castSucc.succ = g x.castSucc
⊢ g x.succ = (Fin.partialProd g x.castSucc.castSucc * g x.castSucc)⁻¹ * (Fin.partialProd g x.succ.castSucc * g x.succ)

Tactic:
simp only [mul_inv_rev, Fin.castSucc_fin_succ] at this ⊢

Result:
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
x : Fin n
this : (Fin.partialProd g x.castSucc.castSucc)⁻¹ * Fin.partialProd g x.castSucc.succ = g x.castSucc
⊢ g x.succ =
    (g x.castSucc)⁻¹ * (Fin.partialProd g x.castSucc.castSucc)⁻¹ * (Fin.partialProd g x.castSucc.succ * g x.succ)