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
⊢ (cochainsIso₀ A).hom ≫ d₀₁ A = (inhomogeneousCochains A).d 0 1 ≫ (cochainsIso₁ A).hom
have 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))
Tactic: ext x a y
-- 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 : 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))
have hf : HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
    ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
      (↑A : Type u))
    (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) =
  HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
    ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a fun (i : Fin 0) ↦ y : (↑A : Type u)) :
      (↑A : Type u))
    (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a
        (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2) (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
      (↑A : Type u))
Tactic: simp only [cochainsIso₀, LinearEquiv.toModuleIso_hom, ModuleCat.hom_comp,
    ConcreteCategory.hom_ofHom, LinearMap.coe_comp, LinearEquiv.coe_coe,
    LinearEquiv.funUnique_apply, LinearMap.coe_single, Function.comp_apply, Function.eval,
    d₀₁_hom_apply, zero_add, ↓reduceDIte, Nat.reduceAdd, eqToHom_refl, Category.comp_id,
    cochainsIso₁, Iso.symm_hom, LinearEquiv.toModuleIso_inv, LinearEquiv.funCongrLeft_symm,
    LinearEquiv.funCongrLeft_apply, Equiv.funUnique_symm_apply, LinearMap.funLeft_apply,
    inhomogeneousCochains.d_hom_apply, Fin.isValue, uniqueElim_const, Finset.univ_unique,
    Fin.default_eq_zero, Fin.val_eq_zero, pow_one, neg_smul, one_smul, Finset.sum_neg_distrib,
    Finset.sum_singleton, ← sub_eq_add_neg, CochainComplex.of.d]
-- 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 : Fin 0 → G
a : (↑A : Type u)
y : G
⊢ HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) =
    HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a fun (i : Fin 0) ↦ y : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a
          (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2) (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
        (↑A : Type u))
have hf : HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
    ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
      (↑A : Type u))
    (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) =
  HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
    ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
      (↑A : Type u))
    (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a
        (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2) (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
      (↑A : Type u))
Tactic: rw [← Subsingleton.elim (α := Fin 0 → G) default (fun i ↦ y), Subsingleton.elim
    (Fin.contractNth 0 _) default, Pi.default_def]
-- 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 : Fin 0 → G
a : (↑A : Type u)
y : G
hf :
  HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) =
    HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a
          (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2) (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
        (↑A : Type u))
⊢ HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) =
    HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a fun (i : Fin 0) ↦ y : (↑A : Type u)) :
        (↑A : Type u))
      (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a
          (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2) (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
        (↑A : Type u))
have hf₁ : HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
    ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
      (↑A : Type u))
    (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) =
  HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
    ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a default : (↑A : Type u)) :
      (↑A : Type u))
    (Pi.single (M := fun (i : Fin 0 → G) ↦ (↑A : Type u)) x a (default (uniqueElim (α := fun (a : Fin 1) ↦ G) y)) :
      (↑A : Type u))
Tactic: rw [← Subsingleton.elim (α := Fin 0 → G) default (fun i ↦ y), Subsingleton.elim
    (Fin.contractNth 0 _) default, Pi.default_def]
-- 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
⊢ (cochainsIso₁ A).hom ≫ d₁₂ A = (inhomogeneousCochains A).d 1 2 ≫ (cochainsIso₂ A).hom
have 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))
Tactic: ext x y
-- 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 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))
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 (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))
Tactic: change A.ρ y.1 (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 1) : Type u)
y : G × 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)))
have 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)
Tactic: rcongr 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 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)
⊢ 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)))
have 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)
Tactic: rcongr 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 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)
⊢ 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)))
have 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)
Tactic: rcongr 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 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 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)
have 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)
Tactic: rw [Subsingleton.elim i 0]
-- 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 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) 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)
have 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)
Tactic: rw [Subsingleton.elim i 0]
-- 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 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 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)
have 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)
Tactic: rw [Subsingleton.elim i 0]
-- 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
⊢ (cochainsIso₂ A).hom ≫ d₂₃ A = (inhomogeneousCochains A).d 2 3 ≫ (cochainsIso₃ A).hom
have 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))
Tactic: ext x y