awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this_1 : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
this : x = x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r)
g : G
h : Ne.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k) (0 : k)
⊢ HSub.hSub (α := G →₀ k) (β := G →₀ k)
      ((((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k)
          (single 1 ((x : (a : G) → k) g)) :
        G →₀ k)
      (single 1 ((x : (a : G) → k) g) : G →₀ k) =
    HSub.hSub (α := G →₀ k) (β := G →₀ k) (single g ((x : (a : G) → k) g) : G →₀ k)
      (single 1 ((x : (a : G) → k) g) : G →₀ k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this_1 : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
this : x = x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r)
⊢ Membership.mem (γ := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
    (x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r))

Tactic:
exact Submodule.finsuppSum_mem _ _ _ _ fun g _ =>
      Coinvariants.mem_ker_of_eq g (single 1 (x g)) _ (by simp)

Premises used: Representation.Coinvariants.mem_ker_of_eq, Submodule.finsuppSum_mem, OfNat.ofNat, DFunLike.coe, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : (↑(leftRegular k G) : Type u)
h_1 :
  Membership.mem (γ := Submodule k (↑(leftRegular k G) : Type u))
    (LinearMap.range (IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))))) x
w : (↑(leftRegular k G) : Type u)
h :
  (IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))) :
        (a : (↑(leftRegular k G) : Type u)) → (↑(leftRegular k G) : Type u))
      w =
    x
⊢ x ∈
    (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).ker

Tactic:
simp [sub_hom, applyAsHom_apply _, ← h, norm]

Premises used: Rep.norm, Rep.sub_hom, Rep.applyAsHom_apply
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : (↑(leftRegular k G) : Type u)
hx :
  x ∈
    (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).ker
h :
  ∀ (a : G),
    Eq (α := k)
      ((((IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))) :
                  (a : (↑(leftRegular k G) : Type u)) → (↑(leftRegular k G) : Type u))
                (single 1 ((x : (a : G) → k) g)) :
              (↑(leftRegular k G) : Type u)) :
            (a : G) → k)
          a :
        k)
      ((x : (a : G) → k) a : k)
⊢ (IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))) :
        (a : (↑(leftRegular k G) : Type u)) → (↑(leftRegular k G) : Type u))
      (single 1 ((x : (a : G) → k) g)) =
    x

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : (↑(leftRegular k G) : Type u)
hx :
  x ∈
    (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).ker
a : G
⊢ (((Representation.leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g : (G →₀ k) →ₗ[k] G →₀ k) :
        (a : G →₀ k) → G →₀ k)
      x =
    x

Tactic:
simpa [sub_hom, sub_eq_zero] using hx

Premises used: sub_eq_zero, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : (↑(leftRegular k G) : Type u)
hx :
  x ∈
    (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).ker
a : G
⊢ ∀ (γ : G), Eq (α := k) ((x : (a : G) → k) γ : k) ((x : (a : G) → k) g : k)

Tactic:
have := apply_eq_of_leftRegular_eq_of_generator (k := k) g hg x
      (by simpa [sub_hom, sub_eq_zero] using hx)
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : (↑(leftRegular k G) : Type u)
hx :
  x ∈
    (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).ker
a : G
this : ∀ (γ : G), Eq (α := k) ((x : (a : G) → k) γ : k) ((x : (a : G) → k) g : k)
⊢ Eq (α := k)
    ((((IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))) :
                (a : (↑(leftRegular k G) : Type u)) → (↑(leftRegular k G) : Type u))
              (single 1 ((x : (a : G) → k) g)) :
            (↑(leftRegular k G) : Type u)) :
          (a : G) → k)
        a :
      k)
    ((x : (a : G) → k) a : k)

Tactic:
simp [norm, Representation.norm, this]

Premises used: Rep.norm, Representation.norm
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
g : G
inst_2 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).range =
    LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)

Tactic:
simp [sub_hom, applyAsHom, FiniteCyclicGroup.coinvariantsKer_eq_range
    (Representation.leftRegular k G) _ hg,
    ← FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker]

Premises used: Representation.FiniteCyclicGroup.coinvariantsKer_eq_range, Rep.applyAsHom, Rep.sub_hom, Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker, Representation.leftRegular
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).range =
    LinearMap.ker (IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))))

Tactic:
simp [norm, ker_leftRegular_norm_eq, range_applyAsHom_sub_eq_ker_linearCombination k g hg]

Premises used: Rep.norm, Representation.ker_leftRegular_norm_eq, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A_1 : Rep k G
g : G
A : Rep.{u_1, u, u} k G
hf :
  ∀ (x : (↑A : Type u_1)),
    Eq (α := (↑A : Type u_1))
      (((Hom.hom
                (A.norm ≫
                  HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A)
                    (𝟙 A))).toLinearMap :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          x :
        (↑A : Type u_1))
      ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) : (a : (↑A : Type u_1)) → (↑A : Type u_1)) x :
        (↑A : Type u_1))
⊢ A.norm ≫ HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A) = 0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A_1 : Rep k G
g : G
A : Rep.{u_1, u, u} k G
x : (↑A : Type u_1)
⊢ Eq (α := (↑A : Type u_1))
    (((Hom.hom
              (A.norm ≫
                HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A))).toLinearMap :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        x :
      (↑A : Type u_1))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) : (a : (↑A : Type u_1)) → (↑A : Type u_1)) x :
      (↑A : Type u_1))

Tactic:
simp [sub_hom, applyAsHom, norm]

Premises used: Rep.norm, Rep.applyAsHom, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A_1 : Rep k G
g : G
A : Rep.{u_1, u, u} k G
hf :
  ∀ (x : (↑A : Type u_1)),
    Eq (α := (↑A : Type u_1))
      (((Hom.hom
                (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A) ≫
                  A.norm)).toLinearMap :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          x :
        (↑A : Type u_1))
      ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) : (a : (↑A : Type u_1)) → (↑A : Type u_1)) x :
        (↑A : Type u_1))
⊢ HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A) ≫ A.norm = 0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A_1 : Rep k G
g : G
A : Rep.{u_1, u, u} k G
x : (↑A : Type u_1)
⊢ Eq (α := (↑A : Type u_1))
    (((Hom.hom
              (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A) ≫
                A.norm)).toLinearMap :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        x :
      (↑A : Type u_1))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) : (a : (↑A : Type u_1)) → (↑A : Type u_1)) x :
      (↑A : Type u_1))

Tactic:
simp [sub_hom, norm, applyAsHom]

Premises used: Rep.norm, Rep.applyAsHom, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
X Y : Rep.{u_1, u, u} k G
f : X ⟶ Y
j : ℕ
pos :
  ∀ (hj : Even (j + 1)),
    Eq (α :=
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯)
          (j + 1) ⟶
        HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) j)
      (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) (j + 1) j)
      (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯) (j + 1) j ≫ f)
neg :
  ∀ (hj : ¬Even (j + 1)),
    Eq (α :=
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯)
          (j + 1) ⟶
        HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) j)
      (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) (j + 1) j)
      (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯) (j + 1) j ≫ f)
⊢ Eq (α :=
    HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯)
        (j + 1) ⟶
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) (j + 1) j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯) (j + 1) j ≫ f)

Tactic:
by_cases hj : Even (j + 1)

Premises used: HAdd.hAdd, Even, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
X Y : Rep.{u_1, u, u} k G
f : X ⟶ Y
j : ℕ
hj : Even (j + 1)
⊢ Eq (α :=
    HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯)
        (j + 1) ⟶
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) (j + 1) j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯) (j + 1) j ≫ f)

Tactic:
simp [if_pos hj, norm_comm]

Premises used: if_pos, Rep.norm_comm
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
X Y : Rep.{u_1, u, u} k G
f : X ⟶ Y
j : ℕ
hj : ¬Even (j + 1)
⊢ Eq (α :=
    HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯)
        (j + 1) ⟶
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) (j + 1) j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯) (j + 1) j ≫ f)

Tactic:
simp [if_neg hj, applyAsHom_comm]

Premises used: Rep.applyAsHom_comm, if_neg
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep.{u_1, u, u} k G
g : G
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
                ModuleCat.ofHom
                  (Hom.hom
                      (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A)
                        (𝟙 A))).toLinearMap) :
            (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
          x :
        (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
      ((ModuleCat.Hom.hom 0 :
            (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
          x :
        (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
      ModuleCat.ofHom
        (Hom.hom
            (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A))).toLinearMap =
    0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep.{u_1, u, u} k G
g : G
x : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
              ModuleCat.ofHom
                (Hom.hom
                    (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A)
                      (𝟙 A))).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
        x :
      (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
        x :
      (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))

Tactic:
simp [sub_hom, applyAsHom, norm]

Premises used: Rep.norm, Rep.applyAsHom, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep.{u_1, u, u} k G
g : G
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom
                  (Hom.hom
                      (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A)
                        (𝟙 A))).toLinearMap ≫
                ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
            (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
          x :
        (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
      ((ModuleCat.Hom.hom 0 :
            (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
          x :
        (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
⊢ ModuleCat.ofHom
        (Hom.hom
            (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A))).toLinearMap ≫
      ModuleCat.ofHom (Hom.hom A.norm).toLinearMap =
    0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep.{u_1, u, u} k G
g : G
x : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                (Hom.hom
                    (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A)
                      (𝟙 A))).toLinearMap ≫
              ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
        x :
      (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
        x :
      (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))

Tactic:
simp [sub_hom, applyAsHom, norm]

Premises used: Rep.norm, Rep.applyAsHom, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g_1 g : G
⊢ Eq (α := (↑(trivial k G k) : Type u))
    ((leftRegularHomEquiv (trivial k G k) : (a : leftRegular k G ⟶ trivial k G k) → (↑(trivial k G k) : Type u))
        (CategoryStruct.comp (Y := HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 0)
            (HomologicalComplex.d (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1 0)
            (leftRegularHom (trivial k G k) 1) :
          Quiver.Hom (V := Rep k G) (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1)
            (trivial k G k)) :
      (↑(trivial k G k) : Type u))
    ((leftRegularHomEquiv (trivial k G k) : (a : leftRegular k G ⟶ trivial k G k) → (↑(trivial k G k) : Type u)) 0 :
      (↑(trivial k G k) : Type u))

Tactic:
simp [homEquiv, sub_hom, applyAsHom]

Premises used: Rep.homEquiv, Rep.applyAsHom, Rep.sub_hom
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x :
  (↑(ShortComplex.X₂
        (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (ChainComplex.single₀ (Rep k G)) (trivial k G k)))) :
    Type u)
⊢ (Hom.hom
          (ShortComplex.Hom.τ₂
            (CategoryTheory.Functor.map (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
              ((Equiv.symm
                    (ChainComplex.toSingle₀Equiv (Functor.obj (chainComplexFunctor k g) (leftRegular k G))
                      (trivial k G k)) :
                  (a :
                      { f : ((chainComplexFunctor k g).obj (leftRegular k G)).X 0 ⟶ trivial k G k //
                        ((chainComplexFunctor k g).obj (leftRegular k G)).d 1 0 ≫ f = 0 }) →
                    (chainComplexFunctor k g).obj (leftRegular k G) ⟶
                      (ChainComplex.single₀ (Rep k G)).obj (trivial k G k))
                (Subtype.mk (p :=
                    fun
                      (f :
                        Quiver.Hom (V := Rep k G)
                          (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 0)
                          (trivial k G k)) ↦
                    Eq (α :=
                      Quiver.Hom (V := Rep k G)
                        (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1)
                        (trivial k G k))
                      (HomologicalComplex.d (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1 0 ≫ f) 0)
                    (leftRegularHom (trivial k G k) 1) ⋯ :
                  { f :
                    Quiver.Hom (V := Rep k G)
                      (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 0)
                      (trivial k G k) //
                    Eq (α :=
                      Quiver.Hom (V := Rep k G)
                        (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1)
                        (trivial k G k))
                      (HomologicalComplex.d (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1 0 ≫ f) 0 })))) :
        (a :
            (↑((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                    ((chainComplexFunctor k g).obj (leftRegular k G))).X₂ :
              Type u)) →
          (↑((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                  ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂ :
            Type u))
      (single 1 x) =
    x

Tactic:
simp [ChainComplex.toSingle₀Equiv]

Premises used: ChainComplex.toSingle₀Equiv
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
⊢ (ComplexShape.down ℕ).prev (m + 1) = m + 2

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
⊢ (ComplexShape.down ℕ).next (m + 1) = m

Tactic:
simp