awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
x : (↑(Functor.obj (𝟭 (Rep.{max (max u v) w, u, v} k ↥S)) A) : Type (max (max u v) w))
⊢ Eq (α := (↑(Functor.obj (coindFunctor k S.subtype ⋙ resFunctor S.subtype) A) : Type (max (max u v) w)))
    (((Hom.hom (NatTrans.app (Adjunction.unit (coindResAdjunction.{w, u, v} k S)) A)).toLinearMap :
          (a : (↑((𝟭 (Rep.{max (max u v) w, u, v} k ↥S)).obj A) : Type (max (max u v) w))) →
            (↑((coindFunctor k S.subtype ⋙ resFunctor S.subtype).obj A) : Type (max (max u v) w)))
        x :
      (↑(Functor.obj (coindFunctor k S.subtype ⋙ resFunctor S.subtype) A) : Type (max (max u v) w)))
    ((IntertwiningMap.toLinearMap
            (Hom.hom
              (NatTrans.app (Adjunction.unit (indResAdjunction.{w, u, v, v} k S.subtype)) A ≫
                CategoryTheory.Functor.map (resFunctor S.subtype) A.indCoindIso.hom)) :
          (a : (↑((𝟭 (Rep.{max (max u v) w, u, v} k ↥S)).obj A) : Type (max (max u v) w))) →
            (↑((coindFunctor k S.subtype ⋙ resFunctor S.subtype).obj A) : Type (max (max u v) w)))
        x :
      (↑(Functor.obj (coindFunctor k S.subtype ⋙ resFunctor S.subtype) A) : Type (max (max u v) w)))

Tactic:
simp [coindResAdjunction, Adjunction.ofNatIsoLeft,
    indResAdjunction, indCoindIso]

Premises used: Rep.indResAdjunction, Rep.coindResAdjunction, Rep.indCoindIso, CategoryTheory.Adjunction.ofNatIsoLeft
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max (max u v) w, u, v} k G
f : coind.{u, v, v, max (max u v) w} S.subtype A ⟶ B
⊢ Eq (α := A ⟶ Functor.obj (resFunctor S.subtype) B)
    ((Adjunction.homEquiv (coindResAdjunction.{w, u, v} k S) A B :
          (a : (coindFunctor k S.subtype).obj A ⟶ B) → A ⟶ (resFunctor S.subtype).obj B)
        f :
      A ⟶ Functor.obj (resFunctor S.subtype) B)
    ((indResHomEquiv.{w, u, v, v} S.subtype A B : (a : ind S.subtype A ⟶ B) → A ⟶ res S.subtype B)
        (A.indCoindIso.hom ≫ f) :
      A ⟶ res S.subtype B)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max (max u v) w, u, v} k G
f : A ⟶ res S.subtype B
simp :
  Eq (α := Functor.obj (coindFunctor k S.subtype) A ⟶ B)
    (NatTrans.app (Iso.inv (indCoindNatIso k S)) A ≫
      ((Adjunction.homEquiv
              (Adjunction.mkOfHomEquiv
                {
                  homEquiv := fun (A : Rep.{max w u v, u, v} k ↥S) (B : Rep.{max w u v, u, v} k G) ↦
                    (indResHomEquiv S.subtype A B).toEquiv,
                  homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ :
                  Adjunction.CoreHomEquiv (C := Rep.{max w u v, u, v} k ↥S) (indFunctor k S.subtype)
                    (resFunctor S.subtype) })
              A B).symm :
          (a : A ⟶ of (MonoidHom.comp B.ρ S.subtype)) → (indFunctor k S.subtype).obj A ⟶ B)
        f)
    (A.indCoindIso.inv ≫
      ((indResHomEquiv.{w, u, v, v} S.subtype A B).symm : (a : A ⟶ res S.subtype B) → ind S.subtype A ⟶ B) f)
⊢ Eq (α := Functor.obj (coindFunctor k S.subtype) A ⟶ B)
    (((Adjunction.homEquiv (coindResAdjunction k S) A B).symm :
          (a : A ⟶ (resFunctor S.subtype).obj B) → (coindFunctor k S.subtype).obj A ⟶ B)
        f :
      Functor.obj (coindFunctor k S.subtype) A ⟶ B)
    (A.indCoindIso.inv ≫
        ((indResHomEquiv.{w, u, v, v} S.subtype A B).symm : (a : A ⟶ res S.subtype B) → ind S.subtype A ⟶ B) f :
      coind.{u, v, v, max u w u v} S.subtype A ⟶ B)

Tactic:
simp only [coindResAdjunction, indResAdjunction,
    Adjunction.homEquiv_ofNatIsoLeft_symm_apply _]

Premises used: Rep.indResAdjunction, Rep.coindResAdjunction, CategoryTheory.Adjunction.homEquiv_ofNatIsoLeft_symm_apply
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max (max u v) w, u, v} k G
f : A ⟶ res S.subtype B
simp :
  Eq (α := ind S.subtype A ⟶ B)
    (((indResHomEquiv S.subtype A B).toEquiv.symm : (a : A ⟶ of (MonoidHom.comp B.ρ S.subtype)) → ind S.subtype A ⟶ B)
        f :
      ind S.subtype A ⟶ B)
    (ofHom
        {
          toLinearMap :=
            Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)
              (TensorProduct.lift
                ((Finsupp.lift ((↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) k G :
                    (a : G → (↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) →
                      (G →₀ k) →ₗ[k] (↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w)))
                  fun (h : G) ↦
                  (B.ρ : (a : G) → (↑B : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) h⁻¹ ∘ₗ
                    (Hom.hom f).toLinearMap))
              ⋯,
          isIntertwining' := ⋯ } :
      of (Representation.ind S.subtype A.ρ) ⟶ of B.ρ)
⊢ Eq (α := Functor.obj (coindFunctor k S.subtype) A ⟶ B)
    (NatTrans.app (Iso.inv (indCoindNatIso k S)) A ≫
      ((Adjunction.homEquiv
              (Adjunction.mkOfHomEquiv
                {
                  homEquiv := fun (A : Rep.{max w u v, u, v} k ↥S) (B : Rep.{max w u v, u, v} k G) ↦
                    (indResHomEquiv S.subtype A B).toEquiv,
                  homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ :
                  Adjunction.CoreHomEquiv (C := Rep.{max w u v, u, v} k ↥S) (indFunctor k S.subtype)
                    (resFunctor S.subtype) })
              A B).symm :
          (a : A ⟶ of (MonoidHom.comp B.ρ S.subtype)) → (indFunctor k S.subtype).obj A ⟶ B)
        f)
    (A.indCoindIso.inv ≫
      ((indResHomEquiv.{w, u, v, v} S.subtype A B).symm : (a : A ⟶ res S.subtype B) → ind S.subtype A ⟶ B) f)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max (max u v) w, u, v} k G
f : A ⟶ res S.subtype B
⊢ Eq (α := ind S.subtype A ⟶ B)
    (((indResHomEquiv S.subtype A B).toEquiv.symm : (a : A ⟶ of (MonoidHom.comp B.ρ S.subtype)) → ind S.subtype A ⟶ B)
        f :
      ind S.subtype A ⟶ B)
    (ofHom
        {
          toLinearMap :=
            Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)
              (TensorProduct.lift
                ((Finsupp.lift ((↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) k G :
                    (a : G → (↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) →
                      (G →₀ k) →ₗ[k] (↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w)))
                  fun (h : G) ↦
                  (B.ρ : (a : G) → (↑B : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) h⁻¹ ∘ₗ
                    (Hom.hom f).toLinearMap))
              ⋯,
          isIntertwining' := ⋯ } :
      of (Representation.ind S.subtype A.ρ) ⟶ of B.ρ)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
⊢ Coinvariants.ker ρ =
    (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range

Tactic:
le_antisymm (Submodule.span_le.2 ?_) ?_

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
refine_1 :
  (Set.range fun (gv : G × V) ↦
      HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2) ⊆
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
refine_2 :
  (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range ≤
    Coinvariants.ker ρ
⊢ Coinvariants.ker ρ =
    (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range

Tactic:
refine le_antisymm (Submodule.span_le.2 ?_) ?_

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
γ : G
α : V
refine_1 :
  ∀ (i : ℕ),
    (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
        ((fun (x : ℕ) ↦ g ^ x) i, α) ∈
      (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
        Set V)
⊢ (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      (γ, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)

Tactic:
rcases mem_powers_iff_mem_zpowers.2 (hg γ) with ⟨i, rfl⟩

Premises used: Iff.mpr, mem_powers_iff_mem_zpowers, rfl
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
α : V
⊢ Eq (α := V)
    ((HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
        0 :
      V)
    ((fun (gv : G × V) ↦
          HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
        ((fun (x : ℕ) ↦ g ^ x) 0, α) :
      V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
α : V
⊢ (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) 0, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
α : V
n : ℕ
h_1 :
  (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) n, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
h :
  Eq (α := V)
    ((HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
        (Fin.partialSum (n := n + 1)
          (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) α)
          (Fin.last (n + 1))) :
      V)
    ((fun (gv : G × V) ↦
          HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
        ((fun (x : ℕ) ↦ g ^ x) (n + 1), α) :
      V)
⊢ (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) (n + 1), α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)

Tactic:
use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))

Premises used: Fin.val, HPow.hPow, Fin.last, DFunLike.coe, Fin.partialSum
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
α : V
n : ℕ
h :
  (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) n, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
⊢ Eq (α := V)
    ((HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
        (Fin.partialSum (n := n + 1)
          (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) α)
          (Fin.last (n + 1))) :
      V)
    ((fun (gv : G × V) ↦
          HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
        ((fun (x : ℕ) ↦ g ^ x) (n + 1), α) :
      V)

Tactic:
simpa using ρ.apply_sub_id_partialSum_eq _ _ _

Premises used: Representation.apply_sub_id_partialSum_eq
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
α : V
i : ℕ
refine_1 :
  (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) 0, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
refine_1₁ :
  ∀ (n : ℕ),
    (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
          ((fun (x : ℕ) ↦ g ^ x) n, α) ∈
        (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
          Set V) →
      (fun (gv : G × V) ↦
            HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
          ((fun (x : ℕ) ↦ g ^ x) (n + 1), α) ∈
        (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
          Set V)
⊢ (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) i, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)

Tactic:
induction i with | zero => exact ⟨0, by simp⟩ | succ n _ =>
    use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
    simpa using ρ.apply_sub_id_partialSum_eq _ _ _

Premises used: Representation.apply_sub_id_partialSum_eq
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
y : V
⊢ Membership.mem (α := V) (Coinvariants.ker ρ)
    ((HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
        y :
      V)

Tactic:
simpa using Coinvariants.sub_mem_ker g y

Premises used: Representation.Coinvariants.sub_mem_ker
-- 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
have :
  ∀ (this : Fintype G),
    Eq (α := Submodule k (G →₀ k))
      (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
      (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1) : Submodule k (G →₀ k))
⊢ Eq (α := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
    (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1) : Submodule k (G →₀ k))

Tactic:
have := Fintype.ofFinite G
-- 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 : Fintype G
⊢ Eq (α := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
    (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1) : Submodule k (G →₀ k))

Tactic:
le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- 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 : Fintype G
refine_1 :
  (Set.range fun (gv : G × (G →₀ k)) ↦
      HSub.hSub (α := G →₀ k)
        ((((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) gv.1 : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k)
            gv.2 :
          G →₀ k)
        gv.2) ⊆
    (↑(LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) : Set (G →₀ k))
refine_2 :
  ∀ (x : G →₀ k)
    (hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x),
    Membership.mem (γ := Submodule k (G →₀ k))
      (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k)) x
⊢ Eq (α := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
    (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1) : Submodule k (G →₀ k))

Tactic:
refine le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- 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 : Fintype G
g : G
y : G →₀ k
⊢ ∀ (i : G), Membership.mem (γ := Finset G) Finset.univ i ↔ Membership.mem (γ := Finset G) Finset.univ (g⁻¹ * i)

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 : Fintype G
g : G
y : G →₀ k
⊢ ∀ (i : G),
    Membership.mem (γ := Finset G) Finset.univ i →
      Eq.{u_1 + 1} (α := k) ((y : (a : G) → k) (g⁻¹ * i) : k) ((y : (a : G) → k) (g⁻¹ * i) : k)

Tactic:
lia
-- 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 : Fintype G
g : G
y : G →₀ k
⊢ (fun (gv : G × (G →₀ k)) ↦
        HSub.hSub (α := G →₀ k)
          ((((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) gv.1 : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k)
              gv.2 :
            G →₀ k)
          gv.2)
      (g, y) ∈
    (↑(LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) : Set (G →₀ k))

Tactic:
simpa [linearCombination, sub_eq_zero, sum_fintype]
      using Finset.sum_bijective _ (Group.mulLeft_bijective g⁻¹) (by simp) (by lia)

Premises used: sub_eq_zero, Finsupp.sum_fintype, Group.mulLeft_bijective, Inv.inv, Finset.sum_bijective, Finsupp.linearCombination
-- 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 : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
h :
  ∀ (g : G),
    Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
      ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
⊢ x = x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r)

Tactic:
ext g
-- 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 : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
g : G
pos :
  ∀ (hg : g = 1),
    Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
      ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
neg :
  ∀ (hg : ¬g = 1),
    Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
      ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
    ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)

Tactic:
by_cases hg : g = 1
-- 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 : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
g : G
hg : g = 1
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
    ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)

Tactic:
simp_all [linearCombination, sum_apply']

Premises used: Finsupp.sum_apply', Finsupp.linearCombination
-- 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 : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
g : G
hg : ¬g = 1
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
    ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)

Tactic:
simp_all [sum_apply']

Premises used: Finsupp.sum_apply'
-- 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 : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
⊢ x = x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r)

Tactic:
have : x = x.sum (fun g r => single g r - single 1 r) := by
      ext g
      by_cases hg : g = 1
      · simp_all [linearCombination, sum_apply']
      · simp_all [sum_apply']
-- 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)
refine_2 :
  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))
⊢ Membership.mem (γ := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k)) x

Tactic:
rw [this]