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
C : (↑(H0 A) : Type u) → Prop
x : (↑(H0 A) : Type u)
h :
  ∀ (x : (↑A : Type u)),
    C
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H0π A) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(H0 A) : Type u))
        x)
y : (↑(cycles A 0) : Type u)
⊢ C
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := cycles A 0) (π A 0) :
        (a : (↑(cycles A 0) : Type u)) → (↑(groupHomology A 0) : Type u))
      y)

Tactic:
simpa using h ((cyclesIso₀ A).hom y)

Premises used: CategoryTheory.ConcreteCategory.hom, groupHomology.cyclesIso₀, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ (ComplexShape.down ℕ).prev 0 = 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
inst_2 : A.IsTrivial
h :
  ∀ (g : Fin 1 → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
    Eq (α := (↑A : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (inhomogeneousChains A).d 1 0) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
                x :
              (↑((inhomogeneousChains A).X 0) : Type u)) :
            (a : Fin 0 → G) → (↑A : Type u))
          default :
        (↑A : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ 0) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
                x :
              (↑((inhomogeneousChains A).X 0) : Type u)) :
            (a : Fin 0 → G) → (↑A : Type u))
          default :
        (↑A : Type u))
⊢ Eq (α := (inhomogeneousChains A).X 1 ⟶ (inhomogeneousChains A).X 0) ((inhomogeneousChains A).d 1 0) 0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g : Fin 1 → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
⊢ Eq (α := (↑A : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (inhomogeneousChains A).d 1 0) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
              x :
            (↑((inhomogeneousChains A).X 0) : Type u)) :
          (a : Fin 0 → G) → (↑A : Type u))
        default :
      (↑A : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ 0) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
              x :
            (↑((inhomogeneousChains A).X 0) : Type u)) :
          (a : Fin 0 → G) → (↑A : Type u))
        default :
      (↑A : Type u))

Tactic:
simp [inhomogeneousChains.d_single (G := G), ChainComplex.of.d,
       Unique.eq_default (α := Fin 0 → G)]

Premises used: groupHomology.inhomogeneousChains.d_single, Unique.eq_default, ChainComplex.of.d
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ (H0IsoOfIsTrivial A).inv = H0π A

Tactic:
rfl

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

Tactic:
simp [H0IsoOfIsTrivial]

Premises used: groupHomology.H0IsoOfIsTrivial
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Epi (H1π A)

Tactic:
inferInstanceAs <| Epi (_ ≫ _)

Premises used: _private.0.groupHomology.instEpiModuleCatH1π._proof_1
-- 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 (α := (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 1).homology)
    ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)
    (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)

Tactic:
have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv
    (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousChains A).sc 1).leftHomologyIso.hom
-- 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)
h :
  Eq (α := (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 1).homology)
    ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)
    (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)
simp :
  Eq (α := (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
      ((ModuleCat.Hom.hom (shortComplexH1 A).moduleCatLeftHomologyData.π :
            (a : ↥(cycles₁ A)) → (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
          x :
        (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
      (0 : (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u)) ↔
    (↑x : G →₀ (↑A : Type u)) ∈ boundaries₁ 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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          x :
        (↑(H1 A) : Type u))
      (0 : (↑(H1 A) : Type u)) ↔
    (↑x : G →₀ (↑A : Type u)) ∈ boundaries₁ A

Tactic:
simp only [H1π, isoCycles₁, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]

Premises used: groupHomology.isoCycles₁, HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.ShortComplex.cyclesMapIso'_inv, inferInstance, ModuleCat.mono_iff_injective, groupHomology.H1π, LinearMap.coe_comp, map_eq_zero_iff, CategoryTheory.ShortComplex.leftHomologyMapIso'_inv, Iff.mp, Function.comp_apply, ModuleCat.hom_comp, groupHomology.π
-- 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)
h :
  Eq (α := (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 1).homology)
    ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)
    (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)
⊢ Eq (α := (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
      ((ModuleCat.Hom.hom (shortComplexH1 A).moduleCatLeftHomologyData.π :
            (a : ↥(cycles₁ A)) → (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
          x :
        (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
      (0 : (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u)) ↔
    (↑x : G →₀ (↑A : Type u)) ∈ boundaries₁ A

Tactic:
simp [LinearMap.range_codRestrict, boundaries₁, shortComplexH1, cycles₁]

Premises used: groupHomology.cycles₁, groupHomology.shortComplexH1, LinearMap.range_codRestrict, groupHomology.boundaries₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cycles₁ A)
rw :
  (↑(x - y) : G →₀ (↑A : Type u)) ∈ boundaries₁ A ↔
    (↑x : G →₀ (↑A : Type u)) - (↑y : G →₀ (↑A : Type u)) ∈ boundaries₁ 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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          x :
        (↑(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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          y :
        (↑(H1 A) : Type u)) ↔
    (↑x : G →₀ (↑A : Type u)) - (↑y : G →₀ (↑A : Type u)) ∈ boundaries₁ A

Tactic:
rw [← sub_eq_zero, ← map_sub, H1π_eq_zero_iff]

Premises used: map_sub, sub_eq_zero, groupHomology.H1π_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cycles₁ A)
⊢ (↑(x - y) : G →₀ (↑A : Type u)) ∈ boundaries₁ A ↔
    (↑x : G →₀ (↑A : Type u)) - (↑y : G →₀ (↑A : Type u)) ∈ boundaries₁ A

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
C : (↑(H1 A) : Type u) → Prop
x : (↑(H1 A) : Type u)
h :
  ∀ (x : ↥(cycles₁ A)),
    C
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π A) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
        x)
y : (↑(cycles A 1) : Type u)
⊢ C
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := cycles A 1) (π A 1) :
        (a : (↑(cycles A 1) : Type u)) → (↑(groupHomology A 1) : Type u))
      y)

Tactic:
simpa [H1π] using h ((isoCycles₁ A).hom y)

Premises used: groupHomology.isoCycles₁, CategoryTheory.ConcreteCategory.hom, groupHomology.H1π, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ π A 1 ≫ (H1Iso A).hom = (isoCycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π

Tactic:
simp [H1Iso, isoCycles₁, π, HomologicalComplex.homologyπ, leftHomologyπ]

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

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

Premises used: Set.Mem, CategoryTheory.CommSq.vert_inv, groupHomology.H1π, CategoryTheory.CommSq.mk, groupHomology.cycles₁, CategoryTheory.CommSq.w, groupHomology.π_comp_H1Iso_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g h : G
a : (↑A : Type u)
⊢ (ModuleCat.Hom.hom (d₂₁ A) : (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → G →₀ (↑A : Type u))
      (single (g, h) a) =
    HSub.hSub (α := G →₀ (↑A : Type u))
      (↑((ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv : (a : G →₀ (↑A : Type u)) → ↥(cycles₁ A))
            (HAdd.hAdd (α := G →₀ (↑A : Type u)) (single g a) (single h a))) :
        G →₀ (↑A : Type u))
      (↑((ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv : (a : G →₀ (↑A : Type u)) → ↥(cycles₁ A))
            (single (g * h) a)) :
        G →₀ (↑A : Type u))

Tactic:
simp [cycles₁IsoOfIsTrivial, sub_add_eq_add_sub, add_comm (single h a),
          d₂₁_single (A := A)]

Premises used: groupHomology.cycles₁IsoOfIsTrivial, add_comm, groupHomology.d₂₁_single, sub_add_eq_add_sub, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g h : G
a : (↑A : Type u)
⊢ Eq (α := (↑(H1 A) : Type u))
    ((((Multiplicative.toAdd :
                (a : Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u))) → (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u))
              ((Multiplicative.ofAdd :
                  (a : (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)) →
                    Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)))
                (AddMonoidHom.toIntLinearMap
                  (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle (g * h)) :
                    (↑A : Type u) →+ (↑(H1 A) : Type u)))) :
            (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)) :
          (a : (↑A : Type u)) → (↑(H1 A) : Type u))
        a :
      (↑(H1 A) : Type u))
    ((((Multiplicative.toAdd :
                (a : Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u))) → (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u))
              (HMul.hMul (α := Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u))) (β :=
                Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)))
                ((Multiplicative.ofAdd :
                      (a : (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)) →
                        Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)))
                    (AddMonoidHom.toIntLinearMap
                      (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle g) :
                        (↑A : Type u) →+ (↑(H1 A) : Type u))) :
                  Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)))
                ((Multiplicative.ofAdd :
                      (a : (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)) →
                        Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)))
                    (AddMonoidHom.toIntLinearMap
                      (↑(ModuleCat.Hom.hom (H1π A) ∘ₗ ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).inv ∘ₗ lsingle h) :
                        (↑A : Type u) →+ (↑(H1 A) : Type u))) :
                  Multiplicative ((↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)))) :
            (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)) :
          (a : (↑A : Type u)) → (↑(H1 A) : Type u))
        a :
      (↑(H1 A) : Type u))

Tactic:
simpa [← map_add] using ((H1π_eq_iff _ _).2 ⟨single (g, h) a, by
        simp [cycles₁IsoOfIsTrivial, sub_add_eq_add_sub, add_comm (single h a),
          d₂₁_single (A := A)]⟩).symm

Premises used: Iff.mpr, map_add, Prod.mk, Exists.intro, Eq.symm, Finsupp.single, groupHomology.H1π_eq_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g : G
a : (↑A : Type u)
⊢ Eq (α := (↑(H1 A) : Type u))
    ((((mkH1OfIsTrivial A : (a : Additive (Abelianization G)) → (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u))
              ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
                ((Abelianization.of : (a : G) → Abelianization G) g)) :
            (↑A : Type u) →ₗ[ℤ] (↑(H1 A) : Type u)) :
          (a : (↑A : Type u)) → (↑(H1 A) : Type u))
        a :
      (↑(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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
              (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
            (single g a) :
          (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) :
      (↑(H1 A) : Type u))

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
x : ↥(cycles₁ A).toAddSubgroup
y : G →₀ (↑A : Type u)
hy : y ∈ (cycles₁ A).toAddSubgroup
h :
  Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ (cycles₁ A).toAddSubgroup) y hy ∈
    (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
z : (↑(shortComplexH1 A).X₁ : Type u)
hz :
  ((shortComplexH1 A).moduleCatToCycles :
        (a : (↑(shortComplexH1 A).X₁ : Type u)) → ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker)
      z =
    Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ (cycles₁ A).toAddSubgroup) y hy
⊢ Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((AddMonoidHom.comp
            ((Finsupp.liftAddHom :
                (a : G → (↑A : Type u) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                  (G →₀ (↑A : Type u)) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
              fun (g : G) ↦
              (↑((TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u) :
                        (a : Additive (Abelianization G)) →
                          (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
                      ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
                        ((Abelianization.of : (a : G) → Abelianization G) g)) :
                    (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
                (↑A : Type u) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
            (cycles₁ A).toAddSubgroup.subtype :
          (a : ↥(cycles₁ A).toAddSubgroup) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
        (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ (cycles₁ A).toAddSubgroup) y hy) :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    (0 : Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))

Tactic:
simp [← hz, d₂₁, sum_sum_index, sum_add_index', tmul_add, sum_sub_index, tmul_sub,
        shortComplexH1]

Premises used: Finsupp.sum_sub_index, TensorProduct.tmul_sub, Finsupp.sum_add_index', groupHomology.d₂₁, TensorProduct.tmul_add, groupHomology.shortComplexH1, Finsupp.sum_sum_index
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g : G
a : (↑A : Type u)
⊢ Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((QuotientAddGroup.lift (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
            (AddMonoidHom.comp
              ((Finsupp.liftAddHom :
                  (a : G → (↑A : Type u) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                    (G →₀ (↑A : Type u)) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
                fun (g : G) ↦
                (↑((TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u) :
                          (a : Additive (Abelianization G)) →
                            (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
                        ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
                          ((Abelianization.of : (a : G) → Abelianization G) g)) :
                      (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
                  (↑A : Type u) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
              (cycles₁ A).toAddSubgroup.subtype)
            ⋯ :
          (a :
              ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker ⧸
                (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup) →
            Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1Iso A).hom :
            (a : (↑(H1 A) : Type u)) → (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) ((isoCycles₁ A).inv ≫ π A 1) :
              (a : ↥(cycles₁ A)) → (↑(H1 A) : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
                  (a : G →₀ (↑A : Type u)) → ↥(cycles₁ A))
                (single g a) :
              ↥(cycles₁ A)))) :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))

Tactic:
simp [π_comp_H1Iso_hom_apply, ← Submodule.Quotient.quotientAddGroupMk_eq_mk, Submodule.mkQ,
    AddSubgroup.subtype, cycles₁IsoOfIsTrivial]

Premises used: groupHomology.cycles₁IsoOfIsTrivial, Submodule.Quotient.quotientAddGroupMk_eq_mk, groupHomology.π_comp_H1Iso_hom_apply, AddSubgroup.subtype, Submodule.mkQ