awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
r : k
x : G × G → (↑A : Type u_1)
g : G × G × G
dsimp :
  HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (r • x (g.2.1, g.2.2)) :
            (↑A : Type u_1))
          (r • x (g.1 * g.2.1, g.2.2)) +
        r • x (g.1, g.2.1 * g.2.2) -
      r • x (g.1, g.2.1) =
    r •
      (HSub.hSub (α := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (x (g.2.1, g.2.2)) :
              (↑A : Type u_1))
            (x (g.1 * g.2.1, g.2.2)) +
          x (g.1, g.2.1 * g.2.2) -
        x (g.1, g.2.1))
⊢ (((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            ((r • x) (g.2.1, g.2.2)) -
          (r • x) (g.1 * g.2.1, g.2.2) +
        (r • x) (g.1, g.2.1 * g.2.2) -
      (r • x) (g.1, g.2.1) =
    HSMul.hSMul (α := k) (β := G × G × G → (↑A : Type u_1)) ((RingHom.id k : (a : k) → k) r : k)
      (fun (g : G × G × G) ↦
        HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (x (g.2.1, g.2.2)) :
                (↑A : Type u_1))
              (x (g.1 * g.2.1, g.2.2)) +
            x (g.1, g.2.1 * g.2.2) -
          x (g.1, g.2.1))
      g

Tactic:
dsimp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
r : k
x : G × G → (↑A : Type u_1)
g : G × G × G
⊢ HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (r • x (g.2.1, g.2.2)) :
            (↑A : Type u_1))
          (r • x (g.1 * g.2.1, g.2.2)) +
        r • x (g.1, g.2.1 * g.2.2) -
      r • x (g.1, g.2.1) =
    r •
      (HSub.hSub (α := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (x (g.2.1, g.2.2)) :
              (↑A : Type u_1))
            (x (g.1 * g.2.1, g.2.2)) +
          x (g.1, g.2.1 * g.2.2) -
        x (g.1, g.2.1))

Tactic:
simp only [map_smul, smul_add, smul_sub]

Premises used: smul_sub, smul_add, map_smul
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
hf :
  ∀ (x : Fin 0 → G) (a : (↑A : Type u)) (y : G),
    Eq (α := (↑A : Type u))
      ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ d₀₁ A) ∘ₗ LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) x :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u))
          a y :
        (↑A : Type u))
      ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1 ≫ (cochainsIso₁ A).hom) ∘ₗ
              LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) x :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u))
          a y :
        (↑A : Type u))
⊢ (cochainsIso₀ A).hom ≫ d₀₁ A = (inhomogeneousCochains A).d 0 1 ≫ (cochainsIso₁ A).hom

Tactic:
ext x a y
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (cochainsIso₀ A).inv ≫ (inhomogeneousCochains A).d 0 1 = d₀₁ A ≫ (cochainsIso₁ A).inv

Tactic:
(CommSq.horiz_inv ⟨comp_d₀₁_eq A⟩).w

Premises used: groupCohomology.comp_d₀₁_eq, CategoryTheory.CommSq.horiz_inv, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
hf :
  ∀ (x : (↑((inhomogeneousCochains A).X 1) : Type u)) (y : G × G),
    Eq (α := (↑A : Type u))
      ((ModuleCat.Hom.hom ((cochainsIso₁ A).hom ≫ d₁₂ A) :
            (a : (↑((inhomogeneousCochains A).X 1) : Type u)) → (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u))
          x y :
        (↑A : Type u))
      ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2 ≫ (cochainsIso₂ A).hom) :
            (a : (↑((inhomogeneousCochains A).X 1) : Type u)) → (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u))
          x y :
        (↑A : Type u))
⊢ (cochainsIso₁ A).hom ≫ d₁₂ A = (inhomogeneousCochains A).d 1 2 ≫ (cochainsIso₂ A).hom

Tactic:
ext x y
-- 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 1) : Type u)
y : G × G
hf :
  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 ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.2)) :
          (↑A : Type u))
        (x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) (y.1 * y.2))) +
      x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.1) =
    HAdd.hAdd (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u))
                (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                    (a : G × G) → (i : Fin 2) → G)
                  y 0) :
              (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (x fun (i : Fin 1) ↦
            ((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              y i.succ) :
        (↑A : Type u))
      (∑ j : Fin (1 + 1),
          HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) •
            x
              (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2)
                (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                    (a : G × G) → (i : Fin 2) → G)
                  y)) :
        (↑A : Type u))
⊢ Eq (α := (↑A : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₁ A).hom ≫ d₁₂ A) :
          (a : (↑((inhomogeneousCochains A).X 1) : Type u)) → (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u))
        x y :
      (↑A : Type u))
    ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2 ≫ (cochainsIso₂ A).hom) :
          (a : (↑((inhomogeneousCochains A).X 1) : Type u)) → (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u))
        x y :
      (↑A : Type u))

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

Premises used: Prod.fst, Rep.ρ, DFunLike.coe
-- 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 1) : Type u)
y : G × G
hf :
  ∀ (i : Fin 1),
    Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.2 i : G)
      (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G) y
          i.succ :
        G)
hf₁ :
  ∀ (i : Fin 1),
    Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) (y.1 * y.2) i : G)
      (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2)
          (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
              (a : G × G) → (i : Fin 2) → G)
            y)
          i :
        G)
hf₂ :
  ∀ (i : Fin 1),
    Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.1 i : G)
      (Fin.contractNth 1 (fun (x1 x2 : G) ↦ x1 * x2)
          (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
              (a : G × G) → (i : Fin 2) → G)
            y)
          i :
        G)
⊢ 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 ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.2)) :
        (↑A : Type u))
      (-x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) (y.1 * y.2)) +
        x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.1)) =
    HAdd.hAdd (α := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u))
                (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                    (a : G × G) → (i : Fin 2) → G)
                  y 0) :
              (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (x fun (i : Fin 1) ↦
            ((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              y i.succ) :
        (↑A : Type u))
      (-x
            (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2)
              (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                  (a : G × G) → (i : Fin 2) → G)
                y)) +
        x
          (Fin.contractNth 1 (fun (x1 x2 : G) ↦ x1 * x2)
            (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              y)))

Tactic:
rcongr i
-- 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 1) : Type u)
y : G × G
i : Fin 1
hf :
  Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.2 0 : G)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G) y
        (Fin.succ 0) :
      G)
⊢ Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.2 i : G)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G) y
        i.succ :
      G)

Tactic:
rw [Subsingleton.elim i 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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 1) : Type u)
y : G × G
i : Fin 1
hf :
  Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) (y.1 * y.2) 0 : G)
    (Fin.contractNth (n := 1) 0 (fun (x1 x2 : G) ↦ x1 * x2)
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          y)
        0 :
      G)
⊢ Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) (y.1 * y.2) i : G)
    (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2)
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          y)
        i :
      G)

Tactic:
rw [Subsingleton.elim i 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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 1) : Type u)
y : G × G
i : Fin 1
hf :
  Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.1 0 : G)
    (Fin.contractNth (n := 1) 1 (fun (x1 x2 : G) ↦ x1 * x2)
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          y)
        0 :
      G)
⊢ Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.1 i : G)
    (Fin.contractNth 1 (fun (x1 x2 : G) ↦ x1 * x2)
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          y)
        i :
      G)

Tactic:
rw [Subsingleton.elim i 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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 1) : Type u)
y : G × G
i : Fin 1
⊢ Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.2 0 : G)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G) y
        (Fin.succ 0) :
      G)

Tactic:
rfl
-- 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 1) : Type u)
y : G × G
i : Fin 1
⊢ Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) (y.1 * y.2) 0 : G)
    (Fin.contractNth (n := 1) 0 (fun (x1 x2 : G) ↦ x1 * x2)
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          y)
        0 :
      G)

Tactic:
rfl
-- 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 1) : Type u)
y : G × G
i : Fin 1
⊢ Eq (α := G) ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.1 0 : G)
    (Fin.contractNth (n := 1) 1 (fun (x1 x2 : G) ↦ x1 * x2)
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          y)
        0 :
      G)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (cochainsIso₁ A).inv ≫ (inhomogeneousCochains A).d 1 2 = d₁₂ A ≫ (cochainsIso₂ A).inv

Tactic:
(CommSq.horiz_inv ⟨comp_d₁₂_eq A⟩).w

Premises used: groupCohomology.comp_d₁₂_eq, CategoryTheory.CommSq.horiz_inv, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
hf :
  ∀ (x : (↑((inhomogeneousCochains A).X 2) : Type u)) (y : G × G × G),
    Eq (α := (↑A : Type u))
      ((ModuleCat.Hom.hom ((cochainsIso₂ A).hom ≫ d₂₃ A) :
            (a : (↑((inhomogeneousCochains A).X 2) : Type u)) →
              (↑(ModuleCat.of k (G × G × G → (↑A : Type u))) : Type u))
          x y :
        (↑A : Type u))
      ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3 ≫ (cochainsIso₃ A).hom) :
            (a : (↑((inhomogeneousCochains A).X 2) : Type u)) →
              (↑(ModuleCat.of k (G × G × G → (↑A : Type u))) : Type u))
          x y :
        (↑A : Type u))
⊢ (cochainsIso₂ A).hom ≫ d₂₃ A = (inhomogeneousCochains A).d 2 3 ≫ (cochainsIso₃ A).hom

Tactic:
ext x y
-- 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 :
  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
                (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                    (a : G × G) → (i : Fin 2) → G)
                  (y.2.1, y.2.2))) :
            (↑A : Type u))
          (x
            (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              (y.1 * y.2.1, y.2.2))) +
        x
          (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
              (a : G × G) → (i : Fin 2) → G)
            (y.1, y.2.1 * y.2.2)) -
      x
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          (y.1, y.2.1)) =
    HAdd.hAdd (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u))
                ((Equiv.symm
                      (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                        ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
                    (a : G × G × G) → (i : Fin (2 + 1)) → G)
                  y 0) :
              (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (x fun (i : Fin 2) ↦
            (Equiv.symm
                  (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                    ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
                (a : G × G × G) → (i : Fin (2 + 1)) → G)
              y i.succ) :
        (↑A : Type u))
      (∑ j : Fin (2 + 1),
          HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) •
            x
              (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2)
                ((Equiv.symm
                      (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                        ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
                    (a : G × G × G) → (i : Fin (2 + 1)) → G)
                  y)) :
        (↑A : Type u))
⊢ Eq (α := (↑A : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₂ A).hom ≫ d₂₃ A) :
          (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G × G → (↑A : Type u))) : Type u))
        x y :
      (↑A : Type u))
    ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3 ≫ (cochainsIso₃ A).hom) :
          (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G × G → (↑A : Type u))) : Type u))
        x y :
      (↑A : Type u))

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

Premises used: Prod.fst, Rep.ρ, DFunLike.coe
-- 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
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
hf :
  Eq.{u + 1} (α := G)
    (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)))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      G)
    (Fin.contractNth (n := 2) 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))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      G)
hf₁ :
  Eq.{u + 1} (α := G)
    (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)))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      G)
    (Fin.contractNth (n := 2) 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))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      G)
⊢ Eq.{u + 1} (α := G)
    (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))) i :
      G)
    (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))
      i)

Tactic:
fin_cases i
-- 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
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
hf :
  Eq.{u + 1} (α := G)
    (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)))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      G)
    (Fin.contractNth (n := 2) 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))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      G)
hf₁ :
  Eq.{u + 1} (α := G)
    (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)))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      G)
    (Fin.contractNth (n := 2) 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))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      G)
⊢ Eq.{u + 1} (α := G)
    (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))) i :
      G)
    (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))
      i)

Tactic:
fin_cases i