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 : (↑A : Type (max u u_1))
hx :
  Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u)))
            (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        x :
      (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
g : G
⊢ (((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
          (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
        (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
      x =
    x
have rw : HSub.hSub (α := (↑A : Type (max u u_1)))
    ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
            (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
          (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
        x :
      (↑A : Type (max u u_1)))
    x =
  0
Tactic: rw [← sub_eq_zero]
-- 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
⊢ (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f = iCocycles A 0 ≫ (cochainsIso₀ A).hom
have dsimp : (KernelFork.ofι (HomologicalComplex.iCycles (inhomogeneousCochains A) 0) sorry).mapOfIsLimit sorry.fIsKernel
      (dArrowIso₀₁ A).hom ≫
    (shortComplexH0 A).f =
  iCocycles A 0 ≫ (cochainsIso₀ A).hom
Tactic: dsimp [cocyclesIso₀]
-- 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
⊢ (cocyclesIso₀ A).inv ≫ iCocycles A 0 = (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
have rw : iCocycles A 0 = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, cocyclesIso₀_hom_comp_f]
-- 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
rw : iCocycles A 0 = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
⊢ (cocyclesIso₀ A).inv ≫ iCocycles A 0 = (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
have rw₁ : iCocycles A 0 = ((cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f) ≫ (cochainsIso₀ A).inv
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, cocyclesIso₀_hom_comp_f]
-- 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
rw : iCocycles A 0 = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
rw₁ : iCocycles A 0 = ((cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f) ≫ (cochainsIso₀ A).inv
⊢ (cocyclesIso₀ A).inv ≫ iCocycles A 0 = (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
have rw₂ : iCocycles A 0 ≫ (cochainsIso₀ A).hom = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, cocyclesIso₀_hom_comp_f]
-- 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
rw : iCocycles A 0 = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
rw₁ : iCocycles A 0 = ((cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f) ≫ (cochainsIso₀ A).inv
rw₂ : iCocycles A 0 ≫ (cochainsIso₀ A).hom = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f
⊢ (cocyclesIso₀ A).inv ≫ iCocycles A 0 = (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
have rw₃ : iCocycles A 0 ≫ (cochainsIso₀ A).hom = iCocycles A 0 ≫ (cochainsIso₀ A).hom
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, cocyclesIso₀_hom_comp_f]
-- 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 : ↥A.ρ.invariants
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 0 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 0) :
          (a : (↑(ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (0 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ A).inv :
              (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
            (↑x : (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 0) : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 0 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 0 1) → G) → (↑A : Type u))) : Type u))
have h : ∀ (g : Fin (HAdd.hAdd (α := ℕ) 0 1) → G),
  Eq (α := (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 0) :
          (a : (↑(ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (0 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ A).inv :
              (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
            (↑x : (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 0) : Type u))
        g :
      (↑A : Type u))
    (0 g : (↑A : Type u))
Tactic: ext 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 k G
x : ↥A.ρ.invariants
⊢ Eq (α := (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 0) (iCocycles A 0) :
          (a : (↑(cocycles A 0) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        (cocyclesMk
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ A).inv :
              (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
            (↑x : (↑A : Type u)))
          ⋯) :
      (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 0) (iCocycles A 0) :
          (a : (↑(cocycles A 0) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cocyclesIso₀ A).inv :
              (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type u)) → (↑(cocycles A 0) : Type u))
            x :
          (↑(cocycles A 0) : Type u)) :
      (↑((inhomogeneousCochains A).X 0) : Type u))
have rw : Eq (α := (↑((inhomogeneousCochains A).X 0) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (cochainsIso₀ A).inv :
        (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
      (↑x : (↑A : Type u)) :
    (↑((inhomogeneousCochains A).X 0) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := cocycles A 0) (iCocycles A 0) :
        (a : (↑(cocycles A 0) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cocyclesIso₀ A).inv :
            (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type u)) → (↑(cocycles A 0) : Type u))
          x :
        (↑(cocycles A 0) : Type u)) :
    (↑((inhomogeneousCochains A).X 0) : Type u))
Tactic: rw [iCocycles_mk]
-- 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 : ↥(cocycles₁ A)
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 1) :
          (a : (↑(ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₁ A).inv :
              (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
            (⇑x : (a : G) → (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 1) : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
have rw : Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 1) ∘ₗ
          ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₁ A).inv :
        (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
      (⇑x : (a : G) → (↑A : Type u)) :
    (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
  (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← inhomogeneousCochains.d_def,
        eq_d₁₂_comp_inv, ModuleCat.hom_comp, LinearMap.comp_apply, cocycles₁.d₁₂_apply x,
        map_zero]
-- 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 : ↥(cocycles₁ A)
rw :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 1) ∘ₗ
            ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cochainsIso₁ A).inv :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 1) :
          (a : (↑(ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₁ A).inv :
              (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
            (⇑x : (a : G) → (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 1) : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
have rw₁ : Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
  ((ModuleCat.Hom.hom ((cochainsIso₁ A).inv ≫ inhomogeneousCochains.d A 1) :
        (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
      (⇑x : (a : G) → (↑A : Type u)) :
    (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
  (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← inhomogeneousCochains.d_def,
        eq_d₁₂_comp_inv, ModuleCat.hom_comp, LinearMap.comp_apply, cocycles₁.d₁₂_apply x,
        map_zero]
-- 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 : ↥(cocycles₁ A)
this :
  Eq (α := (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv) :
          (a : ↥(cocycles₁ A)) → (Fin 1 → G) → (↑A : Type u))
        x :
      (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 1) (iCocycles A 1) :
          (a : (↑(cocycles A 1) : Type u)) → (Fin 1 → G) → (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (isoCocycles₁ A).inv :
              (a : ↥(cocycles₁ A)) → (↑(cocycles A 1) : Type u))
            x :
          (↑(cocycles A 1) : Type u)) :
      (Fin 1 → G) → (↑A : Type u))
⊢ Eq (α := (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₁ A).inv :
          (a : G → (↑A : Type u)) → (Fin 1 → G) → (↑A : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (Fin 1 → G) → (↑A : Type u))
    ((ModuleCat.Hom.hom (HomologicalComplex.iCycles (inhomogeneousCochains A) 1) :
          (a : (↑(HomologicalComplex.cycles (inhomogeneousCochains A) 1) : Type u)) → (Fin 1 → G) → (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (isoCocycles₁ A).inv :
              (a : ↥(cocycles₁ A)) → (↑(cocycles A 1) : Type u))
            x :
          (↑(cocycles A 1) : Type u)) :
      (Fin 1 → G) → (↑A : Type u))
have rw : Eq (α := (Fin 1 → G) → (↑A : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (cochainsIso₁ A).inv :
        (a : G → (↑A : Type u)) → (Fin 1 → G) → (↑A : Type u))
      (⇑x : (a : G) → (↑A : Type u)) :
    (Fin 1 → G) → (↑A : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv) :
        (a : ↥(cocycles₁ A)) → (Fin 1 → G) → (↑A : Type u))
      x :
    (Fin 1 → G) → (↑A : Type u))
Tactic: rw [← this]
-- 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 : ↥(cocycles₂ A)
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 2 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 2) :
          (a : (↑(ModuleCat.of k ((Fin 2 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (2 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₂ A).inv :
              (a : (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u)) → (↑((inhomogeneousCochains A).X 2) : Type u))
            (⇑x : (a : G × G) → (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 2) : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
have rw : Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 2 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 2) ∘ₗ
          ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₂ A).inv :
        (a : (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k ((Fin (2 + 1) → G) → (↑A : Type u))) : Type u))
      (⇑x : (a : G × G) → (↑A : Type u)) :
    (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
  (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← inhomogeneousCochains.d_def,
        eq_d₂₃_comp_inv, ModuleCat.hom_comp, LinearMap.comp_apply, cocycles₂.d₂₃_apply x,
        map_zero]
-- 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 : ↥(cocycles₂ A)
rw :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ((Fin 2 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 2) ∘ₗ
            ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cochainsIso₂ A).inv :
          (a : (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (2 + 1) → G) → (↑A : Type u))) : Type u))
        (⇑x : (a : G × G) → (↑A : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 2 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 2) :
          (a : (↑(ModuleCat.of k ((Fin 2 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (2 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₂ A).inv :
              (a : (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u)) → (↑((inhomogeneousCochains A).X 2) : Type u))
            (⇑x : (a : G × G) → (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 2) : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
have rw₁ : Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
  ((ModuleCat.Hom.hom ((cochainsIso₂ A).inv ≫ inhomogeneousCochains.d A 2) :
        (a : (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k ((Fin (2 + 1) → G) → (↑A : Type u))) : Type u))
      (⇑x : (a : G × G) → (↑A : Type u)) :
    (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
  (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 2 1) → G) → (↑A : Type u))) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← inhomogeneousCochains.d_def,
        eq_d₂₃_comp_inv, ModuleCat.hom_comp, LinearMap.comp_apply, cocycles₂.d₂₃_apply x,
        map_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ Eq (α := (↑(H1 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1π A) :
            (a : (↑(ModuleCat.of k ↥(cocycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          x :
        (↑(H1 A) : Type u))
      (0 : (↑(H1 A) : Type u)) ↔
    (⇑x : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A
have h : Eq (α := (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 1).homology)
  ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
    leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
      Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
  (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
      (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
    (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData.π ≫
      Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
Tactic: have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv
    (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousCochains A).sc 1).leftHomologyIso.hom