-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← Subsingleton.elim (α := Fin 0 → G) default (fun i ↦ y), Subsingleton.elim
    (Fin.contractNth 0 _) default, Pi.default_def]