-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : Fin 0 → G
a : (↑A : Type u)
y : G
hf :
  HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) =
    HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a fun (i : Fin 0) ↦ y : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a
          (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2) (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
        (↑A : Type u))
⊢ Eq (α := (↑A : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ d₀₁ A) ∘ₗ LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u))
        a y :
      (↑A : Type u))
    ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1 ≫ (cochainsIso₁ A).hom) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u))
        a y :
      (↑A : Type u))

Tactic:
simp only [cochainsIso₀, LinearEquiv.toModuleIso_hom, ModuleCat.hom_comp,
    ConcreteCategory.hom_ofHom, LinearMap.coe_comp, LinearEquiv.coe_coe,
    LinearEquiv.funUnique_apply, LinearMap.coe_single, Function.comp_apply, Function.eval,
    d₀₁_hom_apply, zero_add, ↓reduceDIte, Nat.reduceAdd, eqToHom_refl, Category.comp_id,
    cochainsIso₁, Iso.symm_hom, LinearEquiv.toModuleIso_inv, LinearEquiv.funCongrLeft_symm,
    LinearEquiv.funCongrLeft_apply, Equiv.funUnique_symm_apply, LinearMap.funLeft_apply,
    inhomogeneousCochains.d_hom_apply, Fin.isValue, uniqueElim_const, Finset.univ_unique,
    Fin.default_eq_zero, Fin.val_eq_zero, pow_one, neg_smul, one_smul, Finset.sum_neg_distrib,
    Finset.sum_singleton, ← sub_eq_add_neg, CochainComplex.of.d]

Premises used: neg_smul, groupCohomology.d₀₁_hom_apply, LinearEquiv.toModuleIso_inv, CochainComplex.of.d, groupCohomology.cochainsIso₀, sub_eq_add_neg, CategoryTheory.Iso.symm_hom, groupCohomology.cochainsIso₁, LinearEquiv.funCongrLeft_apply, reduceDIte, Finset.univ_unique, Nat.reduceAdd, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, Function.eval, zero_add, one_smul, Finset.sum_singleton, uniqueElim_const, Fin.val_eq_zero, inhomogeneousCochains.d_hom_apply, Fin.isValue, LinearMap.coe_comp, LinearMap.coe_single, LinearEquiv.funUnique_apply, pow_one, LinearMap.funLeft_apply, Function.comp_apply, Fin.default_eq_zero, Equiv.funUnique_symm_apply, Finset.sum_neg_distrib, ModuleCat.hom_comp, CategoryTheory.ConcreteCategory.hom_ofHom, LinearEquiv.toModuleIso_hom, LinearEquiv.coe_coe, LinearEquiv.funCongrLeft_symm