awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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
⊢ 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))
have 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))
Tactic: change A.ρ y.1 (x _) - x _ + x _ - x _ = _ + _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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)
⊢ 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)
have 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, sorry⟩) :
    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, sorry⟩) :
    G)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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)
⊢ 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)
have 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, sorry⟩) :
    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, sorry⟩) :
    G)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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)
⊢ 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)
have 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, sorry⟩) :
    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, sorry⟩) :
    G)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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)
⊢ 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)
have 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, sorry⟩) :
    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, sorry⟩) :
    G)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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)
⊢ Eq.{u + 1} (α := G)
    (Fin.cons (α := fun (x : Fin 2) ↦ G) y.1
        (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.1 (finZeroElim (α := fun (i : Fin 0) ↦ G))) i :
      G)
    (Fin.contractNth 2 (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)
have hf : Eq.{u + 1} (α := G)
  (Fin.cons (α := fun (x : Fin 2) ↦ G) y.1
      (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.1 (finZeroElim (α := fun (i : Fin 0) ↦ G)))
      ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, sorry⟩) :
    G)
  (Fin.contractNth (n := 2) 2 (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, sorry⟩) :
    G)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
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 (finZeroElim (α := fun (i : Fin 0) ↦ G)))
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      G)
    (Fin.contractNth (n := 2) 2 (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)
⊢ Eq.{u + 1} (α := G)
    (Fin.cons (α := fun (x : Fin 2) ↦ G) y.1
        (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.1 (finZeroElim (α := fun (i : Fin 0) ↦ G))) i :
      G)
    (Fin.contractNth 2 (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)
have hf₁ : Eq.{u + 1} (α := G)
  (Fin.cons (α := fun (x : Fin 2) ↦ G) y.1
      (Fin.cons (α := fun (i : Fin 1) ↦ G) y.2.1 (finZeroElim (α := fun (i : Fin 0) ↦ G)))
      ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, sorry⟩) :
    G)
  (Fin.contractNth (n := 2) 2 (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, sorry⟩) :
    G)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ d₀₁.{u, u_1} A ≫ d₁₂ A = 0
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) (x_1 : G × G),
  Eq (α := (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A ≫ d₁₂ A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
⊢ d₁₂ A ≫ d₂₃ A = 0
have hf : ∀ (f : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) (g : G × G × G),
  Eq.{u_1 + 1} (α := (↑A : Type u_1))
    ((ModuleCat.Hom.hom (d₁₂ A ≫ d₂₃ A) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
        f g :
      (↑A : Type u_1))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
        f g :
      (↑A : Type u_1))
Tactic: ext f g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))
g : G × G × G
⊢ Eq.{u_1 + 1} (α := (↑A : Type u_1))
    ((ModuleCat.Hom.hom (d₁₂ A ≫ d₂₃ A) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
        f g :
      (↑A : Type u_1))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
        f g :
      (↑A : Type u_1))
have hf : HAdd.hAdd (β := (↑A : Type u_1))
          (HSub.hSub (α := (↑A : Type u_1)) (β := (↑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))
                ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.2.1 :
                        (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                      (a : (↑A : Type u_1)) → (↑A : Type u_1))
                    (f g.2.2) :
                  (↑A : Type u_1)) :
              (↑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))
                (f (g.2.1 * g.2.2)) :
              (↑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))
              (f g.2.1) :
            (↑A : Type u_1)) -
        (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))
                ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.2.1 :
                        (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                      (a : (↑A : Type u_1)) → (↑A : Type u_1))
                    (f g.2.2) :
                  (↑A : Type u_1)) :
              (↑A : Type u_1))
            (f (g.1 * (g.2.1 * g.2.2))) +
          f (g.1 * g.2.1)) +
      (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))
              (f (g.2.1 * g.2.2)) :
            (↑A : Type u_1))
          (f (g.1 * (g.2.1 * g.2.2))) +
        f g.1) -
    (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))
            (f g.2.1) :
          (↑A : Type u_1))
        (f (g.1 * g.2.1)) +
      f g.1) =
  0
Tactic: simp [mul_assoc, Pi.zero_apply (M := fun _ => A)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : G → (↑A : Type u_1)
⊢ Eq (α := (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))
      ((ModuleCat.Hom.hom (d₁₂ A) :
            (a : G → (↑A : Type u_1)) → (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))
          f :
        (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))
      (0 : (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1))) ↔
    ∀ (g h : G),
      HSub.hSub (α := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f h) :
              (↑A : Type u_1))
            (f (g * h)) +
          f g =
        0
have simp_rw : (∀ (a b : G),
    HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) a : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f b) :
            (↑A : Type u_1))
          (f (a * b)) +
        f a =
      0 (a, b)) ↔
  ∀ (g h : G),
    HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f h) :
            (↑A : Type u_1))
          (f (g * h)) +
        f g =
      0
Tactic: simp_rw [funext_iff, d₁₂_hom_apply, Prod.forall]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : G → (↑A : Type u_1)
⊢ f ∈ cocycles₁ A ↔
    ∀ (g h : G),
      f (g * h) =
        HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f h) :
            (↑A : Type u_1))
          (f g)
have simp_rw : (∀ (g h : G),
    HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f h) :
            (↑A : Type u_1))
          (f (g * h)) +
        f g =
      0) ↔
  ∀ (g h : G),
    f (g * h) =
      HAdd.hAdd (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (f h) :
          (↑A : Type u_1))
        (f g)
Tactic: simp_rw [mem_cocycles₁_def, sub_add_eq_add_sub, sub_eq_zero, eq_comm]