awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
slice_lhs :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
      0 ≫ Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A)))
    0
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
      CategoryStruct.comp (Y := HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1))
        (HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1))
        ((𝟙 (HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1)) ≫
            HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1)) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A))))
    0

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

Premises used: ChainComplex.linearYonedaObj, Rep.barComplex, HomologicalComplex.d_comp_d, CategoryTheory.Category.id_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
      0 ≫ Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A)))
    0

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
simp : d A n ≫ d A (n + 1) = 0
simp₁ :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)))
      (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A))))
    0
simp₂ :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
      CategoryStruct.comp (Y := HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1))
        (HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1))
        ((𝟙 (HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1)) ≫
            HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1)) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A))))
    0
simp₃ :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
      0 ≫ Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A)))
    0
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := ModuleCat k) ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) n)
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) (n + 1 + 1)))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) (n + 1))
      ((fun (n : ℕ) ↦ d A n) n) ((fun (n : ℕ) ↦ d A n) (n + 1)))
    0

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

Premises used: ChainComplex.linearYonedaObj, CategoryTheory.Iso.hom_inv_id, Rep.barComplex, inhomogeneousCochains.d_eq, HomologicalComplex.d_comp_d, CategoryTheory.Category.id_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
A : Rep k G
x y : (↑((inhomogeneousCochains A).X n) : Type u)
h : ∀ (g : Fin n → G), x g = y g
⊢ x = y

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ (inhomogeneousCochains A).d n (n + 1) = d A n

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
A : Rep k G
⊢ d A n ≫ d A (n + 1) = 0

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

Premises used: CochainComplex.of.d, groupCohomology.inhomogeneousCochains, HAdd.hAdd, HomologicalComplex.d_comp_d, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
A : Rep k G
refine :
  ∀ (i j : ℕ),
    (ComplexShape.up ℕ).Rel i j →
      Eq (α :=
        (inhomogeneousCochains A).X i ⟶ HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) j)
        (Iso.hom
            ((fun (i : ℕ) ↦
                (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
                  Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                    (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
              i) ≫
          HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) i j)
        ((inhomogeneousCochains A).d i j ≫
          Iso.hom
            ((fun (i : ℕ) ↦
                (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
                  Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                    (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
              j))
⊢ inhomogeneousCochains A ≅ ChainComplex.linearYonedaObj (barComplex k G) k A

Tactic:
refine HomologicalComplex.Hom.isoOfComponents
    (fun i ↦ (Rep.freeLiftLEquiv k G (Fin i → G) A).toModuleIso.symm) ?_

Premises used: HomologicalComplex.Hom.isoOfComponents
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
A : Rep k G
i j : ℕ
h : i + 1 = j
subst :
  Eq (α :=
    (inhomogeneousCochains A).X i ⟶ HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (i + 1))
    (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
              Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
          i) ≫
      HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) i (i + 1))
    (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
              Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
          (i + 1))))
⊢ Eq (α := (inhomogeneousCochains A).X i ⟶ HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) j)
    (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
              Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
          i) ≫
      HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) i j)
    ((inhomogeneousCochains A).d i j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
              Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
          j))

Tactic:
subst h
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
A : Rep k G
i : ℕ
⊢ Eq (α :=
    (inhomogeneousCochains A).X i ⟶ HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (i + 1))
    (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
              Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
          i) ≫
      HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) i (i + 1))
    (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin i → G) A)) :
              Iso (C := ModuleCat k) (ModuleCat.of k ((Fin i → G) → (↑A : Type u)))
                (ModuleCat.of k (free k G (Fin i → G) ⟶ A))))
          (i + 1))))

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

Premises used: LinearEquiv.toModuleIso_inv, inhomogeneousCochains.d_eq, LinearEquiv.toModuleIso_hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
f : (Fin n → G) → (↑A : Type u)
h :
  Eq (α := (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d A n) :
          (a : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
        f :
      (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
⊢ (ComplexShape.up ℕ).next n = n + 1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
f : (Fin n → G) → (↑A : Type u)
h :
  Eq (α := (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d A n) :
          (a : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
        f :
      (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
⊢ (ComplexShape.up ℕ).next n = n + 1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
f : (Fin n → G) → (↑A : Type u)
h :
  Eq (α := (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d A n) :
          (a : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
        f :
      (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (iCocycles A n) :
        (a : (↑(cocycles A n) : Type u)) → (↑((inhomogeneousCochains A).X n) : Type u))
      (cocyclesMk f h) =
    f

Tactic:
exact (inhomogeneousCochains A).i_cyclesMk (i := n) f (n + 1) (by simp) (by simp [h])

Premises used: HomologicalComplex.i_cyclesMk, groupCohomology.inhomogeneousCochains, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
C : (↑(groupCohomology A n) : Type u) → Prop
x : (↑(groupCohomology A n) : Type u)
h rcases :
  ∀ (y : (↑(cocycles 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 : (↑(cocycles A n) : Type u)) → (↑(groupCohomology 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, groupCohomology.π, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
C : (↑(groupCohomology A n) : Type u) → Prop
h :
  ∀ (x : (↑(cocycles 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 : (↑(cocycles A n) : Type u)) → (↑(groupCohomology A n) : Type u))
        x)
y : (↑(cocycles 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 : (↑(cocycles A n) : Type u)) → (↑(groupCohomology A n) : Type u))
      y)

Tactic:
h y
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
C : (↑(groupCohomology A n) : Type u) → Prop
h :
  ∀ (x : (↑(cocycles 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 : (↑(cocycles A n) : Type u)) → (↑(groupCohomology A n) : Type u))
        x)
y : (↑(cocycles 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 : (↑(cocycles A n) : Type u)) → (↑(groupCohomology A n) : Type u))
      y)

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

Tactic:
(isZero_Ext_succ_of_projective (Rep.trivial k G k) A n).of_iso <| groupCohomologyIsoExt _ _

Premises used: groupCohomologyIsoExt, CategoryTheory.Limits.IsZero.of_iso, Rep.trivial, isZero_Ext_succ_of_projective
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
i : ℕ
hf :
  ∀ (x : leftRegular k G ⟶ A),
    Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
      ((ModuleCat.Hom.hom
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
                (moduleCatCochainComplex A g).d i (i + 1)) :
            (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
              (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
          x :
        (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
      ((ModuleCat.Hom.hom
              (CategoryStruct.comp (Y :=
                HomologicalComplex.X
                  (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) (i + 1))
                (HomologicalComplex.d
                  (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
                (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
            (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
              (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
          x :
        (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
⊢ Eq (α :=
    HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i ⟶
      (moduleCatCochainComplex A g).X (i + 1))
    (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫ (moduleCatCochainComplex A g).d i (i + 1))
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
        (i + 1))
      (HomologicalComplex.d (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i
        (i + 1))
      (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1))))

Tactic:
ext (x : leftRegular _ _ ⟶ _)

Premises used: Rep.leftRegular
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
i : ℕ
x : leftRegular k G ⟶ A
hi : Even i
⊢ ¬Even (i + 1)

Tactic:
have : ¬(Even (i + 1)) := Nat.even_add_one.not_left.mpr hi
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
i : ℕ
x : leftRegular k G ⟶ A
hi : Even i
this : ¬Even (i + 1)
⊢ Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
              (moduleCatCochainComplex A g).d i (i + 1)) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y :=
              HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
                (i + 1))
              (HomologicalComplex.d
                (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))

Tactic:
simp [sub_hom, hi, this, homEquiv, ← hom_comm_apply x, Rep.applyAsHom]

Premises used: Rep.homEquiv, Rep.applyAsHom, Rep.sub_hom, Rep.hom_comm_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
i : ℕ
x : leftRegular k G ⟶ A
hi : ¬Even i
⊢ Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
              (moduleCatCochainComplex A g).d i (i + 1)) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y :=
              HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
                (i + 1))
              (HomologicalComplex.d
                (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))

Tactic:
simp [hi, Nat.even_add_one.2 hi, Representation.norm, homEquiv, Rep.norm, ← hom_comm_apply x]

Premises used: Iff.mpr, Nat.even_add_one, Rep.homEquiv, Rep.norm, Rep.hom_comm_apply, Representation.norm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
h :
  ∀ (x : (↑A : Type u)),
    x ∈ A.ρ.invariants ↔ x ∈ (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker
⊢ A.ρ.invariants = (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
x : (↑A : Type u)
⊢ x ∈ A.ρ.invariants ↔ x ∈ (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).ker

Tactic:
simpa [sub_hom, sub_eq_zero]
    using Representation.mem_invariants_iff_of_forall_mem_zpowers A.ρ g hg _

Premises used: sub_eq_zero, Representation.mem_invariants_iff_of_forall_mem_zpowers, Rep.sub_hom, Rep.ρ
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
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