awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type u)
rw :
  Eq (α := (↑((inhomogeneousChains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₀ A).inv :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        x :
      (↑((inhomogeneousChains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 0) (iCycles A 0) :
          (a : (↑(cycles A 0) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cyclesIso₀ A).inv :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(cycles A 0) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 0) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 0) (iCycles A 0) :
          (a : (↑(cycles A 0) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        (cyclesMk 0 0 cyclesMk₀_eq._proof_1
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (chainsIso₀ A).inv :
              (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
            x)
          ⋯) :
      (↑((inhomogeneousChains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 0) (iCycles A 0) :
          (a : (↑(cycles A 0) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cyclesIso₀ A).inv :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(cycles A 0) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 0) : Type u))

Tactic:
rw [iCycles_mk]

Premises used: groupHomology.iCycles_mk
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type u)
⊢ Eq (α := (↑((inhomogeneousChains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₀ A).inv :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        x :
      (↑((inhomogeneousChains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 0) (iCycles A 0) :
          (a : (↑(cycles A 0) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cyclesIso₀ A).inv :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(cycles A 0) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 0) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).prev 1 = 2

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).next 1 = 0

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (isoCycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.i = iCycles A 1 ≫ (chainsIso₁ A).hom

Tactic:
simp [isoCycles₁, iCycles, HomologicalComplex.iCycles, ShortComplex.iCycles]

Premises used: groupHomology.isoCycles₁, HomologicalComplex.iCycles, groupHomology.iCycles, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (isoCycles₁ A).inv ≫ iCycles A 1 = (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (chainsIso₁ A).inv

Tactic:
(CommSq.horiz_inv ⟨isoCycles₁_hom_comp_i A⟩).w

Premises used: Set.Mem, CategoryTheory.CommSq.horiz_inv, CategoryTheory.CommSq.mk, groupHomology.cycles₁, CategoryTheory.CommSq.w, groupHomology.isoCycles₁_hom_comp_i
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ toCycles A 2 1 ≫ (isoCycles₁ A).hom = (chainsIso₂ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.f'

Tactic:
simp [← cancel_mono (shortComplexH1 A).moduleCatLeftHomologyData.i, comp_d₂₁_eq,
    shortComplexH1_f]

Premises used: groupHomology.shortComplexH1_f, groupHomology.comp_d₂₁_eq, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, groupHomology.shortComplexH1, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ComplexShape.down ℕ).next 1 = 0

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
rw :
  Eq (α := (↑((inhomogeneousChains A).X 0) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A ≫ (chainsIso₀ A).inv) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        (↑x : G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 0) : Type u))
    (0 : (↑((inhomogeneousChains A).X 0) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousChains A).X 1) (Y := (inhomogeneousChains A).X 0)
            ((inhomogeneousChains A).d 1 0) :
          (a : (↑((inhomogeneousChains A).X 1) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chainsIso₁ A).inv :
            (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
          (↑x : G →₀ (↑A : Type u))) :
      (↑((inhomogeneousChains A).X 0) : Type u))
    (0 : (↑((inhomogeneousChains A).X 0) : Type u))

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]

Premises used: LinearMap.comp_apply, groupHomology.eq_d₁₀_comp_inv, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ Eq (α := (↑((inhomogeneousChains A).X 0) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A ≫ (chainsIso₀ A).inv) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
        (↑x : G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 0) : Type u))
    (0 : (↑((inhomogeneousChains A).X 0) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
rw :
  Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₁ A).inv :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        (↑x : G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 1) (iCycles A 1) :
          (a : (↑(cycles A 1) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₁ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(cycles A 1) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 1) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 1) (iCycles A 1) :
          (a : (↑(cycles A 1) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        (cyclesMk 1 0 cyclesMk₁_eq._proof_1
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (chainsIso₁ A).inv :
              (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
            (↑x : G →₀ (↑A : Type u)))
          ⋯) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 1) (iCycles A 1) :
          (a : (↑(cycles A 1) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₁ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(cycles A 1) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 1) : Type u))

Tactic:
rw [iCycles_mk]

Premises used: groupHomology.iCycles_mk
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
simp :
  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) (chainsIso₁ A).inv :
          (a : G →₀ (↑A : Type u)) → (Fin 1 → G) →₀ (↑A : Type u))
        (↑x : 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 ≫ (chainsIso₁ A).inv) :
          (a : ↥(cycles₁ A)) → (Fin 1 → G) →₀ (↑A : Type u))
        x :
      (Fin 1 → G) →₀ (↑A : Type u))
⊢ Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₁ A).inv :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        (↑x : G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 1) (iCycles A 1) :
          (a : (↑(cycles A 1) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₁ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(cycles A 1) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 1) : Type u))

Tactic:
simp only [ChainComplex.of_X, isoCycles₁_inv_comp_iCycles_apply]

Premises used: groupHomology.isoCycles₁_inv_comp_iCycles_apply, ChainComplex.of_X
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ 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) (chainsIso₁ A).inv :
          (a : G →₀ (↑A : Type u)) → (Fin 1 → G) →₀ (↑A : Type u))
        (↑x : 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 ≫ (chainsIso₁ A).inv) :
          (a : ↥(cycles₁ A)) → (Fin 1 → G) →₀ (↑A : Type u))
        x :
      (Fin 1 → G) →₀ (↑A : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).prev 2 = 3

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ComplexShape.down ℕ).next 2 = 1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (isoCycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.i = iCycles A 2 ≫ (chainsIso₂ A).hom

Tactic:
simp [isoCycles₂, iCycles, HomologicalComplex.iCycles, ShortComplex.iCycles]

Premises used: HomologicalComplex.iCycles, groupHomology.iCycles, groupHomology.isoCycles₂, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (isoCycles₂ A).inv ≫ iCycles A 2 = (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (chainsIso₂ A).inv

Tactic:
(CommSq.horiz_inv ⟨isoCycles₂_hom_comp_i A⟩).w

Premises used: Set.Mem, CategoryTheory.CommSq.horiz_inv, CategoryTheory.CommSq.mk, groupHomology.cycles₂, CategoryTheory.CommSq.w, groupHomology.isoCycles₂_hom_comp_i
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ toCycles A 3 2 ≫ (isoCycles₂ A).hom = (chainsIso₃ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.f'

Tactic:
simp [← cancel_mono (shortComplexH2 A).moduleCatLeftHomologyData.i, comp_d₃₂_eq,
    shortComplexH2_f]

Premises used: groupHomology.shortComplexH2_f, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, groupHomology.shortComplexH2, CategoryTheory.ShortComplex.LeftHomologyData.i, groupHomology.comp_d₃₂_eq
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ (ComplexShape.down ℕ).next 2 = 1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
rw :
  Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ A ≫ (chainsIso₁ A).inv) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        (↑x : G × G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    (0 : (↑((inhomogeneousChains A).X 1) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousChains A).X 2) (Y := (inhomogeneousChains A).X 1)
            ((inhomogeneousChains A).d 2 1) :
          (a : (↑((inhomogeneousChains A).X 2) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chainsIso₂ A).inv :
            (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
          (↑x : G × G →₀ (↑A : Type u))) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    (0 : (↑((inhomogeneousChains A).X 1) : Type u))

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]

Premises used: groupHomology.eq_d₂₁_comp_inv, LinearMap.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ A ≫ (chainsIso₁ A).inv) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        (↑x : G × G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    (0 : (↑((inhomogeneousChains A).X 1) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
rw :
  Eq (α := (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₂ A).inv :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        (↑x : G × G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 2) (iCycles A 2) :
          (a : (↑(cycles A 2) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₂ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(cycles A 2) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 2) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 2) (iCycles A 2) :
          (a : (↑(cycles A 2) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        (cyclesMk 2 1 cyclesMk₂_eq._proof_1
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (chainsIso₂ A).inv :
              (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
            (↑x : G × G →₀ (↑A : Type u)))
          ⋯) :
      (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 2) (iCycles A 2) :
          (a : (↑(cycles A 2) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₂ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(cycles A 2) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 2) : Type u))

Tactic:
rw [iCycles_mk]

Premises used: groupHomology.iCycles_mk
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
simp :
  Eq (α := (Fin 2 → G) →₀ (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₂ A).inv :
          (a : G × G →₀ (↑A : Type u)) → (Fin 2 → G) →₀ (↑A : Type u))
        (↑x : G × G →₀ (↑A : Type u)) :
      (Fin 2 → G) →₀ (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (chainsIso₂ A).inv) :
          (a : ↥(cycles₂ A)) → (Fin 2 → G) →₀ (↑A : Type u))
        x :
      (Fin 2 → G) →₀ (↑A : Type u))
⊢ Eq (α := (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₂ A).inv :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        (↑x : G × G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 2) (iCycles A 2) :
          (a : (↑(cycles A 2) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₂ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(cycles A 2) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 2) : Type u))

Tactic:
simp only [ChainComplex.of_X, isoCycles₂_inv_comp_iCycles_apply]

Premises used: ChainComplex.of_X, groupHomology.isoCycles₂_inv_comp_iCycles_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ Eq (α := (Fin 2 → G) →₀ (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₂ A).inv :
          (a : G × G →₀ (↑A : Type u)) → (Fin 2 → G) →₀ (↑A : Type u))
        (↑x : G × G →₀ (↑A : Type u)) :
      (Fin 2 → G) →₀ (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (chainsIso₂ A).inv) :
          (a : ↥(cycles₂ A)) → (Fin 2 → G) →₀ (↑A : Type u))
        x :
      (Fin 2 → G) →₀ (↑A : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Epi (H0π A)

Tactic:
inferInstanceAs <| Epi (_ ≫ _)

Premises used: _private.0.groupHomology.instEpiModuleCatH0π._proof_1
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ π A 0 ≫ (H0Iso A).hom = (cyclesIso₀ A).hom ≫ NatTrans.app (coinvariantsMk k G) A

Tactic:
simp [H0Iso, cyclesIso₀]

Premises used: groupHomology.cyclesIso₀, groupHomology.H0Iso
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ NatTrans.app (coinvariantsMk k G) A ≫ (H0Iso A).inv = H0π A

Tactic:
(CommSq.vert_inv ⟨π_comp_H0Iso_hom A⟩).w

Premises used: CategoryTheory.CommSq.vert_inv, CategoryTheory.CommSq.mk, groupHomology.H0π, groupHomology.π_comp_H0Iso_hom, CategoryTheory.CommSq.w
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ H0π A ≫ (H0Iso A).hom = NatTrans.app (coinvariantsMk k G) A

Tactic:
simp [H0π]

Premises used: groupHomology.H0π
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (cyclesIso₀ A).hom ≫ H0π A = π A 0

Tactic:
simp [H0π]

Premises used: groupHomology.H0π