Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: 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, ⋯⟩)

pp: 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, ⋯⟩)

pp: 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, ⋯⟩)

pp: 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, ⋯⟩)

pp: 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, ⋯⟩)

pp: 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, ⋯⟩)

Tactic:
<;>

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, ⋯⟩)