-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem dTwo_comp_eq :
    dTwo A ∘ₗ twoCochainsLequiv A =
      threeCochainsLequiv A ∘ₗ ((inhomogeneousCochains A).d 2 3).hom

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) +
      (-x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) +
        (x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) + -x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)))) =
    (A.ρ (Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) 0))
        (x fun i => Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) i.succ) +
      (-x
            (Fin.contractNth 0 (fun x1 x2 => x1 * x2)
              ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) +
        (x
            (Fin.contractNth 1 (fun x1 x2 => x1 * x2)
              ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) +
          -x
              (Fin.contractNth 2 (fun x1 x2 => x1 * x2)
                ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y)))))

Tactic:
rcongr i <;> fin_cases i <;> rfl

Result:
no goals

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) -
          x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) +
        x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) -
      x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)) =
    (A.ρ (Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) 0))
        (x fun i => Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) i.succ) +
      ((-1) ^ (↑0 + 1) •
            x
              (Fin.contractNth 0 (fun x1 x2 => x1 * x2)
                ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) +
          (-1) ^ (↑1 + 1) •
            x
              (Fin.contractNth 1 (fun x1 x2 => x1 * x2)
                ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) +
        (-1) ^ (↑2 + 1) •
          x
            (Fin.contractNth 2 (fun x1 x2 => x1 * x2)
              ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) 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]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) +
      (-x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) +
        (x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) + -x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)))) =
    (A.ρ (Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) 0))
        (x fun i => Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) i.succ) +
      (-x
            (Fin.contractNth 0 (fun x1 x2 => x1 * x2)
              ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) +
        (x
            (Fin.contractNth 1 (fun x1 x2 => x1 * x2)
              ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) +
          -x
              (Fin.contractNth 2 (fun x1 x2 => x1 * x2)
                ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y)))))

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) -
          x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) +
        x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) -
      x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)) =
    (A.ρ (Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) 0))
        (x fun i => Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) i.succ) +
      ∑ j : Fin 3,
        (-1) ^ (↑j + 1) •
          x
            (j.contractNth (fun x1 x2 => x1 * x2)
              ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y)))

Tactic:
rw [Fin.sum_univ_three]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) -
          x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) +
        x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) -
      x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)) =
    (A.ρ (Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) 0))
        (x fun i => Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) i.succ) +
      ((-1) ^ (↑0 + 1) •
            x
              (Fin.contractNth 0 (fun x1 x2 => x1 * x2)
                ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) +
          (-1) ^ (↑1 + 1) •
            x
              (Fin.contractNth 1 (fun x1 x2 => x1 * x2)
                ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) +
        (-1) ^ (↑2 + 1) •
          x
            (Fin.contractNth 2 (fun x1 x2 => x1 * x2)
              ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))))

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

Tactic:
dsimp

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) -
          x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) +
        x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) -
      x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)) =
    (A.ρ (Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) 0))
        (x fun i => Fin.cons y.1 (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim)) i.succ) +
      ∑ j : Fin 3,
        (-1) ^ (↑j + 1) •
          x
            (j.contractNth (fun x1 x2 => x1 * x2)
              ((Fin.consEquiv fun a => G) (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y)))

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

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 2)
y : G × G × G
⊢ (dTwo A ∘ₗ ↑(twoCochainsLequiv A)) x y =
    (↑(threeCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3)) x y