Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: 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) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) 0))
        (x fun i ↦ (Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) i.succ) +
      (-x
            (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
        (x
            (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
          -x
              (Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
                ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)))))

Tactic:
rcongr i <;> fin_cases i

Goal state after:
case e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)

case e_a.e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)

case e_a.e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)