awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_12 : S.Normal
g : ↥S
x : V
⊢ Eq (α := Coinvariants (MonoidHom.comp ρ S.subtype))
    (((MonoidHom.comp (ρ.toCoinvariants S) S.subtype :
                (a : ↥S) → Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
              g ∘ₗ
            mk (MonoidHom.comp ρ S.subtype) :
          (a : V) → Coinvariants (MonoidHom.comp ρ S.subtype))
        x :
      Coinvariants (MonoidHom.comp ρ S.subtype))
    ((LinearMap.id ∘ₗ mk (MonoidHom.comp ρ S.subtype) : (a : V) → Coinvariants (MonoidHom.comp ρ S.subtype)) x :
      Coinvariants (MonoidHom.comp ρ S.subtype))

Tactic:
(Coinvariants.mk_eq_iff _).2 <| mem_ker_of_eq g x _ rfl

Premises used: Iff.mpr, Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Representation.Coinvariants.mk_eq_iff, Representation.Coinvariants.mem_ker_of_eq, rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_12 : S.Normal
g : ↥S
x : V
⊢ Eq (α := Coinvariants (MonoidHom.comp ρ S.subtype))
    (((MonoidHom.comp (ρ.toCoinvariants S) S.subtype :
                (a : ↥S) → Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
              g ∘ₗ
            mk (MonoidHom.comp ρ S.subtype) :
          (a : V) → Coinvariants (MonoidHom.comp ρ S.subtype))
        x :
      Coinvariants (MonoidHom.comp ρ S.subtype))
    ((LinearMap.id ∘ₗ mk (MonoidHom.comp ρ S.subtype) : (a : V) → Coinvariants (MonoidHom.comp ρ S.subtype)) x :
      Coinvariants (MonoidHom.comp ρ S.subtype))

Tactic:
exact (Coinvariants.mk_eq_iff _).2 <| mem_ker_of_eq g x _ rfl

Premises used: Iff.mpr, Representation.Coinvariants.mk_eq_iff, Representation.Coinvariants.mem_ker_of_eq, rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
x : G
h :
  ∀ (a : α) (x_1 : V) (a_1 : α),
    Eq.{u_8 + 1} (α := ρ.Coinvariants)
      (((((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α : (a : G) → (α →₀ V) →ₗ[k] α →₀ V) x) ∘ₗ lsingle a :
                  (a : V) → α →₀ ρ.Coinvariants)
                x_1 :
              Finsupp.{u_9, u_8} α ρ.Coinvariants) :
            (a : α) → ρ.Coinvariants)
          a_1 :
        ρ.Coinvariants)
      ((((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ lsingle a : (a : V) → α →₀ ρ.Coinvariants) x_1 :
              Finsupp.{u_9, u_8} α ρ.Coinvariants) :
            (a : α) → ρ.Coinvariants)
          a_1 :
        ρ.Coinvariants)
⊢ Eq (α := (α →₀ V) →ₗ[k] Finsupp.{u_9, u_8} α ρ.Coinvariants)
    (mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α : (a : G) → (α →₀ V) →ₗ[k] α →₀ V) x)
    (mapRange.linearMap (Coinvariants.mk ρ))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
x : G
a : α
x_1 : V
a_1 : α
⊢ Eq.{u_8 + 1} (α := ρ.Coinvariants)
    (((((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α : (a : G) → (α →₀ V) →ₗ[k] α →₀ V) x) ∘ₗ lsingle a :
                (a : V) → α →₀ ρ.Coinvariants)
              x_1 :
            Finsupp.{u_9, u_8} α ρ.Coinvariants) :
          (a : α) → ρ.Coinvariants)
        a_1 :
      ρ.Coinvariants)
    ((((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ lsingle a : (a : V) → α →₀ ρ.Coinvariants) x_1 :
            Finsupp.{u_9, u_8} α ρ.Coinvariants) :
          (a : α) → ρ.Coinvariants)
        a_1 :
      ρ.Coinvariants)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_6
G : Type u_7
V : Type u_8
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
α : Type u_9
x : α
a : V
⊢ Eq (α := Finsupp.{u_9, u_8} α ρ.Coinvariants)
    ((ρ.coinvariantsToFinsupp α : (a : (ρ.finsupp α).Coinvariants) → α →₀ ρ.Coinvariants)
        ((Coinvariants.mk (ρ.finsupp α) : (a : α →₀ V) → (ρ.finsupp α).Coinvariants) (single x a)) :
      Finsupp.{u_9, u_8} α ρ.Coinvariants)
    (single x ((Coinvariants.mk ρ : (a : V) → ρ.Coinvariants) a) : Finsupp.{u_9, u_8} α ρ.Coinvariants)

Tactic:
simp [coinvariantsToFinsupp]

Premises used: Representation.coinvariantsToFinsupp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
a : α
g : G
x : V
⊢ HSub.hSub (α := α →₀ V) (β := α →₀ V)
      ((((ρ.finsupp α : (a : G) → (α →₀ V) →ₗ[k] α →₀ V) g : (α →₀ V) →ₗ[k] α →₀ V) : (a : α →₀ V) → α →₀ V)
          (single a x) :
        α →₀ V)
      (single a x) =
    HSub.hSub (α := α →₀ V) (β := α →₀ V)
      ((lsingle a : (a : V) → α →₀ V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x) : α →₀ V)
      ((lsingle a : (a : V) → α →₀ V) x : α →₀ V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_6
G : Type u_7
V : Type u_8
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
α : Type u_9
a : α
x : V
⊢ Eq (α := (ρ.finsupp α).Coinvariants)
    ((ρ.finsuppToCoinvariants α : (a : α →₀ ρ.Coinvariants) → (ρ.finsupp α).Coinvariants)
        (single a ((Coinvariants.mk ρ : (a : V) → ρ.Coinvariants) x)) :
      (ρ.finsupp α).Coinvariants)
    ((Coinvariants.mk (ρ.finsupp α) : (a : α →₀ V) → (ρ.finsupp α).Coinvariants) (single a x) :
      (ρ.finsupp α).Coinvariants)

Tactic:
simp [finsuppToCoinvariants]

Premises used: Representation.finsuppToCoinvariants
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
h :
  ∀ (a : α) (x : V) (a_1 : α),
    Eq.{u_8 + 1} (α := ρ.Coinvariants)
      ((((((ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α) ∘ₗ lsingle a) ∘ₗ Coinvariants.mk ρ :
                  (a : V) → α →₀ ρ.Coinvariants)
                x :
              Finsupp.{u_9, u_8} α ρ.Coinvariants) :
            (a : α) → ρ.Coinvariants)
          a_1 :
        ρ.Coinvariants)
      (((((LinearMap.id ∘ₗ lsingle a) ∘ₗ Coinvariants.mk ρ : (a : V) → α →₀ ρ.Coinvariants) x :
              Finsupp.{u_9, u_8} α ρ.Coinvariants) :
            (a : α) → ρ.Coinvariants)
          a_1 :
        ρ.Coinvariants)
⊢ ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α = LinearMap.id

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
a : α
x : V
a_1 : α
⊢ Eq.{u_8 + 1} (α := ρ.Coinvariants)
    ((((((ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α) ∘ₗ lsingle a) ∘ₗ Coinvariants.mk ρ :
                (a : V) → α →₀ ρ.Coinvariants)
              x :
            Finsupp.{u_9, u_8} α ρ.Coinvariants) :
          (a : α) → ρ.Coinvariants)
        a_1 :
      ρ.Coinvariants)
    (((((LinearMap.id ∘ₗ lsingle a) ∘ₗ Coinvariants.mk ρ : (a : V) → α →₀ ρ.Coinvariants) x :
            Finsupp.{u_9, u_8} α ρ.Coinvariants) :
          (a : α) → ρ.Coinvariants)
        a_1 :
      ρ.Coinvariants)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
H :
  ∀ (a : α) (x : V),
    Eq (α := (ρ.finsupp α).Coinvariants)
      ((((ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α) ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a :
            (a : V) → (ρ.finsupp α).Coinvariants)
          x :
        (ρ.finsupp α).Coinvariants)
      (((LinearMap.id ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a : (a : V) → (ρ.finsupp α).Coinvariants) x :
        (ρ.finsupp α).Coinvariants)
⊢ ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α = LinearMap.id

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
a : α
x : V
⊢ Eq (α := (ρ.finsupp α).Coinvariants)
    ((((ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α) ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a :
          (a : V) → (ρ.finsupp α).Coinvariants)
        x :
      (ρ.finsupp α).Coinvariants)
    (((LinearMap.id ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a : (a : V) → (ρ.finsupp α).Coinvariants) x :
      (ρ.finsupp α).Coinvariants)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_6
G : Type u_7
V : Type u_8
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
α : Type u_9
x : (ρ.finsupp α).Coinvariants
⊢ Eq (α := Finsupp.{u_9, u_8} α ρ.Coinvariants)
    ((ρ.coinvariantsFinsuppLEquiv α : (a : (ρ.finsupp α).Coinvariants) → α →₀ ρ.Coinvariants) x :
      Finsupp.{u_9, u_8} α ρ.Coinvariants)
    ((ρ.coinvariantsToFinsupp α : (a : (ρ.finsupp α).Coinvariants) → α →₀ ρ.Coinvariants) x :
      Finsupp.{u_9, u_8} α ρ.Coinvariants)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
τ : Representation k G W
x : V
y : W
g : G
⊢ HSub.hSub (α := TensorProduct k V W) (β := TensorProduct k V W)
      ((((ρ.tprod τ : (a : G) → TensorProduct k V W →ₗ[k] TensorProduct k V W) g⁻¹ :
              TensorProduct k V W →ₗ[k] TensorProduct k V W) :
            (a : TensorProduct k V W) → TensorProduct k V W)
          (x ⊗ₜ[k] (((τ : (a : G) → W →ₗ[k] W) g : W →ₗ[k] W) : (a : W) → W) y) :
        TensorProduct k V W)
      (x ⊗ₜ[k] (((τ : (a : G) → W →ₗ[k] W) g : W →ₗ[k] W) : (a : W) → W) y : TensorProduct k V W) =
    HSub.hSub (α := TensorProduct k V W) (β := TensorProduct k V W)
      ((((ρ : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y : TensorProduct k V W)
      (x ⊗ₜ[k] (((τ : (a : G) → W →ₗ[k] W) g : W →ₗ[k] W) : (a : W) → W) y : TensorProduct k V W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
τ : Representation k G W
x : V
y : W
g : G
⊢ HSub.hSub (α := TensorProduct k V W) (β := TensorProduct k V W)
      ((((ρ.tprod τ : (a : G) → TensorProduct k V W →ₗ[k] TensorProduct k V W) g⁻¹ :
              TensorProduct k V W →ₗ[k] TensorProduct k V W) :
            (a : TensorProduct k V W) → TensorProduct k V W)
          ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y) :
        TensorProduct k V W)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y : TensorProduct k V W) =
    HSub.hSub (α := TensorProduct k V W) (β := TensorProduct k V W)
      (x ⊗ₜ[k] (((τ : (a : G) → W →ₗ[k] W) g⁻¹ : W →ₗ[k] W) : (a : W) → W) y : TensorProduct k V W)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y : TensorProduct k V W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module k_1 W_1
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ_1 : Representation k_1 G_1 W_1
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
inst_12 : AddCommGroup W
inst_13 : Module k W
ρ : Representation k G V
τ : Representation k G W
x : G
a :
  ∀ (x_1 : V) (a : G),
    Eq.{u_8 + 1} (α := V)
      ((((TensorProduct.AlgebraTensorModule.curry
                      ((TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
                          (↑(_root_.TensorProduct.comm k V (G →₀ k)) :
                            TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V)) ∘ₗ
                        (ρ.tprod (leftRegular k G) :
                            (a : G) → TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k V (G →₀ k))
                          x) :
                    V →ₗ[k] (G →₀ k) →ₗ[k] V) :
                  (a : V) → (G →₀ k) →ₗ[k] V)
                x_1 ∘ₗ
              lsingle a :
            (a : k) → V)
          1 :
        V)
      ((((TensorProduct.AlgebraTensorModule.curry
                      (TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
                        (↑(_root_.TensorProduct.comm k V (G →₀ k)) :
                          TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V)) :
                    V →ₗ[k] (G →₀ k) →ₗ[k] V) :
                  (a : V) → (G →₀ k) →ₗ[k] V)
                x_1 ∘ₗ
              lsingle a :
            (a : k) → V)
          1 :
        V)
⊢ Eq (α := TensorProduct k V (G →₀ k) →ₗ[k] V)
    ((TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
        (↑(_root_.TensorProduct.comm k V (G →₀ k)) : TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V)) ∘ₗ
      (ρ.tprod (leftRegular k G) : (a : G) → TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k V (G →₀ k)) x)
    (TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
      (↑(_root_.TensorProduct.comm k V (G →₀ k)) : TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module k_1 W_1
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ_1 : Representation k_1 G_1 W_1
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
inst_12 : AddCommGroup W
inst_13 : Module k W
ρ : Representation k G V
τ : Representation k G W
x : G
x_1 : V
a : G
⊢ Eq.{u_8 + 1} (α := V)
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
                        (↑(_root_.TensorProduct.comm k V (G →₀ k)) :
                          TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V)) ∘ₗ
                      (ρ.tprod (leftRegular k G) :
                          (a : G) → TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k V (G →₀ k))
                        x) :
                  V →ₗ[k] (G →₀ k) →ₗ[k] V) :
                (a : V) → (G →₀ k) →ₗ[k] V)
              x_1 ∘ₗ
            lsingle a :
          (a : k) → V)
        1 :
      V)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
                      (↑(_root_.TensorProduct.comm k V (G →₀ k)) :
                        TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V)) :
                  V →ₗ[k] (G →₀ k) →ₗ[k] V) :
                (a : V) → (G →₀ k) →ₗ[k] V)
              x_1 ∘ₗ
            lsingle a :
          (a : k) → V)
        1 :
      V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_6
G : Type u_7
V : Type u_8
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
x : V
g : G
r : k
⊢ (ρ.ofCoinvariantsTprodLeftRegular : (a : (ρ.tprod (leftRegular k G)).Coinvariants) → V)
      ((Coinvariants.mk (ρ.tprod (leftRegular k G)) :
            (a : TensorProduct k V (G →₀ k)) → (ρ.tprod (leftRegular k G)).Coinvariants)
          (x ⊗ₜ[k] single g r) :
        (ρ.tprod (leftRegular k G)).Coinvariants) =
    HSMul.hSMul (β := V) r ((((ρ : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] V) : (a : V) → V) x : V)

Tactic:
congr($(Finsupp.linearCombination_single k (v := fun g => ρ g⁻¹) r g) x)

Premises used: congrArg, id, Finsupp.linearCombination_single, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module k_1 W_1
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ_1 : Representation k_1 G_1 W_1
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
inst_12 : AddCommGroup W
inst_13 : Module k W
ρ : Representation k G V
τ : Representation k G W
h :
  ∀ (x : V),
    Eq (α := V)
      ((ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
              Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
                (LinearMap.flip (TensorProduct.mk k V (G →₀ k)) : (a : G →₀ k) → V →ₗ[k] TensorProduct k V (G →₀ k))
                  (single 1 1) :
            (a : V) → V)
          x :
        V)
      ((LinearMap.id : (a : V) → V) x : V)
⊢ ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
      Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
        (LinearMap.flip (TensorProduct.mk k V (G →₀ k)) : (a : G →₀ k) → V →ₗ[k] TensorProduct k V (G →₀ k))
          (single 1 1) =
    LinearMap.id

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module k_1 W_1
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ_1 : Representation k_1 G_1 W_1
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
inst_12 : AddCommGroup W
inst_13 : Module k W
ρ : Representation k G V
τ : Representation k G W
x : V
⊢ Eq (α := V)
    ((ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
            Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
              (LinearMap.flip (TensorProduct.mk k V (G →₀ k)) : (a : G →₀ k) → V →ₗ[k] TensorProduct k V (G →₀ k))
                (single 1 1) :
          (a : V) → V)
        x :
      V)
    ((LinearMap.id : (a : V) → V) x : V)

Tactic:
simp