awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A_1 : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
x : (↑B : Type (max w u_1))
x_1 : H
⊢ Eq (α := (↑A : Type (max u_1 w)))
    ((↑((LinearMap.codRestrict (Representation.coindV φ A.ρ)
                  (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
                    (Hom.hom f).toLinearMap ∘ₗ
                      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
                  ⋯ ∘ₗ
                (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g :
              (a : (↑B : Type (max w u_1))) → ↥(Representation.coindV φ A.ρ))
            x) :
        H → (↑A : Type (max u_1 w)))
      x_1)
    ((↑((LinearMap.restrict (LinearMap.funLeft k (↑A : Type (max u_1 w)) fun (x : H) ↦ x * g) ⋯ ∘ₗ
                LinearMap.codRestrict (Representation.coindV φ A.ρ)
                  (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
                    (Hom.hom f).toLinearMap ∘ₗ
                      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
                  ⋯ :
              (a : (↑B : Type (max w u_1))) → ↥(Representation.coindV φ A.ρ))
            x) :
        H → (↑A : Type (max u_1 w)))
      x_1)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
c : (↑B : Type (max w u_1))
i : H
⊢ Eq (α := (↑A : Type (max u_1 w)))
    ((↑((Hom.hom (resCoindToHom.{u, v, w, u_1} φ B A f) :
                (a : (↑B : Type (max w u_1))) → (↑(coind φ A) : Type (max w u_1)))
              c) :
          H → (↑A : Type (max u_1 w)))
        i :
      (↑A : Type (max u_1 w)))
    ((Hom.hom f : (a : (↑(res φ B) : Type (max w u_1))) → (↑A : Type (max w u_1)))
        ((((B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) i :
              (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) :
            (a : (↑B : Type (max w u_1))) → (↑B : Type (max w u_1)))
          c) :
      (↑A : Type (max w u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep.{?u.234193, u, v} k G
X' X : Rep.{max w t, u, w} k H
Y : Rep.{max w t, u, v} k G
f : X' ⟶ X
g : X ⟶ Functor.obj (coindFunctor k φ) Y
⊢ Eq (α := Functor.obj (resFunctor φ) X' ⟶ Y)
    (((resCoindHomEquiv.{t, u, v, w} φ X' Y).toEquiv.symm :
          (a : X' ⟶ (coindFunctor k φ).obj Y) → (resFunctor φ).obj X' ⟶ Y)
        (f ≫ g) :
      Functor.obj (resFunctor φ) X' ⟶ Y)
    (CategoryTheory.Functor.map (resFunctor φ) f ≫
        ((resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv.symm :
            (a : X ⟶ (coindFunctor k φ).obj Y) → (resFunctor φ).obj X ⟶ Y)
          g :
      Functor.obj (resFunctor φ) X' ⟶ Y)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep.{?u.234193, u, v} k G
X : Rep.{max w t, u, w} k H
Y Y' : Rep.{max w t, u, v} k G
f : Functor.obj (resFunctor φ) X ⟶ Y
g : Y ⟶ Y'
hf :
  ∀ (x : (↑X : Type (max t w))),
    Eq (α := (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))
      ((Representation.IntertwiningMap.toLinearMap
              (Hom.hom
                (((resCoindHomEquiv.{t, u, v, w} φ X Y').toEquiv :
                    (a : (resFunctor φ).obj X ⟶ Y') → X ⟶ (coindFunctor k φ).obj Y')
                  (f ≫ g))) :
            (a : (↑X : Type (max t w))) → (↑((coindFunctor k φ).obj Y') : Type (max t w)))
          x :
        (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))
      ((Representation.IntertwiningMap.toLinearMap
              (Hom.hom
                (((resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv :
                      (a : (resFunctor φ).obj X ⟶ Y) → X ⟶ (coindFunctor k φ).obj Y)
                    f ≫
                  CategoryTheory.Functor.map (coindFunctor k φ) g)) :
            (a : (↑X : Type (max t w))) → (↑((coindFunctor k φ).obj Y') : Type (max t w)))
          x :
        (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))
⊢ Eq (α := X ⟶ Functor.obj (coindFunctor k φ) Y')
    (((resCoindHomEquiv.{t, u, v, w} φ X Y').toEquiv : (a : (resFunctor φ).obj X ⟶ Y') → X ⟶ (coindFunctor k φ).obj Y')
        (f ≫ g) :
      X ⟶ Functor.obj (coindFunctor k φ) Y')
    (((resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv : (a : (resFunctor φ).obj X ⟶ Y) → X ⟶ (coindFunctor k φ).obj Y) f ≫
        CategoryTheory.Functor.map (coindFunctor k φ) g :
      X ⟶ Functor.obj (coindFunctor k φ) Y')

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep.{?u.234193, u, v} k G
X : Rep.{max w t, u, w} k H
Y Y' : Rep.{max w t, u, v} k G
f : Functor.obj (resFunctor φ) X ⟶ Y
g : Y ⟶ Y'
x : (↑X : Type (max t w))
⊢ Eq (α := (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              (((resCoindHomEquiv.{t, u, v, w} φ X Y').toEquiv :
                  (a : (resFunctor φ).obj X ⟶ Y') → X ⟶ (coindFunctor k φ).obj Y')
                (f ≫ g))) :
          (a : (↑X : Type (max t w))) → (↑((coindFunctor k φ).obj Y') : Type (max t w)))
        x :
      (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              (((resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv :
                    (a : (resFunctor φ).obj X ⟶ Y) → X ⟶ (coindFunctor k φ).obj Y)
                  f ≫
                CategoryTheory.Functor.map (coindFunctor k φ) g)) :
          (a : (↑X : Type (max t w))) → (↑((coindFunctor k φ).obj Y') : Type (max t w)))
        x :
      (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep.{?u.237814, u, v} k G
⊢ Functor.IsRightAdjoint (C := Rep.{max w t, u, w} k H) (coindFunctor k φ)

Tactic:
(resCoindAdjunction k φ).isRightAdjoint

Premises used: Rep.resCoindAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep.{?u.238433, u, v} k G
⊢ Functor.IsLeftAdjoint (C := Rep.{max w t, u, w} k H) (resFunctor φ)

Tactic:
(resCoindAdjunction k φ).isLeftAdjoint

Premises used: Rep.resCoindAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep.{?u.239238, u, v} k G_1
G : Type w
inst_3 : Group G
S : Subgroup G
⊢ Functor.PreservesProjectiveObjects (C := Rep.{max w t, u, w} k G) (resFunctor S.subtype)

Tactic:
(resFunctor S.subtype).preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms
    (resCoindAdjunction k S.subtype)

Premises used: Subgroup.subtype, Rep.resCoindAdjunction, CategoryTheory.Functor.preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
inst_6 : AddCommGroup X
inst_7 : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
inst_8 : Module.Finite k V
⊢ Module.Finite.{u_1, u_3} k ρ.Coinvariants

Tactic:
inferInstanceAs <| Module.Finite k (V ⧸ Coinvariants.ker ρ)

Premises used: _private.0.Representation.Coinvariants.instFinite._proof_1
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) x ∈ ker ρ

Tactic:
Submodule.subset_span <| Set.mem_range_self (g, x)

Premises used: Set.mem_range_self, Set.Mem, Prod.mk, Submodule.subset_span
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
x a : V
h : HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) x = a
⊢ a ∈ ker ρ

Tactic:
Submodule.subset_span ⟨(g, x), h⟩

Premises used: Set.Mem, Prod.mk, Exists.intro, Submodule.subset_span
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
x y : V
⊢ Eq (α := ρ.Coinvariants) ((mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants)
      ((mk ρ : (a : V) → ρ.Coinvariants) y : ρ.Coinvariants) ↔
    x - y ∈ ker ρ

Tactic:
Submodule.Quotient.eq _

Premises used: Submodule.Quotient.eq, Set.Mem, Submodule.Quotient.mk, Representation.Coinvariants
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
x : V
⊢ Eq (α := ρ.Coinvariants) ((mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants) (0 : ρ.Coinvariants) ↔ x ∈ ker ρ

Tactic:
Submodule.Quotient.mk_eq_zero _

Premises used: Set.Mem, Submodule.Quotient.mk, Representation.Coinvariants, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
⊢ Function.Surjective (α := V) (β := ρ.Coinvariants) (⇑(mk ρ) : (a : V) → ρ.Coinvariants)

Tactic:
Submodule.Quotient.mk_surjective _

Premises used: Submodule.Quotient.mk, Representation.Coinvariants, Submodule.Quotient.mk_surjective
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ Eq (α := ρ.Coinvariants)
    ((mk ρ : (a : V) → ρ.Coinvariants) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x) : ρ.Coinvariants)
    ((mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants)

Tactic:
(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 : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
motive : ρ.Coinvariants → Prop
x : ρ.Coinvariants
h : ∀ (v : V), motive ((mk ρ : (a : V) → ρ.Coinvariants) v)
⊢ motive x

Tactic:
Submodule.Quotient.induction_on _ x h

Premises used: Representation.Coinvariants.ker, Submodule.Quotient.induction_on
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
inst_6 : AddCommGroup X
inst_7 : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
f : V →ₗ[k] W
h : ∀ (x : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) x = f
x : V
h_1 :
  Membership.mem (γ := Set V)
    (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)
    x
g : G
y : V
hy :
  (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)
      (g, y) =
    x
⊢ x ∈ (↑f.ker : Set V)

Tactic:
simpa only [← hy, SetLike.mem_coe, LinearMap.mem_ker, map_sub, sub_eq_zero, LinearMap.coe_comp,
      Function.comp_apply] using LinearMap.ext_iff.1 (h g) y

Premises used: map_sub, sub_eq_zero, LinearMap.ext_iff, LinearMap.mem_ker, LinearMap.coe_comp, SetLike.mem_coe, Iff.mp, Function.comp_apply
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
f : V →ₗ[k] W
h : ∀ (x : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) x = f
⊢ lift ρ f h ∘ₗ mk ρ = f

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
f : V →ₗ[k] W
h : ∀ (x : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) x = f
x : V
⊢ Eq.{u_4 + 1} (α := W)
    ((lift ρ f h : (a : ρ.Coinvariants) → W) ((mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants) : W)
    ((f : (a : V) → W) x : W)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
f g : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id k) ρ.Coinvariants W
H : f ∘ₗ mk ρ = g ∘ₗ mk ρ
⊢ f = g

Tactic:
Submodule.linearMap_qext _ H

Premises used: Submodule.linearMap_qext, Representation.Coinvariants
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
inst_6 : AddCommGroup X
inst_7 : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
f : ρ.IntertwiningMap τ
g : G
x : V
⊢ HSub.hSub (α := W) (β := W) ((((τ : (a : G) → W →ₗ[k] W) g : W →ₗ[k] W) : (a : W) → W) ((f : (a : V) → W) x : W) : W)
      ((f : (a : V) → W) x : W) =
    HSub.hSub (α := W) (β := W)
      (((↑f :
              [inst_8 : FunLike (ρ.IntertwiningMap τ) V W] →
                [SemilinearMapClass (ρ.IntertwiningMap τ) (RingHom.id k) V W] → V →ₗ[k] W) :
            (a : V) → W)
          ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) :
        W)
      (((↑f :
              [inst_8 : FunLike (ρ.IntertwiningMap τ) V W] →
                [SemilinearMapClass (ρ.IntertwiningMap τ) (RingHom.id k) V W] → V →ₗ[k] W) :
            (a : V) → W)
          x :
        W)

Tactic:
simpa using congr($((f.isIntertwining' g).symm) x)
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Monoid 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
f : ρ.IntertwiningMap τ
⊢ map ρ τ f ∘ₗ mk ρ =
    mk τ ∘ₗ
      (↑f :
        [inst_6 : FunLike (ρ.IntertwiningMap τ) V W] →
          [SemilinearMapClass (ρ.IntertwiningMap τ) (RingHom.id k) V W] → V →ₗ[k] W)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Representation.Coinvariants.map, Quotient, Representation.Coinvariants.mk, Submodule.mkQ, rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Monoid 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
f : ρ.IntertwiningMap τ
x : V
⊢ Eq.{u_4 + 1} (α := τ.Coinvariants)
    ((map ρ τ f : (a : ρ.Coinvariants) → τ.Coinvariants) ((mk ρ : (a : V) → ρ.Coinvariants) x) : τ.Coinvariants)
    ((mk τ : (a : W) → τ.Coinvariants) ((f : (a : V) → W) x) : τ.Coinvariants)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
H :
  ∀ (x : V),
    Eq (α := ρ.Coinvariants) ((map ρ ρ (IntertwiningMap.id ρ) ∘ₗ mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants)
      ((LinearMap.id ∘ₗ mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants)
⊢ map ρ ρ (IntertwiningMap.id ρ) = LinearMap.id

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
x : V
⊢ Eq (α := ρ.Coinvariants) ((map ρ ρ (IntertwiningMap.id ρ) ∘ₗ mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants)
    ((LinearMap.id ∘ₗ mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
inst_6 : AddCommGroup X
inst_7 : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
φ : ρ.IntertwiningMap τ
ψ : τ.IntertwiningMap υ
⊢ map τ υ ψ ∘ₗ map ρ τ φ = map ρ υ (ψ.comp φ)

Tactic:
hom_ext rfl

Premises used: Representation.Coinvariants.hom_ext, rfl
-- 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
S : Subgroup G
inst_4 : S.Normal
g : G
x_1 : V
h :
  Membership.mem (γ := Set V)
    (Set.range fun (gv : Prod.{u_7, u_8} (↥S) V) ↦
      HSub.hSub (α := V)
        ((((MonoidHom.comp ρ S.subtype : (a : ↥S) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
    x_1
s : ↥S
x : V
hs :
  (fun (gv : Prod.{u_7, u_8} (↥S) V) ↦
        HSub.hSub (α := V)
          ((((MonoidHom.comp ρ S.subtype : (a : ↥S) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      (s, x) =
    x_1
⊢ HSub.hSub (α := V) (β := V)
      ((((MonoidHom.comp ρ S.subtype : (a : ↥S) → V →ₗ[k] V)
                (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (↑s : G) * g⁻¹) ⋯) :
              V →ₗ[k] V) :
            (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) :
        V)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) =
    HSub.hSub (α := V) (β := V)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[k] V) (↑s : G) : V →ₗ[k] V) : (a : V) → V) x : V) :
        V)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (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
S : Subgroup G
inst_4 : S.Normal
g : G
x_1 : V
h :
  Membership.mem (γ := Set V)
    (Set.range fun (gv : Prod.{u_7, u_8} (↥S) V) ↦
      HSub.hSub (α := V)
        ((((MonoidHom.comp ρ S.subtype : (a : ↥S) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
    x_1
s : ↥S
x : V
hs :
  (fun (gv : Prod.{u_7, u_8} (↥S) V) ↦
        HSub.hSub (α := V)
          ((((MonoidHom.comp ρ S.subtype : (a : ↥S) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      (s, x) =
    x_1
⊢ x_1 ∈
    (↑(Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) (ker (MonoidHom.comp ρ S.subtype))) : Set V)

Tactic:
simpa [← hs] using mem_ker_of_eq
      ⟨g * s * g⁻¹, Subgroup.Normal.conj_mem ‹_› s.1 s.2 g⟩ (ρ g x) _ <| by simp

Premises used: Representation.Coinvariants.mem_ker_of_eq, DFunLike.coe
-- 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
S : Subgroup G
inst_4 : S.Normal
g : G
x : V
⊢ Eq (α := Coinvariants (MonoidHom.comp ρ S.subtype))
    ((((ρ.toCoinvariants S :
                (a : G) → Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
              g :
            Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype)) :
          (a : Coinvariants (MonoidHom.comp ρ S.subtype)) → Coinvariants (MonoidHom.comp ρ S.subtype))
        ((mk (MonoidHom.comp ρ S.subtype) : (a : V) → Coinvariants (MonoidHom.comp ρ S.subtype)) x) :
      Coinvariants (MonoidHom.comp ρ S.subtype))
    ((mk (MonoidHom.comp ρ S.subtype) : (a : V) → Coinvariants (MonoidHom.comp ρ S.subtype))
        ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x) :
      Coinvariants (MonoidHom.comp ρ S.subtype))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, 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
H :
  ∀ (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))
⊢ Eq.{u_8 + 1} (α := Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] 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 :
      Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
    (LinearMap.id : Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))

Tactic:
ext x