awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 0
| (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

Tactic:
rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]

Premises used: Rep.barComplex, HomologicalComplex.coinvariantsTensorObj, HomologicalComplex.d_comp_d, CategoryTheory.Category.id_comp
-- 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))) ≫
      0 ≫ 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))))
    (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

Tactic:
slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]

Premises used: Rep.barComplex, HomologicalComplex.coinvariantsTensorObj, HomologicalComplex.d_comp_d, CategoryTheory.Category.id_comp
-- 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 : ℕ
⊢ 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))) ≫
      0 ≫ Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
    0

Tactic:
simp
-- 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 : ℕ
simp : inhomogeneousChains.d A (n + 1) ≫ inhomogeneousChains.d A n = 0
simp₁ :
  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
simp₂ :
  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
simp₃ :
  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))) ≫
      0 ≫ Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
    0
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := ModuleCat k)
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) (n + 1 + 1))
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) n))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) (n + 1))
      ((fun (n : ℕ) ↦ inhomogeneousChains.d A n) (n + 1)) ((fun (n : ℕ) ↦ inhomogeneousChains.d A n) n))
    0

Tactic:
classical
    simp only
    rw [inhomogeneousChains.d_eq, inhomogeneousChains.d_eq]
    slice_lhs 3 4 => rw [Iso.hom_inv_id]
    slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]
    simp

Premises used: CategoryTheory.Iso.hom_inv_id, Rep.barComplex, HomologicalComplex.coinvariantsTensorObj, HomologicalComplex.d_comp_d, groupHomology.inhomogeneousChains.d_eq, CategoryTheory.Category.id_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
M : ModuleCat k
x y : (inhomogeneousChains A).X n ⟶ M
h : ∀ (g : Fin n → G), ModuleCat.ofHom (lsingle g) ≫ x = ModuleCat.ofHom (lsingle g) ≫ y
⊢ x = y

Tactic:
ModuleCat.hom_ext <| lhom_ext' fun g => ModuleCat.hom_ext_iff.1 (h g)

Premises used: Finsupp.lhom_ext', ModuleCat.hom_ext_iff, Iff.mp, ModuleCat.hom_ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ (inhomogeneousChains A).d (n + 1) n = d A n

Tactic:
simp [inhomogeneousChains]

Premises used: groupHomology.inhomogeneousChains
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ d A (n + 1) ≫ d A n = 0

Tactic:
simpa [ChainComplex.of.d] using ((inhomogeneousChains A).d_comp_d (n + 2) (n + 1) n)

Premises used: HAdd.hAdd, ChainComplex.of.d, HomologicalComplex.d_comp_d, OfNat.ofNat, groupHomology.inhomogeneousChains
-- 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 : ℕ
inst_4 : DecidableEq G
refine_1 : (i : ℕ) → (inhomogeneousChains A).X i ≅ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X i
refine_2 :
  ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      Iso.hom (Iso.symm (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin i → G)))) ≫
          (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d i j =
        (inhomogeneousChains A).d i j ≫
          Iso.hom (Iso.symm (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin j → G))))
⊢ inhomogeneousChains A ≅ HomologicalComplex.coinvariantsTensorObj A (barComplex k G)

Tactic:
refine HomologicalComplex.Hom.isoOfComponents ?_ ?_

Premises used: HomologicalComplex.Hom.isoOfComponents
-- 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 : ℕ
inst_4 : DecidableEq G
i : ℕ
⊢ (inhomogeneousChains A).X i ≅ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X i

Tactic:
apply (coinvariantsTensorFreeLEquiv A (Fin i → G)).toModuleIso.symm

Premises used: LinearEquiv.toModuleIso, Rep.coinvariantsTensorFreeLEquiv, CategoryTheory.Iso.symm
-- 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 : ℕ
inst_4 : DecidableEq G
j : ℕ
⊢ Eq (α := (inhomogeneousChains A).X (j + 1) ⟶ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X j)
    (Iso.hom (Iso.symm (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (j + 1) → G)))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (j + 1) j)
    ((inhomogeneousChains A).d (j + 1) j ≫
      Iso.hom (Iso.symm (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin j → G)))))

Tactic:
simp [d_eq, -LinearEquiv.toModuleIso_hom, -LinearEquiv.toModuleIso_inv]

Premises used: LinearEquiv.toModuleIso_inv, groupHomology.inhomogeneousChains.d_eq, LinearEquiv.toModuleIso_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
m n : ℕ
h : (ComplexShape.down ℕ).next m = n
f : (Fin m → G) →₀ (↑A : Type u)
hf :
  Eq (α := (↑((inhomogeneousChains A).X n) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousChains A).d m n) :
          (a : (↑((inhomogeneousChains A).X m) : Type u)) → (↑((inhomogeneousChains A).X n) : Type u))
        f :
      (↑((inhomogeneousChains A).X n) : Type u))
    (0 : (↑((inhomogeneousChains A).X n) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (iCycles A m) :
        (a : (↑(cycles A m) : Type u)) → (↑((inhomogeneousChains A).X m) : Type u))
      (cyclesMk m n h f hf) =
    f

Tactic:
(inhomogeneousChains A).i_cyclesMk f n h hf

Premises used: HomologicalComplex.i_cyclesMk, groupHomology.inhomogeneousChains
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
m n : ℕ
h : (ComplexShape.down ℕ).next m = n
f : (Fin m → G) →₀ (↑A : Type u)
hf :
  Eq (α := (↑((inhomogeneousChains A).X n) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousChains A).d m n) :
          (a : (↑((inhomogeneousChains A).X m) : Type u)) → (↑((inhomogeneousChains A).X n) : Type u))
        f :
      (↑((inhomogeneousChains A).X n) : Type u))
    (0 : (↑((inhomogeneousChains A).X n) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (iCycles A m) :
        (a : (↑(cycles A m) : Type u)) → (↑((inhomogeneousChains A).X m) : Type u))
      (cyclesMk m n h f hf) =
    f

Tactic:
exact (inhomogeneousChains A).i_cyclesMk f n h hf

Premises used: HomologicalComplex.i_cyclesMk, groupHomology.inhomogeneousChains
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
C : (↑(groupHomology A n) : Type u) → Prop
x : (↑(groupHomology A n) : Type u)
h rcases :
  ∀ (y : (↑(cycles A n) : Type u)),
    C
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (π A n) :
          (a : (↑(cycles A n) : Type u)) → (↑(groupHomology A n) : Type u))
        y)
⊢ C x

Tactic:
rcases (ModuleCat.epi_iff_surjective (π A n)).1 inferInstance x with ⟨y, rfl⟩

Premises used: ModuleCat.epi_iff_surjective, inferInstance, Iff.mp, rfl, groupHomology.π
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
C : (↑(groupHomology A n) : Type u) → Prop
h :
  ∀ (x : (↑(cycles A n) : Type u)),
    C
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (π A n) :
          (a : (↑(cycles A n) : Type u)) → (↑(groupHomology A n) : Type u))
        x)
y : (↑(cycles A n) : Type u)
⊢ C
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (π A n) :
        (a : (↑(cycles A n) : Type u)) → (↑(groupHomology A n) : Type u))
      y)

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

Tactic:
exact h y
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : Subsingleton G
n : ℕ
⊢ IsZero (groupHomology A (n + 1))

Tactic:
(isZero_Tor_succ_of_projective A (Rep.trivial k G k) n).of_iso <| groupHomologyIsoTor _ _

Premises used: CategoryTheory.Limits.IsZero.of_iso, Rep.trivial, Rep.isZero_Tor_succ_of_projective, groupHomologyIsoTor
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g_1 : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g_1) x
j : ℕ
a : (↑A : Type u)
g : G
hj : Even (j + 1)
⊢ ∀ (i : G),
    Membership.mem (γ := Finset G) Finset.univ i ↔
      Membership.mem (α := G) (γ := Finset G) Finset.univ ((MulEquiv.inv G : (a : G) → G) i : G)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g_1 : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g_1) x
j : ℕ
a : (↑A : Type u)
g : G
hj : Even (j + 1)
⊢ ∀ (i : G),
    Membership.mem (γ := Finset G) Finset.univ i →
      Eq (α := (↑A : Type u))
        ((((A.ρ : (a : G) → Module.End k (↑A : Type u)) (i * g⁻¹) : Module.End k (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a :
          (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u))
                  (HMul.hMul (α := G) (((MulEquiv.inv G : (a : G) → G) i)⁻¹ : G) g⁻¹) :
                (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a :
          (↑A : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g_1 : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g_1) x
j : ℕ
a : (↑A : Type u)
g : G
hj : Even (j + 1)
⊢ Eq (α := (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                  (ModuleCat.Hom.hom
                    (CategoryStruct.comp (Y := (moduleCatChainComplex A g_1).X (j + 1))
                      (Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) (j + 1)))
                      ((moduleCatChainComplex A g_1).d (j + 1) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                  (ModuleCat.Hom.hom
                    ((HomologicalComplex.coinvariantsTensorObj A
                            (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯))).d
                        (j + 1) j ≫
                      Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))

Tactic:
simpa [hj, coinvariantsTensorMk, ofCoinvariantsTprodLeftRegular, Rep.norm,
        Representation.norm, ← Module.End.mul_apply, ← map_mul, mul_comm g⁻¹] using
        Finset.sum_bijective _ (MulEquiv.inv G).bijective (by simp) (by simp)

Premises used: MulEquiv.inv, Representation.ofCoinvariantsTprodLeftRegular, Rep.norm, map_mul, Inv.inv, Finset.sum_bijective, mul_comm, MulEquiv.bijective, Representation.norm, Module.End.mul_apply, Rep.coinvariantsTensorMk
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g_1 : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g_1) x
j : ℕ
a : (↑A : Type u)
g : G
hj : ¬Even (j + 1)
⊢ Eq (α := (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                  (ModuleCat.Hom.hom
                    (CategoryStruct.comp (Y := (moduleCatChainComplex A g_1).X (j + 1))
                      (Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) (j + 1)))
                      ((moduleCatChainComplex A g_1).d (j + 1) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                  (ModuleCat.Hom.hom
                    ((HomologicalComplex.coinvariantsTensorObj A
                            (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯))).d
                        (j + 1) j ≫
                      Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))

Tactic:
simp [sub_hom, hj, Rep.applyAsHom, coinvariantsTensorMk, TensorProduct.tmul_sub,
        ← Module.End.mul_apply, ← map_mul, mul_comm g⁻¹, Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, TensorProduct.tmul_sub, Rep.applyAsHom, map_mul, Rep.sub_hom, Inv.inv, mul_comm, Module.End.mul_apply, Rep.coinvariantsTensorMk
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ Coinvariants.ker A.ρ = (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range

Tactic:
simp [Representation.FiniteCyclicGroup.coinvariantsKer_eq_range A.ρ g hg, sub_hom,
      Rep.applyAsHom]

Premises used: Representation.FiniteCyclicGroup.coinvariantsKer_eq_range, Rep.applyAsHom, Rep.sub_hom, Rep.ρ
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
                ModuleCat.ofHom
                  (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom 0 :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
      ModuleCat.ofHom
        (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap =
    0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
              ModuleCat.ofHom
                (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [sub_hom,
    Rep.applyAsHom, Rep.norm]

Premises used: Rep.norm, Rep.applyAsHom, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
h₀ : NeZero i
hi : Even i
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom
                  (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
                ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom 0 :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ ModuleCat.ofHom (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).toLinearMap ≫
      ModuleCat.ofHom (Hom.hom A.norm).toLinearMap =
    0

Tactic:
ext