-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem dOne_comp_eq : dOne A ∘ₗ oneCochainsLequiv A =
    twoCochainsLequiv A ∘ₗ ((inhomogeneousCochains A).d 1 2).hom

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) +
      (-x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) + x ((Equiv.funUnique (Fin 1) G).symm y.1)) =
    (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) +
      (-x (Fin.contractNth 0 (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y)) +
        x (Fin.contractNth 1 (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y)))

Tactic:
rcongr i <;> rw [Subsingleton.elim i 0] <;> rfl

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ dOne A ∘ₗ ↑(oneCochainsLequiv A) = ↑(twoCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2)

Tactic:
ext x y

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (dOne A ∘ₗ ↑(oneCochainsLequiv A)) x y =
    (↑(twoCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2)) x y

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (dOne A ∘ₗ ↑(oneCochainsLequiv A)) x y =
    (↑(twoCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2)) x y

Tactic:
show A.ρ y.1 (x _) - x _ + x _ =  _ + _

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) +
      x ((Equiv.funUnique (Fin 1) G).symm y.1) =
    (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) +
      ∑ j : Fin (1 + 1), (-1) ^ (↑j + 1) • x (j.contractNth (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y))

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) +
      x ((Equiv.funUnique (Fin 1) G).symm y.1) =
    (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) +
      ∑ j : Fin (1 + 1), (-1) ^ (↑j + 1) • x (j.contractNth (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y))

Tactic:
rw [Fin.sum_univ_two]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) +
      x ((Equiv.funUnique (Fin 1) G).symm y.1) =
    (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) +
      ((-1) ^ (↑0 + 1) • x (Fin.contractNth 0 (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y)) +
        (-1) ^ (↑1 + 1) • x (Fin.contractNth 1 (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y)))

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) +
      x ((Equiv.funUnique (Fin 1) G).symm y.1) =
    (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) +
      ((-1) ^ (↑0 + 1) • x (Fin.contractNth 0 (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y)) +
        (-1) ^ (↑1 + 1) • x (Fin.contractNth 1 (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y)))

Tactic:
simp only [Fin.val_zero, zero_add, pow_one, neg_smul, one_smul, Fin.val_one,
  Nat.one_add, neg_one_sq, sub_eq_add_neg, add_assoc]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) +
      (-x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) + x ((Equiv.funUnique (Fin 1) G).symm y.1)) =
    (A.ρ ((piFinTwoEquiv fun x => G).symm y 0)) (x fun i => (piFinTwoEquiv fun x => G).symm y i.succ) +
      (-x (Fin.contractNth 0 (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y)) +
        x (Fin.contractNth 1 (fun x1 x2 => x1 * x2) ((piFinTwoEquiv fun x => G).symm y)))