awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
hf :
  ∀ (i : Fin 0 → G) (x : (↑A : Type u)) (g : Fin 1 → G),
    Eq (α := (↑A : Type u))
      ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1) ∘ₗ
              LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) i :
            (a : (↑A : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
          x g :
        (↑A : Type u))
      (((ModuleCat.Hom.hom 0 :
                (↑((inhomogeneousCochains A).X 0) : Type u) →ₗ[k] (↑((inhomogeneousCochains A).X 1) : Type u)) ∘ₗ
              LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) i :
            (a : (↑A : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
          x g :
        (↑A : Type u))
⊢ Eq (α := (inhomogeneousCochains A).X 0 ⟶ (inhomogeneousCochains A).X 1) ((inhomogeneousCochains A).d 0 1) 0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
i : Fin 0 → G
x : (↑A : Type u)
g : Fin 1 → G
⊢ Eq (α := (↑A : Type u))
    ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) i :
          (a : (↑A : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
        x g :
      (↑A : Type u))
    (((ModuleCat.Hom.hom 0 :
              (↑((inhomogeneousCochains A).X 0) : Type u) →ₗ[k] (↑((inhomogeneousCochains A).X 1) : Type u)) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) i :
          (a : (↑A : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
        x g :
      (↑A : Type u))

Tactic:
simp [inhomogeneousCochains.d, Unique.eq_default (α := Fin 0 → G),
      CochainComplex.of.d]

Premises used: inhomogeneousCochains.d, CochainComplex.of.d, Unique.eq_default
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ H1π A ≫ (H1IsoOfIsTrivial A).hom = (cocycles₁IsoOfIsTrivial A).hom

Tactic:
simp [H1IsoOfIsTrivial, H1π]

Premises used: groupCohomology.H1IsoOfIsTrivial, groupCohomology.H1π
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
f : ↥(cocycles₁ A)
x : Additive G
⊢ Eq (α := (↑A : Type u))
    ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (H1IsoOfIsTrivial A).hom :
                (a : (↑(H1 A) : Type u)) → (↑(ModuleCat.of k (Additive G →+ (↑A : Type u))) : 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))
                f) :
            (↑(ModuleCat.of k (Additive G →+ (↑A : Type u))) : Type u)) :
          (a : Additive G) → (↑A : Type u))
        x :
      (↑A : Type u))
    ((f : (a : G) → (↑A : Type u)) ((Additive.toMul : (a : Additive G) → G) x : G) : (↑A : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
f : Additive G →+ (↑A : Type u)
⊢ Eq (α := (↑(H1 A) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1IsoOfIsTrivial A).inv :
          (a : (↑(ModuleCat.of k (Additive G →+ (↑A : Type u))) : Type u)) → (↑(H1 A) : Type u))
        f :
      (↑(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))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cocycles₁IsoOfIsTrivial A).inv :
              (a : (↑(ModuleCat.of k (Additive G →+ (↑A : Type u))) : Type u)) →
                (↑(ModuleCat.of k ↥(cocycles₁ A)) : Type u))
            f :
          (↑(ModuleCat.of k ↥(cocycles₁ A)) : Type u)) :
      (↑(H1 A) : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Epi (H2π A)

Tactic:
inferInstanceAs <| Epi (_ ≫ _)

Premises used: _private.0.groupCohomology.instEpiModuleCatH2π._proof_1
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ Eq (α :=
    (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 2).homology)
    ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
    (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)

Tactic:
have h := leftHomologyπ_naturality'_assoc (isoShortComplexH2 A).inv
    (shortComplexH2 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousCochains A).sc 2).leftHomologyIso.hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₂ A)
h :
  Eq (α :=
    (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 2).homology)
    ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
    (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
simp :
  Eq (α := (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
      ((ModuleCat.Hom.hom (shortComplexH2 A).moduleCatLeftHomologyData.π :
            (a : ↥(cocycles₂ A)) → (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
          x :
        (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
      (0 : (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u)) ↔
    (⇑x : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A
⊢ Eq (α := (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cocycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      (0 : (↑(H2 A) : Type u)) ↔
    (⇑x : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A

Tactic:
simp only [H2π, isoCocycles₂, π, 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: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.ShortComplex.cyclesMapIso'_inv, inferInstance, ModuleCat.mono_iff_injective, LinearMap.coe_comp, map_eq_zero_iff, groupCohomology.isoCocycles₂, CategoryTheory.ShortComplex.leftHomologyMapIso'_inv, Iff.mp, groupCohomology.π, Function.comp_apply, ModuleCat.hom_comp, groupCohomology.H2π
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₂ A)
h :
  Eq (α :=
    (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 2).homology)
    ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
    (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
⊢ Eq (α := (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
      ((ModuleCat.Hom.hom (shortComplexH2 A).moduleCatLeftHomologyData.π :
            (a : ↥(cocycles₂ A)) → (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
          x :
        (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
      (0 : (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u)) ↔
    (⇑x : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A

Tactic:
simp [LinearMap.range_codRestrict, coboundaries₂, shortComplexH2, cocycles₂]

Premises used: groupCohomology.shortComplexH2, groupCohomology.coboundaries₂, groupCohomology.cocycles₂, LinearMap.range_codRestrict
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cocycles₂ A)
rw :
  (⇑(x - y) : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A ↔
    HSub.hSub (α := (a : G × G) → (↑A : Type u)) (⇑x : (a : G × G) → (↑A : Type u)) (⇑y : (a : G × G) → (↑A : Type u)) ∈
      coboundaries₂ A
⊢ Eq (α := (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cocycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cocycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          y :
        (↑(H2 A) : Type u)) ↔
    HSub.hSub (α := (a : G × G) → (↑A : Type u)) (⇑x : (a : G × G) → (↑A : Type u)) (⇑y : (a : G × G) → (↑A : Type u)) ∈
      coboundaries₂ A

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

Premises used: map_sub, sub_eq_zero, groupCohomology.H2π_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cocycles₂ A)
⊢ (⇑(x - y) : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A ↔
    HSub.hSub (α := (a : G × G) → (↑A : Type u)) (⇑x : (a : G × G) → (↑A : Type u)) (⇑y : (a : G × G) → (↑A : Type u)) ∈
      coboundaries₂ A

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

Tactic:
simpa [H2π] using h ((isoCocycles₂ A).hom y)

Premises used: CategoryTheory.ConcreteCategory.hom, groupCohomology.isoCocycles₂, CategoryTheory.Iso.hom, DFunLike.coe, groupCohomology.H2π
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ π A 2 ≫ (H2Iso A).hom = (isoCocycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.π

Tactic:
simp [H2Iso, isoCocycles₂, π, HomologicalComplex.homologyπ, leftHomologyπ]

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.leftHomologyπ, groupCohomology.H2Iso, groupCohomology.isoCocycles₂, groupCohomology.π
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A_1 : Rep.{?u.447, u, u} k ↥S
P : ProjectiveResolution (C := Rep.{u, u, u} k G) (Rep.trivial k G k)
A : Rep.{u, u, u} k ↥S
x x_1 : ℕ
h : (ComplexShape.up ℕ).Rel x x_1
f :
  (↑(HomologicalComplex.X
        (ChainComplex.linearYonedaObj
          (ProjectiveResolution.complex (Z := Functor.obj (resFunctor S.subtype) (Rep.trivial k G k))
            (Functor.mapProjectiveResolution (resFunctor S.subtype) P))
          k A)
        x) :
    Type u)
x_2 : (↑(Opposite.unop (Opposite.op (P.complex.X x_1))) : Type u)
x_3 : G
⊢ Eq.{u + 1} (α := (↑A : Type u))
    ((↑((Representation.IntertwiningMap.toLinearMap
                (Hom.hom
                  ((ModuleCat.Hom.hom
                        (Iso.hom
                            ((fun (x : ℕ) ↦ (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x) A).toModuleIso)
                              x) ≫
                          HomologicalComplex.d (P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)) x x_1) :
                      (a :
                          (↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x) :
                            Type u)) →
                        (↑((P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).X x_1) : Type u))
                    f)) :
              (a : (↑(Opposite.unop (Opposite.op (P.complex.X x_1))) : Type u)) →
                (↑(coind.{u, u, u, u} S.subtype A) : Type u))
            x_2) :
        G → (↑A : Type u))
      x_3)
    ((↑((Representation.IntertwiningMap.toLinearMap
                (Hom.hom
                  ((ModuleCat.Hom.hom
                        (HomologicalComplex.d
                            (ChainComplex.linearYonedaObj
                              (ProjectiveResolution.complex (Z :=
                                Functor.obj (resFunctor S.subtype) (Rep.trivial k G k))
                                (Functor.mapProjectiveResolution (resFunctor S.subtype) P))
                              k A)
                            x x_1 ≫
                          Iso.hom
                            ((fun (x : ℕ) ↦ (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x) A).toModuleIso)
                              x_1)) :
                      (a :
                          (↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x) :
                            Type u)) →
                        (↑((P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).X x_1) : Type u))
                    f)) :
              (a : (↑(Opposite.unop (Opposite.op (P.complex.X x_1))) : Type u)) →
                (↑(coind.{u, u, u, u} S.subtype A) : Type u))
            x_2) :
        G → (↑A : Type u))
      x_3)

Tactic:
simp [← ModuleCat.ofHom_comp, resCoindHomEquiv, hom_comm_apply]

Premises used: ModuleCat.ofHom_comp, Rep.resCoindHomEquiv, Rep.hom_comm_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X Y : Rep k G
inst_2 : Projective Y
n : ℕ
⊢ IsZero ((Functor.obj (Tor k G (n + 1)) X).obj Y)

Tactic:
Functor.isZero_leftDerived_obj_projective_succ ..

Premises used: CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
g : Fin (n + 1) → G
a : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d A n) :
        (a : (↑(ModuleCat.of k ((Fin (n + 1) → G) →₀ (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
      (single g a) =
    HAdd.hAdd (α := ((i : Fin n) → G) →₀ (↑A : Type u)) (β := ((k : Fin n) → G) →₀ (↑A : Type u))
      (single (fun (i : Fin n) ↦ g i.succ)
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) (g 0)⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        ((i : Fin n) → G) →₀ (↑A : Type u))
      (∑ j : Fin (n + 1),
          HSMul.hSMul (β := ((k : Fin n) → G) →₀ (↑A : Type u)) (HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1))
            (single (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) a) :
        ((k : Fin n) → G) →₀ (↑A : Type u))

Tactic:
simp [d]

Premises used: groupHomology.inhomogeneousChains.d
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
inst_2 : DecidableEq G
hf :
  ∀ (a : Fin (n + 1) → G) (x : (↑A : Type u)),
    Eq (α := (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
      ((ModuleCat.Hom.hom (d A n) ∘ₗ lsingle a :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
          x :
        (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
      ((ModuleCat.Hom.hom
                (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
                  (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
                    Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))) ∘ₗ
              lsingle a :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
          x :
        (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
⊢ d A n =
    Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
        Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))

Tactic:
ext : 3
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
inst_2 : DecidableEq G
a : Fin (n + 1) → G
x : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom (d A n) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom
              (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
                (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
                  Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))) ∘ₗ
            lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))

Tactic:
simp [d_single (k := k), TensorProduct.tmul_add, TensorProduct.tmul_sum,
    barComplex.d_single (k := k)]

Premises used: TensorProduct.tmul_sum, groupHomology.inhomogeneousChains.d_single, TensorProduct.tmul_add, Rep.barComplex.d_single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
rw :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
      (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) →₀ (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))))
    0
⊢ inhomogeneousChains.d A (n + 1) ≫ inhomogeneousChains.d A n = 0

Tactic:
rw [inhomogeneousChains.d_eq, inhomogeneousChains.d_eq]

Premises used: groupHomology.inhomogeneousChains.d_eq
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
a : 𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1))
| Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
    Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)))

Tactic:
rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
slice_lhs :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
      (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
        (𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1)) ≫
            (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n) ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
    0
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
      (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) →₀ (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))))
    0

Tactic:
slice_lhs 3 4 => rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id