-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑((inhomogeneousCochains A).X 2) : Type u)
y : G × G × G
hf :
  HAdd.hAdd (α := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (x
            (Fin.cons (α := fun (x : Fin 2) ↦ G) y.2.1
              (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))) :
        (↑A : Type u))
      (-x
            (Fin.cons (α := fun (x : Fin 2) ↦ G) (y.1 * y.2.1)
              (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.2 (finZeroElim (α := fun (i : Fin 0) ↦ G)))) +
        (x
            (Fin.cons (α := fun (x : Fin 2) ↦ G) y.1
              (Fin.cons (α := fun (i : Fin 1) ↦ G) (y.2.1 * y.2.2) (finZeroElim (α := fun (i : Fin 0) ↦ G)))) +
          -x
              (Fin.cons (α := fun (x : Fin 2) ↦ G) y.1
                (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.1 (finZeroElim (α := fun (i : Fin 0) ↦ G)))))) =
    HAdd.hAdd (α := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u))
                (Fin.cons (α := fun (a : Fin 3) ↦ G) y.1
                  (Fin.cons (α := fun (x : Fin 2) ↦ G) y.2.1
                    (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
                  0) :
              (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (x fun (i : Fin 2) ↦
            Fin.cons (α := fun (a : Fin 3) ↦ G) y.1
              (Fin.cons (α := fun (x : Fin 2) ↦ G) y.2.1
                (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
              i.succ) :
        (↑A : Type u))
      (-x
            (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2)
              (((Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G :
                    G × ((i : Fin 2) → G) ≃ ((i : Fin (HAdd.hAdd (α := ℕ) 2 1)) → G)) :
                  (a : G × ((i : Fin 2) → G)) → (i : Fin 3) → G)
                (Prod.map id
                  (fun (p : G × G) ↦
                    Fin.cons (α := fun (x : Fin 2) ↦ G) p.1
                      (Fin.cons (α := fun (i : Fin 1) ↦ G) p.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
                  y))) +
        (x
            (Fin.contractNth 1 (fun (x1 x2 : G) ↦ x1 * x2)
              (((Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G :
                    G × ((i : Fin 2) → G) ≃ ((i : Fin (HAdd.hAdd (α := ℕ) 2 1)) → G)) :
                  (a : G × ((i : Fin 2) → G)) → (i : Fin 3) → G)
                (Prod.map id
                  (fun (p : G × G) ↦
                    Fin.cons (α := fun (x : Fin 2) ↦ G) p.1
                      (Fin.cons (α := fun (i : Fin 1) ↦ G) p.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
                  y))) +
          -x
              (Fin.contractNth 2 (fun (x1 x2 : G) ↦ x1 * x2)
                (((Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G :
                      G × ((i : Fin 2) → G) ≃ ((i : Fin (HAdd.hAdd (α := ℕ) 2 1)) → G)) :
                    (a : G × ((i : Fin 2) → G)) → (i : Fin 3) → G)
                  (Prod.map id
                    (fun (p : G × G) ↦
                      Fin.cons (α := fun (x : Fin 2) ↦ G) p.1
                        (Fin.cons (α := fun (i : Fin 1) ↦ G) p.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
                    y)))))
⊢ HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              (x
                (Fin.cons (α := fun (x : Fin 2) ↦ G) y.2.1
                  (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))) :
            (↑A : Type u))
          (x
            (Fin.cons (α := fun (x : Fin 2) ↦ G) (y.1 * y.2.1)
              (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))) +
        x
          (Fin.cons (α := fun (x : Fin 2) ↦ G) y.1
            (Fin.cons (α := fun (i : Fin 1) ↦ G) (y.2.1 * y.2.2) (finZeroElim (α := fun (i : Fin 0) ↦ G)))) -
      x
        (Fin.cons (α := fun (x : Fin 2) ↦ G) y.1
          (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.1 (finZeroElim (α := fun (i : Fin 0) ↦ G)))) =
    HAdd.hAdd (α := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u))
                (Fin.cons (α := fun (a : Fin 3) ↦ G) y.1
                  (Fin.cons (α := fun (x : Fin 2) ↦ G) y.2.1
                    (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
                  0) :
              (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (x fun (i : Fin 2) ↦
            Fin.cons (α := fun (a : Fin 3) ↦ G) y.1
              (Fin.cons (α := fun (x : Fin 2) ↦ G) y.2.1
                (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
              i.succ) :
        (↑A : Type u))
      (HPow.hPow (α := k) (-1) ((↑0 : ℕ) + 1) •
            x
              (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2)
                (((Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G :
                      G × ((i : Fin 2) → G) ≃ ((i : Fin (HAdd.hAdd (α := ℕ) 2 1)) → G)) :
                    (a : G × ((i : Fin 2) → G)) → (i : Fin 3) → G)
                  (Prod.map id
                    (fun (p : G × G) ↦
                      Fin.cons (α := fun (x : Fin 2) ↦ G) p.1
                        (Fin.cons (α := fun (i : Fin 1) ↦ G) p.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
                    y))) +
          HPow.hPow (α := k) (-1) ((↑1 : ℕ) + 1) •
            x
              (Fin.contractNth 1 (fun (x1 x2 : G) ↦ x1 * x2)
                (((Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G :
                      G × ((i : Fin 2) → G) ≃ ((i : Fin (HAdd.hAdd (α := ℕ) 2 1)) → G)) :
                    (a : G × ((i : Fin 2) → G)) → (i : Fin 3) → G)
                  (Prod.map id
                    (fun (p : G × G) ↦
                      Fin.cons (α := fun (x : Fin 2) ↦ G) p.1
                        (Fin.cons (α := fun (i : Fin 1) ↦ G) p.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
                    y))) +
        HPow.hPow (α := k) (-1) ((↑2 : ℕ) + 1) •
          x
            (Fin.contractNth 2 (fun (x1 x2 : G) ↦ x1 * x2)
              (((Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G :
                    G × ((i : Fin 2) → G) ≃ ((i : Fin (HAdd.hAdd (α := ℕ) 2 1)) → G)) :
                  (a : G × ((i : Fin 2) → G)) → (i : Fin 3) → G)
                (Prod.map id
                  (fun (p : G × G) ↦
                    Fin.cons (α := fun (x : Fin 2) ↦ G) p.1
                      (Fin.cons (α := fun (i : Fin 1) ↦ G) p.2 (finZeroElim (α := fun (i : Fin 0) ↦ G))))
                  y))))

Tactic:
simp only [sub_eq_add_neg, add_assoc, Fin.val_zero, zero_add, pow_one, neg_smul,
    one_smul, Fin.val_one, Fin.val_two, pow_succ' (-1 : k) 2, neg_sq, Nat.one_add, one_pow, mul_one]

Premises used: Fin.val_two, one_pow, neg_smul, add_assoc, sub_eq_add_neg, neg_sq, Fin.val_one, zero_add, one_smul, pow_one, mul_one, OfNat.ofNat, Nat.one_add, Fin.val_zero, pow_succ', Neg.neg