-- 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 default : (↑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))
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 default : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a (default (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
        (↑A : Type u))
hf₂ 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 default : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a
          ((fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1) → G) ↦ (default : (k : Fin 0) → G))
            (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
        (↑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 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))

Tactic:
rw [← Subsingleton.elim (α := Fin 0 → G) default (fun i ↦ y), Subsingleton.elim
    (Fin.contractNth 0 _) default, Pi.default_def]

Premises used: Inhabited.default, Pi.default_def, Subsingleton.elim, OfNat.ofNat, Fin.contractNth