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_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) (a : G),
    Eq (α := (ρ.tprod (leftRegular k G)).Coinvariants)
      ((((TensorProduct.AlgebraTensorModule.curry
                    (((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)) ∘ₗ
                        ρ.ofCoinvariantsTprodLeftRegular) ∘ₗ
                      Coinvariants.mk (ρ.tprod (leftRegular k G))) :
                  V →ₗ[k] (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants) :
                (a : V) → (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants)
              x ∘ₗ
            lsingle a :
          (a : k) → (ρ.tprod (leftRegular k G)).Coinvariants)
        1)
      ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.id ∘ₗ Coinvariants.mk (ρ.tprod (leftRegular k G))) :
                  V →ₗ[k] (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants) :
                (a : V) → (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants)
              x ∘ₗ
            lsingle a :
          (a : k) → (ρ.tprod (leftRegular k G)).Coinvariants)
        1)
⊢ (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)) ∘ₗ
      ρ.ofCoinvariantsTprodLeftRegular =
    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
a : G
⊢ Eq (α := (ρ.tprod (leftRegular k G)).Coinvariants)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (((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)) ∘ₗ
                      ρ.ofCoinvariantsTprodLeftRegular) ∘ₗ
                    Coinvariants.mk (ρ.tprod (leftRegular k G))) :
                V →ₗ[k] (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants) :
              (a : V) → (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants)
            x ∘ₗ
          lsingle a :
        (a : k) → (ρ.tprod (leftRegular k G)).Coinvariants)
      1)
    ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.id ∘ₗ Coinvariants.mk (ρ.tprod (leftRegular k G))) :
                V →ₗ[k] (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants) :
              (a : V) → (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants)
            x ∘ₗ
          lsingle a :
        (a : k) → (ρ.tprod (leftRegular k G)).Coinvariants)
      1)

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 : (ρ.tprod (leftRegular k G)).Coinvariants
⊢ Eq.{u_8 + 1} (α := V)
    ((ρ.coinvariantsTprodLeftRegularLEquiv : (a : (ρ.tprod (leftRegular k G)).Coinvariants) → V) x : V)
    ((ρ.ofCoinvariantsTprodLeftRegular : (a : (ρ.tprod (leftRegular k G)).Coinvariants) → V) x : V)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
g : G
h :
  ∀ (x : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))),
    Eq (α := (↑A : Type w))
      (((Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ
              (A.ρ.toCoinvariantsKer S :
                  (a : G) →
                    ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) →ₗ[k]
                      ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)))
                g :
            (a : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))) → (↑A : Type w))
          x :
        (↑A : Type w))
      (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ
              (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype :
            (a : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))) → (↑A : Type w))
          x :
        (↑A : Type w))
⊢ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ
      (A.ρ.toCoinvariantsKer S :
          (a : G) →
            ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) →ₗ[k] ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)))
        g =
    (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
g : G
x : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
⊢ Eq (α := (↑A : Type w))
    (((Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ
            (A.ρ.toCoinvariantsKer S :
                (a : G) →
                  ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) →ₗ[k]
                    ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)))
              g :
          (a : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))) → (↑A : Type w))
        x :
      (↑A : Type w))
    (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ
            (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype :
          (a : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))) → (↑A : Type w))
        x :
      (↑A : Type w))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
hf :
  ∀ (x : (↑(A.toCoinvariantsKer S) : Type w)),
    Eq (α := (↑(A.toCoinvariants S) : Type w))
      ((IntertwiningMap.toLinearMap
              (Hom.hom
                (ofHom
                    { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ :
                      (A.ρ.toCoinvariantsKer S).IntertwiningMap A.ρ } ≫
                  A.toCoinvariantsMkQ S)) :
            (a : (↑(A.toCoinvariantsKer S) : Type w)) → (↑(A.toCoinvariants S) : Type w))
          x :
        (↑(A.toCoinvariants S) : Type w))
      ((IntertwiningMap.toLinearMap (Hom.hom 0) :
            (a : (↑(A.toCoinvariantsKer S) : Type w)) → (↑(A.toCoinvariants S) : Type w))
          x :
        (↑(A.toCoinvariants S) : Type w))
⊢ Eq (α := A.toCoinvariantsKer S ⟶ A.toCoinvariants S)
    (ofHom { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ } ≫
      A.toCoinvariantsMkQ S)
    0

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
x : (↑(A.toCoinvariantsKer S) : Type w)
⊢ Eq (α := (↑(A.toCoinvariants S) : Type w))
    ((IntertwiningMap.toLinearMap
            (Hom.hom
              (ofHom
                  { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ :
                    (A.ρ.toCoinvariantsKer S).IntertwiningMap A.ρ } ≫
                A.toCoinvariantsMkQ S)) :
          (a : (↑(A.toCoinvariantsKer S) : Type w)) → (↑(A.toCoinvariants S) : Type w))
        x :
      (↑(A.toCoinvariants S) : Type w))
    ((IntertwiningMap.toLinearMap (Hom.hom 0) :
          (a : (↑(A.toCoinvariantsKer S) : Type w)) → (↑(A.toCoinvariants S) : Type w))
        x :
      (↑(A.toCoinvariants S) : Type w))

Tactic:
(Submodule.Quotient.mk_eq_zero _).2 x.2

Premises used: Iff.mpr, Submodule.Quotient.mk, Representation.Coinvariants, Submodule.Quotient.mk_eq_zero, Subtype.property
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
x : (↑(A.toCoinvariantsKer S) : Type w)
⊢ Eq (α := (↑(A.toCoinvariants S) : Type w))
    ((IntertwiningMap.toLinearMap
            (Hom.hom
              (ofHom
                  { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ :
                    (A.ρ.toCoinvariantsKer S).IntertwiningMap A.ρ } ≫
                A.toCoinvariantsMkQ S)) :
          (a : (↑(A.toCoinvariantsKer S) : Type w)) → (↑(A.toCoinvariants S) : Type w))
        x :
      (↑(A.toCoinvariants S) : Type w))
    ((IntertwiningMap.toLinearMap (Hom.hom 0) :
          (a : (↑(A.toCoinvariantsKer S) : Type w)) → (↑(A.toCoinvariants S) : Type w))
        x :
      (↑(A.toCoinvariants S) : Type w))

Tactic:
exact (Submodule.Quotient.mk_eq_zero _).2 x.2

Premises used: Iff.mpr, Submodule.Quotient.mk_eq_zero, Subtype.property
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B x : Rep.{w, u, v} k G
⊢ ModuleCat.ofHom (Coinvariants.map x.ρ x.ρ (Hom.hom (𝟙 x))) = 𝟙 (ModuleCat.of k x.ρ.Coinvariants)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B X Y Z : Rep.{w, u, v} k G
x : X ⟶ Y
x_1 : Y ⟶ Z
hf :
  ∀ (x_2 : (↑X : Type w)),
    Eq (α := (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
      ((ModuleCat.Hom.hom (ModuleCat.ofHom (Coinvariants.map X.ρ Z.ρ (Hom.hom (x ≫ x_1)))) ∘ₗ Coinvariants.mk X.ρ :
            (a : (↑X : Type w)) → (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
          x_2 :
        (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
      ((ModuleCat.Hom.hom
                (ModuleCat.ofHom (Coinvariants.map X.ρ Y.ρ (Hom.hom x)) ≫
                  ModuleCat.ofHom (Coinvariants.map Y.ρ Z.ρ (Hom.hom x_1))) ∘ₗ
              Coinvariants.mk X.ρ :
            (a : (↑X : Type w)) → (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
          x_2 :
        (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
⊢ ModuleCat.ofHom (Coinvariants.map X.ρ Z.ρ (Hom.hom (x ≫ x_1))) =
    ModuleCat.ofHom (Coinvariants.map X.ρ Y.ρ (Hom.hom x)) ≫ ModuleCat.ofHom (Coinvariants.map Y.ρ Z.ρ (Hom.hom x_1))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B X Y Z : Rep.{w, u, v} k G
x : X ⟶ Y
x_1 : Y ⟶ Z
x_2 : (↑X : Type w)
⊢ Eq (α := (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (Coinvariants.map X.ρ Z.ρ (Hom.hom (x ≫ x_1)))) ∘ₗ Coinvariants.mk X.ρ :
          (a : (↑X : Type w)) → (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
        x_2 :
      (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
    ((ModuleCat.Hom.hom
              (ModuleCat.ofHom (Coinvariants.map X.ρ Y.ρ (Hom.hom x)) ≫
                ModuleCat.ofHom (Coinvariants.map Y.ρ Z.ρ (Hom.hom x_1))) ∘ₗ
            Coinvariants.mk X.ρ :
          (a : (↑X : Type w)) → (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
        x_2 :
      (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
X : Rep.{u_1, u, v} k G
⊢ Epi (NatTrans.app (coinvariantsMk k G) X)

Tactic:
(ModuleCat.epi_iff_surjective _).2 <| Representation.Coinvariants.mk_surjective X.ρ

Premises used: Iff.mpr, ModuleCat.epi_iff_surjective, Rep.ρ, Representation.Coinvariants.mk_surjective
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A : Rep.{w, u, v} k G
M : ModuleCat.{w, u} k
f g : Functor.obj (coinvariantsFunctor k G) A ⟶ M
hfg : NatTrans.app (coinvariantsMk k G) A ≫ f = NatTrans.app (coinvariantsMk k G) A ≫ g
⊢ f = g

Tactic:
(cancel_epi _).1 hfg

Premises used: Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
inst_2 : B.ρ.IsTrivial
f : A ⟶ B
⊢ ∀ (x : G), (Hom.hom f).toLinearMap ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) x = (Hom.hom f).toLinearMap

Tactic:
simp [f.hom.2]

Premises used: Representation.IntertwiningMap.isIntertwining', Rep.Hom.hom
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B X : Rep.{w, u, v} k G
g : G
h :
  ∀ (x : (↑X : Type w)),
    Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))
      ((ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X) ∘ₗ
              (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g :
            (a : (↑X : Type w)) → (↑((coinvariantsFunctor k G).obj X) : Type w))
          x :
        (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))
      (((Representation.trivial k G (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w) :
                  (a : G) →
                    (↑((coinvariantsFunctor k G).obj X) : Type w) →ₗ[k] (↑((coinvariantsFunctor k G).obj X) : Type w))
                g ∘ₗ
              ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X) :
            (a : (↑X : Type w)) → (↑((coinvariantsFunctor k G).obj X) : Type w))
          x :
        (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))
⊢ ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X) ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Representation.trivial k G (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w) :
          (a : G) → (↑((coinvariantsFunctor k G).obj X) : Type w) →ₗ[k] (↑((coinvariantsFunctor k G).obj X) : Type w))
        g ∘ₗ
      ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B X : Rep.{w, u, v} k G
g : G
x : (↑X : Type w)
⊢ Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))
    ((ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X) ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g :
          (a : (↑X : Type w)) → (↑((coinvariantsFunctor k G).obj X) : Type w))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))
    (((Representation.trivial k G (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w) :
                (a : G) →
                  (↑((coinvariantsFunctor k G).obj X) : Type w) →ₗ[k] (↑((coinvariantsFunctor k G).obj X) : Type w))
              g ∘ₗ
            ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X) :
          (a : (↑X : Type w)) → (↑((coinvariantsFunctor k G).obj X) : Type w))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
Y : ModuleCat.{w, u} k
f : Functor.obj (coinvariantsFunctor k G) X ⟶ Y
⊢ IntertwiningMap.toLinearMap
      (Hom.hom
        ((Adjunction.homEquiv (coinvariantsAdjunction k G) X Y :
            (a : (coinvariantsFunctor k G).obj X ⟶ Y) → X ⟶ (trivialFunctor k G).obj Y)
          f)) =
    ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X ≫ f)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
Y : ModuleCat.{w, u} k
f : X ⟶ Functor.obj (trivialFunctor k G) Y
hfg :
  ∀
    (x :
      (↑(Functor.obj
            (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
              (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
              ModuleCat.carrier))
            X) :
        Type w)),
    Eq (α := (↑Y : Type w))
      ((ModuleCat.Hom.hom
              (NatTrans.app (coinvariantsMk k G) X ≫
                ((Adjunction.homEquiv (coinvariantsAdjunction k G) X Y).symm :
                    (a : X ⟶ (trivialFunctor k G).obj Y) → (coinvariantsFunctor k G).obj X ⟶ Y)
                  f) :
            (a : (↑((forget₂ (Rep k G) (ModuleCat k)).obj X) : Type w)) → (↑Y : Type w))
          x :
        (↑Y : Type w))
      ((ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X ≫ desc f) :
            (a : (↑((forget₂ (Rep k G) (ModuleCat k)).obj X) : Type w)) → (↑Y : Type w))
          x :
        (↑Y : Type w))
⊢ ((Adjunction.homEquiv (coinvariantsAdjunction k G) X Y).symm :
        (a : X ⟶ (trivialFunctor k G).obj Y) → (coinvariantsFunctor k G).obj X ⟶ Y)
      f =
    desc f

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
Y : ModuleCat.{w, u} k
f : X ⟶ Functor.obj (trivialFunctor k G) Y
x :
  (↑(Functor.obj
        (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
          (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
          ModuleCat.carrier))
        X) :
    Type w)
⊢ Eq (α := (↑Y : Type w))
    ((ModuleCat.Hom.hom
            (NatTrans.app (coinvariantsMk k G) X ≫
              ((Adjunction.homEquiv (coinvariantsAdjunction k G) X Y).symm :
                  (a : X ⟶ (trivialFunctor k G).obj Y) → (coinvariantsFunctor k G).obj X ⟶ Y)
                f) :
          (a : (↑((forget₂ (Rep k G) (ModuleCat k)).obj X) : Type w)) → (↑Y : Type w))
        x :
      (↑Y : Type w))
    ((ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X ≫ desc f) :
          (a : (↑((forget₂ (Rep k G) (ModuleCat k)).obj X) : Type w)) → (↑Y : Type w))
        x :
      (↑Y : Type w))

Tactic:
simp [coinvariantsAdjunction, Adjunction.homEquiv_symm_apply]

Premises used: Rep.coinvariantsAdjunction, CategoryTheory.Adjunction.homEquiv_symm_apply
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ Functor.IsLeftAdjoint (C := Rep.{u_1, u, v} k G) (coinvariantsFunctor k G)

Tactic:
(coinvariantsAdjunction k G).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.isLeftAdjoint, Rep.coinvariantsAdjunction
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep k G
a : (↑A : Type u)
b : (↑B : Type u)
⊢ Eq (α := (↑((Functor.obj (coinvariantsTensor k G) A).obj B) : Type u))
    ((((A.coinvariantsTensorMk B :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k G).obj A).obj B) : Type u))
              a :
            (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k G) A).obj B) : Type u)) :
          (a : (↑B : Type u)) → (↑(((coinvariantsTensor k G).obj A).obj B) : Type u))
        b :
      (↑((Functor.obj (coinvariantsTensor k G) A).obj B) : Type u))
    ((Coinvariants.mk (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) B).ρ :
          (a : TensorProduct k (↑A : Type u) (↑B : Type u)) →
            (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj B).ρ.Coinvariants)
        (a ⊗ₜ[k] b) :
      (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) B).ρ.Coinvariants)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Representation.tprod, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep k G
M : ModuleCat k
f g : (Functor.obj (coinvariantsTensor k G) A).obj B ⟶ M
hfg :
  Eq (α := (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑M : Type u))
    ((A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom f)) ((A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom g))
⊢ f = g

Tactic:
coinvariantsFunctor_hom_ext <| ModuleCat.hom_ext <| TensorProduct.ext <| hfg

Premises used: Rep.coinvariantsFunctor_hom_ext, ModuleCat.hom_ext, TensorProduct.ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
A B : Rep.{w, u, v} k_1 G_1
k : Type u
G : Type v
inst_2 : CommRing k
inst_3 : Group G
S : Subgroup G
inst_4 : S.Normal
X Y : Rep.{w, u, v} k G
f : X ⟶ Y
g_1 : G ⧸ S
g : G
H :
  ∀ (x : (↑X : Type w)),
    Eq (α := (↑(Y.toCoinvariants S) : Type w))
      ((((ModuleCat.Hom.hom
                    (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                      (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
                  (((X.toCoinvariants S).ρ.ofQuotient S :
                        Representation.{u, v, w} k (G ⧸ S) (↑(X.toCoinvariants S) : Type w)) :
                      (a : G ⧸ S) → (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(X.toCoinvariants S) : Type w))
                    (↑g : G ⧸ S)) ∘ₗ
                Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
              (↑X : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w)) :
            (a : (↑X : Type w)) → (↑(Y.toCoinvariants S) : Type w))
          x :
        (↑(Y.toCoinvariants S) : Type w))
      ((((((Y.toCoinvariants S).ρ.ofQuotient S : Representation.{u, v, w} k (G ⧸ S) (↑(Y.toCoinvariants S) : Type w)) :
                    (a : G ⧸ S) → (↑(Y.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
                  (↑g : G ⧸ S) ∘ₗ
                ModuleCat.Hom.hom
                  (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                    (CategoryTheory.Functor.map (resFunctor S.subtype) f))) ∘ₗ
              Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
            (a : (↑X : Type w)) → (↑(Y.toCoinvariants S) : Type w))
          x :
        (↑(Y.toCoinvariants S) : Type w))
⊢ Eq (α := (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
    (ModuleCat.Hom.hom
          (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
            (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
        (((X.toCoinvariants S).ρ.ofQuotient S : Representation.{u, v, w} k (G ⧸ S) (↑(X.toCoinvariants S) : Type w)) :
            (a : G ⧸ S) → (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(X.toCoinvariants S) : Type w))
          (↑g : G ⧸ S) :
      (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
    ((((Y.toCoinvariants S).ρ.ofQuotient S : Representation.{u, v, w} k (G ⧸ S) (↑(Y.toCoinvariants S) : Type w)) :
            (a : G ⧸ S) → (↑(Y.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
          (↑g : G ⧸ S) ∘ₗ
        ModuleCat.Hom.hom
          (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
            (CategoryTheory.Functor.map (resFunctor S.subtype) f)) :
      (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))

Tactic:
ext