-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem d_eq (n : ℕ) : ((groupCohomology.resolution k G).d (n + 1) n).hom =
    ModuleCat.ofHom (d k G (n + 1))

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (ModuleCat.Hom.hom
        ((-1) ^ ↑x✝¹ •
          ModuleCat.ofHom (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom)))
      (single x 1) =
    single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)

Tactic:
simp only [ModuleCat.hom_smul, SimplexCategory.len_mk, ModuleCat.hom_ofHom]

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ ((-1) ^ ↑x✝¹ • lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom) (single x 1) =
    single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
⊢ ((resolution k G).d (n + 1) n).hom = ModuleCat.ofHom (d k G (n + 1))

Tactic:
ext : 1

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
⊢ ModuleCat.Hom.hom ((resolution k G).d (n + 1) n).hom = ModuleCat.Hom.hom (ModuleCat.ofHom (d k G (n + 1)))

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ ∑ c : Fin (n + 2),
      (ModuleCat.Hom.hom
          ((-1) ^ ↑c •
            ModuleCat.ofHom (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ c).op).hom)))
        (single x 1) =
    ∑ p : Fin ((Opposite.unop (Opposite.op (SimplexCategory.mk (n + 1)))).len + 1), single (x ∘ p.succAbove) ((-1) ^ ↑p)

Tactic:
refine Finset.sum_congr rfl fun _ _ => ?_

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (ModuleCat.Hom.hom
        ((-1) ^ ↑x✝¹ •
          ModuleCat.ofHom (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom)))
      (single x 1) =
    single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ ∑ c : Fin (n + 2),
      (ModuleCat.Hom.hom
          ((-1) ^ ↑c •
            ModuleCat.ofHom (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ c).op).hom)))
        (single x 1) =
    (d k G (n + 1)) (single x 1)

Tactic:
erw [d_of (k := k) x]

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ ∑ c : Fin (n + 2),
      (ModuleCat.Hom.hom
          ((-1) ^ ↑c •
            ModuleCat.ofHom (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ c).op).hom)))
        (single x 1) =
    ∑ p : Fin ((Opposite.unop (Opposite.op (SimplexCategory.mk (n + 1)))).len + 1), single (x ∘ p.succAbove) ((-1) ^ ↑p)

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ (ModuleCat.Hom.hom ((resolution k G).d (n + 1) n).hom ∘ₗ lsingle x) 1 =
    (ModuleCat.Hom.hom (ModuleCat.ofHom (d k G (n + 1))) ∘ₗ lsingle x) 1

Tactic:
dsimp [groupCohomology.resolution]

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ (ModuleCat.Hom.hom
        (((alternatingFaceMapComplex (Rep k G)).obj (classifyingSpaceUniversalCover G ⋙ Rep.linearization k G)).d
            (n + 1) n).hom)
      (single x 1) =
    (d k G (n + 1)) (single x 1)

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ (ModuleCat.Hom.hom
        (((alternatingFaceMapComplex (Rep k G)).obj (classifyingSpaceUniversalCover G ⋙ Rep.linearization k G)).d
            (n + 1) n).hom)
      (single x 1) =
    (d k G (n + 1)) (single x 1)

Tactic:
simp_rw [alternatingFaceMapComplex_obj_d, AlternatingFaceMapComplex.objD, SimplicialObject.δ,
  Functor.comp_map, ← Int.cast_smul_eq_zsmul k ((-1) ^ _ : ℤ), Int.cast_pow, Int.cast_neg,
  Int.cast_one, Action.sum_hom, Action.smul_hom, Rep.linearization_map_hom]

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ (ModuleCat.Hom.hom
        (∑ x : Fin (n + 2),
          (-1) ^ ↑x •
            ModuleCat.ofHom (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x).op).hom)))
      (single x 1) =
    (d k G (n + 1)) (single x 1)

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ (ModuleCat.Hom.hom
        (∑ x : Fin (n + 2),
          (-1) ^ ↑x •
            ModuleCat.ofHom (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x).op).hom)))
      (single x 1) =
    (d k G (n + 1)) (single x 1)

Tactic:
rw [ModuleCat.hom_sum, LinearMap.coeFn_sum, Fintype.sum_apply]

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ ∑ c : Fin (n + 2),
      (ModuleCat.Hom.hom
          ((-1) ^ ↑c •
            ModuleCat.ofHom (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ c).op).hom)))
        (single x 1) =
    (d k G (n + 1)) (single x 1)

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
⊢ ModuleCat.Hom.hom ((resolution k G).d (n + 1) n).hom = ModuleCat.Hom.hom (ModuleCat.ofHom (d k G (n + 1)))

Tactic:
refine Finsupp.lhom_ext' fun x => LinearMap.ext_ring ?_

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ (ModuleCat.Hom.hom ((resolution k G).d (n + 1) n).hom ∘ₗ lsingle x) 1 =
    (ModuleCat.Hom.hom (ModuleCat.ofHom (d k G (n + 1))) ∘ₗ lsingle x) 1

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (-1) ^ ↑x✝¹ • (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom) (single x 1) =
    single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)

Tactic:
rw [Finsupp.lmapDomain_apply, Finsupp.mapDomain_single, Finsupp.smul_single', mul_one]

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ single (((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom x) ((-1) ^ ↑x✝¹) =
    single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)