awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
X Y : FDRep k G
⊢ ↥((Functor.obj
                (forget₂ (FDRep k G) (FC :=
                  HomSubtype (FGModuleCat k) G (FV :=
                    fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
                    (↑(X.obj (P := ModuleCat.isFG k)) : Type u) →ₗ[k] (↑(Y.obj (P := ModuleCat.isFG k)) : Type u))
                    (CV := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
                    (↑(X.obj (P := ModuleCat.isFG k)) : Type u)))
                  (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat k) G) ↦
                  (↑(X.V.obj (P := ModuleCat.isFG k)) : Type u)) (Rep k G) (FD := fun (A B : Rep k G) ↦
                  A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
                X).ρ.linHom
          (Functor.obj
              (forget₂ (FDRep k G) (FC :=
                HomSubtype (FGModuleCat k) G (FV :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
                  (↑(X.obj (P := ModuleCat.isFG k)) : Type u) →ₗ[k] (↑(Y.obj (P := ModuleCat.isFG k)) : Type u)) (CV :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
                  (↑(X.obj (P := ModuleCat.isFG k)) : Type u)))
                (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat k) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG k)) : Type u))
                (Rep k G) (FD := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
              Y).ρ).invariants ≃ₗ[k]
    X ⟶ Y

Tactic:
exact linHom.invariantsEquivRepHom
    ((forget₂ (FDRep k G) (Rep k G)).obj X) ((forget₂ (FDRep k G) (Rep k G)).obj Y) ≪≫ₗ
    FDRep.forget₂HomLinearEquiv X Y

Premises used: FDRep.forget₂HomLinearEquiv, FDRep, CategoryTheory.forget₂, Rep, Representation.linHom.invariantsEquivRepHom, CategoryTheory.Functor.obj
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A_1 : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
A B : Rep.{w, u, v} k G
f : A ⟶ B
x : ↥A.ρ.invariants
g : G
c : (↑A : Type w)
hc : c ∈ A.ρ.invariants
⊢ Eq (α := (↑B : Type w))
    ((((B.ρ : (a : G) → (↑B : Type w) →ₗ[k] (↑B : Type w)) g : (↑B : Type w) →ₗ[k] (↑B : Type w)) :
          (a : (↑B : Type w)) → (↑B : Type w))
        ((Hom.hom f : (a : (↑A : Type w)) → (↑B : Type w)) c : (↑B : Type w)) :
      (↑B : Type w))
    ((Hom.hom f : (a : (↑A : Type w)) → (↑B : Type w))
        ((((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            c :
          (↑A : Type w)) :
      (↑B : Type w))

Tactic:
have := (hom_comm_apply f g c).symm
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A_1 : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
A B : Rep.{w, u, v} k G
f : A ⟶ B
x : ↥A.ρ.invariants
g : G
c : (↑A : Type w)
hc : c ∈ A.ρ.invariants
this :
  Eq (α := (↑B : Type w))
    ((((B.ρ : (a : G) → (↑B : Type w) →ₗ[k] (↑B : Type w)) g : (↑B : Type w) →ₗ[k] (↑B : Type w)) :
          (a : (↑B : Type w)) → (↑B : Type w))
        ((Hom.hom f : (a : (↑A : Type w)) → (↑B : Type w)) c : (↑B : Type w)) :
      (↑B : Type w))
    ((Hom.hom f : (a : (↑A : Type w)) → (↑B : Type w))
        ((((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            c :
          (↑A : Type w)) :
      (↑B : Type w))
⊢ Eq (α := (↑B : Type w))
    ((((B.ρ : (a : G) → (↑B : Type w) →ₗ[k] (↑B : Type w)) g : (↑B : Type w) →ₗ[k] (↑B : Type w)) :
          (a : (↑B : Type w)) → (↑B : Type w))
        (((↑(Hom.hom f) :
                  [inst_3 : FunLike (A.ρ.IntertwiningMap B.ρ) (↑A : Type w) (↑B : Type w)] →
                    [SemilinearMapClass (A.ρ.IntertwiningMap B.ρ) (RingHom.id k) (↑A : Type w) (↑B : Type w)] →
                      (↑A : Type w) →ₗ[k] (↑B : Type w)) ∘ₗ
                A.ρ.invariants.subtype :
              (a : ↥A.ρ.invariants) → (↑B : Type w))
            (Subtype.mk (p := fun (x : (↑A : Type w)) ↦ x ∈ A.ρ.invariants) c hc) :
          (↑B : Type w)) :
      (↑B : Type w))
    (((↑(Hom.hom f) :
              [inst_3 : FunLike (A.ρ.IntertwiningMap B.ρ) (↑A : Type w) (↑B : Type w)] →
                [SemilinearMapClass (A.ρ.IntertwiningMap B.ρ) (RingHom.id k) (↑A : Type w) (↑B : Type w)] →
                  (↑A : Type w) →ₗ[k] (↑B : Type w)) ∘ₗ
            A.ρ.invariants.subtype :
          (a : ↥A.ρ.invariants) → (↑B : Type w))
        (Subtype.mk (p := fun (x : (↑A : Type w)) ↦ x ∈ A.ρ.invariants) c hc) :
      (↑B : Type w))

Tactic:
simp_all [hc g]
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S_1 : Subgroup G
inst_2 : S_1.Normal
S : Subgroup G
inst_3 : S.Normal
X Y : Rep.{w, u, v} k G
f : X ⟶ Y
g_1 : G ⧸ S
g : G
h :
  ∀ (x : ↥(invariants (MonoidHom.comp X.ρ S.subtype))),
    Eq.{w + 1} (α := (↑Y : Type w))
      (↑(((ModuleCat.Hom.hom
                    (CategoryTheory.Functor.map (invariantsFunctor k ↥S)
                      (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
                  ((X.ρ.quotientToInvariants S :
                        Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp X.ρ S.subtype))) :
                      (a : G ⧸ S) →
                        ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp X.ρ S.subtype)))
                    (↑g : G ⧸ S) :
                ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
              (a : ↥(invariants (MonoidHom.comp X.ρ S.subtype))) → ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
            x) :
        (↑Y : Type w))
      (↑(((((Y.ρ.quotientToInvariants S :
                        Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
                      (a : G ⧸ S) →
                        ↥(invariants (MonoidHom.comp Y.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
                    (↑g : G ⧸ S) ∘ₗ
                  ModuleCat.Hom.hom
                    (CategoryTheory.Functor.map (invariantsFunctor k ↥S)
                      (CategoryTheory.Functor.map (resFunctor S.subtype) f)) :
                ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
              (a : ↥(invariants (MonoidHom.comp X.ρ S.subtype))) → ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
            x) :
        (↑Y : Type w))
⊢ Eq (α := ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
    (ModuleCat.Hom.hom
          (CategoryTheory.Functor.map (invariantsFunctor k ↥S) (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
        ((X.ρ.quotientToInvariants S :
              Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp X.ρ S.subtype))) :
            (a : G ⧸ S) →
              ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp X.ρ S.subtype)))
          (↑g : G ⧸ S) :
      ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
    (((Y.ρ.quotientToInvariants S : Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
            (a : G ⧸ S) →
              ↥(invariants (MonoidHom.comp Y.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
          (↑g : G ⧸ S) ∘ₗ
        ModuleCat.Hom.hom
          (CategoryTheory.Functor.map (invariantsFunctor k ↥S) (CategoryTheory.Functor.map (resFunctor S.subtype) f)) :
      ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S_1 : Subgroup G
inst_2 : S_1.Normal
S : Subgroup G
inst_3 : S.Normal
X Y : Rep.{w, u, v} k G
f : X ⟶ Y
g_1 : G ⧸ S
g : G
x : ↥(invariants (MonoidHom.comp X.ρ S.subtype))
⊢ Eq.{w + 1} (α := (↑Y : Type w))
    (↑(((ModuleCat.Hom.hom
                  (CategoryTheory.Functor.map (invariantsFunctor k ↥S)
                    (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
                ((X.ρ.quotientToInvariants S :
                      Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp X.ρ S.subtype))) :
                    (a : G ⧸ S) →
                      ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp X.ρ S.subtype)))
                  (↑g : G ⧸ S) :
              ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
            (a : ↥(invariants (MonoidHom.comp X.ρ S.subtype))) → ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
          x) :
      (↑Y : Type w))
    (↑(((((Y.ρ.quotientToInvariants S :
                      Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
                    (a : G ⧸ S) →
                      ↥(invariants (MonoidHom.comp Y.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
                  (↑g : G ⧸ S) ∘ₗ
                ModuleCat.Hom.hom
                  (CategoryTheory.Functor.map (invariantsFunctor k ↥S)
                    (CategoryTheory.Functor.map (resFunctor S.subtype) f)) :
              ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
            (a : ↥(invariants (MonoidHom.comp X.ρ S.subtype))) → ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
          x) :
      (↑Y : Type w))

Tactic:
simp [hom_comm_apply]

Premises used: Rep.hom_comm_apply
-- Module: Mathlib.RepresentationTheory.Invariants
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 : ModuleCat.{u_1, u} k
⊢ ∀ (c : (↑x : Type u_1)),
    Membership.mem (α := (↑x : Type u_1)) (γ := Submodule k (↑x : Type u_1))
      (invariants (ρ (Functor.obj (trivialFunctor k G) x)) :
        Submodule k (↑(Functor.obj (trivialFunctor k G) x) : Type u_1))
      ((LinearMap.id : (a : (↑x : Type u_1)) → (↑x : Type u_1)) c : (↑x : Type u_1))

Tactic:
simp [trivialFunctor]

Premises used: Rep.trivialFunctor
-- Module: Mathlib.RepresentationTheory.Invariants
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 : Rep.{u_1, u, v} k G
g : G
h :
  ∀ (x : (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1)),
    Eq (α := (↑X : Type u_1))
      ((X.ρ.invariants.subtype ∘ₗ
              (Representation.trivial k G (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1) :
                  (a : G) →
                    (↑((invariantsFunctor k G).obj X) : Type u_1) →ₗ[k] (↑((invariantsFunctor k G).obj X) : Type u_1))
                g :
            (a : (↑((invariantsFunctor k G).obj X) : Type u_1)) → (↑X : Type u_1))
          x :
        (↑X : Type u_1))
      (((X.ρ : (a : G) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) g ∘ₗ X.ρ.invariants.subtype :
            (a : (↑((invariantsFunctor k G).obj X) : Type u_1)) → (↑X : Type u_1))
          x :
        (↑X : Type u_1))
⊢ X.ρ.invariants.subtype ∘ₗ
      (Representation.trivial k G (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1) :
          (a : G) → (↑((invariantsFunctor k G).obj X) : Type u_1) →ₗ[k] (↑((invariantsFunctor k G).obj X) : Type u_1))
        g =
    (X.ρ : (a : G) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) g ∘ₗ X.ρ.invariants.subtype

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Invariants
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 : Rep.{u_1, u, v} k G
g : G
x : (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    ((X.ρ.invariants.subtype ∘ₗ
            (Representation.trivial k G (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1) :
                (a : G) →
                  (↑((invariantsFunctor k G).obj X) : Type u_1) →ₗ[k] (↑((invariantsFunctor k G).obj X) : Type u_1))
              g :
          (a : (↑((invariantsFunctor k G).obj X) : Type u_1)) → (↑X : Type u_1))
        x :
      (↑X : Type u_1))
    (((X.ρ : (a : G) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) g ∘ₗ X.ρ.invariants.subtype :
          (a : (↑((invariantsFunctor k G).obj X) : Type u_1)) → (↑X : Type u_1))
        x :
      (↑X : Type u_1))

Tactic:
(x.2 g).symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.RepresentationTheory.Invariants
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 : Rep.{u_1, u, v} k G
g : G
x : (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    ((X.ρ.invariants.subtype ∘ₗ
            (Representation.trivial k G (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1) :
                (a : G) →
                  (↑((invariantsFunctor k G).obj X) : Type u_1) →ₗ[k] (↑((invariantsFunctor k G).obj X) : Type u_1))
              g :
          (a : (↑((invariantsFunctor k G).obj X) : Type u_1)) → (↑X : Type u_1))
        x :
      (↑X : Type u_1))
    (((X.ρ : (a : G) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) g ∘ₗ X.ρ.invariants.subtype :
          (a : (↑((invariantsFunctor k G).obj X) : Type u_1)) → (↑X : Type u_1))
        x :
      (↑X : Type u_1))

Tactic:
exact (x.2 g).symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.RepresentationTheory.Invariants
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 : ModuleCat.{u_1, u} k
Y : Rep.{u_1, u, v} k G
f : Functor.obj (trivialFunctor k G) X ⟶ Y
c : (↑(Functor.obj (trivialFunctor k G) X) : Type u_1)
_ :
  ∀ (g : G),
    Eq (α := (↑Y : Type u_1))
      ((((Y.ρ : (a : G) → (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) g : (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) :
            (a : (↑Y : Type u_1)) → (↑Y : Type u_1))
          (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c :
            (↑Y : Type u_1)) :
        (↑Y : Type u_1))
      (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c :
        (↑Y : Type u_1))
⊢ Membership.mem (α := (↑Y : Type u_1)) Y.ρ.invariants
    (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c : (↑Y : Type u_1))

Tactic:
_
-- Module: Mathlib.RepresentationTheory.Invariants
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 : ModuleCat.{u_1, u} k
Y : Rep.{u_1, u, v} k G
f : Functor.obj (trivialFunctor k G) X ⟶ Y
c : (↑(Functor.obj (trivialFunctor k G) X) : Type u_1)
g : G
⊢ Eq (α := (↑Y : Type u_1))
    ((((Y.ρ : (a : G) → (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) g : (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) :
          (a : (↑Y : Type u_1)) → (↑Y : Type u_1))
        (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c :
          (↑Y : Type u_1)) :
      (↑Y : Type u_1))
    (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c : (↑Y : Type u_1))

Tactic:
(hom_comm_apply f _ _).symm

Premises used: Rep.hom_comm_apply, Eq.symm
-- Module: Mathlib.RepresentationTheory.Invariants
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 : ModuleCat.{u_1, u} k
Y : Rep.{u_1, u, v} k G
f : Functor.obj (trivialFunctor k G) X ⟶ Y
c : (↑(Functor.obj (trivialFunctor k G) X) : Type u_1)
g : G
⊢ Eq (α := (↑Y : Type u_1))
    ((((Y.ρ : (a : G) → (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) g : (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) :
          (a : (↑Y : Type u_1)) → (↑Y : Type u_1))
        (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c :
          (↑Y : Type u_1)) :
      (↑Y : Type u_1))
    (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c : (↑Y : Type u_1))

Tactic:
exact (hom_comm_apply f _ _).symm

Premises used: Rep.hom_comm_apply, Eq.symm
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
X : ModuleCat.{u_1, u} k
Y : Rep.{u_1, u, v} k G
f : Functor.obj (trivialFunctor k G) X ⟶ Y
⊢ ModuleCat.Hom.hom
      ((Adjunction.homEquiv (invariantsAdjunction k G) X Y :
          (a : (trivialFunctor k G).obj X ⟶ Y) → X ⟶ (invariantsFunctor k G).obj Y)
        f) =
    LinearMap.codRestrict Y.ρ.invariants (Hom.hom f).toLinearMap ⋯

Tactic:
rfl

Premises used: Set.Mem, LinearMap.codRestrict, rfl
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
X : ModuleCat.{u_1, u} k
Y : Rep.{u_1, u, v} k G
f : X ⟶ Functor.obj (invariantsFunctor k G) Y
⊢ IntertwiningMap.toLinearMap
      (Hom.hom
        (((Adjunction.homEquiv (invariantsAdjunction k G) X Y).symm :
            (a : X ⟶ (invariantsFunctor k G).obj Y) → (trivialFunctor k G).obj X ⟶ Y)
          f)) =
    Y.ρ.invariants.subtype ∘ₗ ModuleCat.Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Invariants
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
⊢ Functor.IsRightAdjoint (C := ModuleCat.{u_1, u} k) (D := Rep.{u_1, u, v} k G) (invariantsFunctor k G)

Tactic:
(invariantsAdjunction k G).isRightAdjoint

Premises used: Rep.invariantsAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
rw : ρ.IsIrreducible ↔ IsSimpleOrder.{u_3} (Submodule k[G] ρ.asModule)
⊢ ρ.IsIrreducible ↔ IsSimpleModule k[G] ρ.asModule

Tactic:
rw [isSimpleModule_iff]

Premises used: isSimpleModule_iff
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
⊢ ρ.IsIrreducible ↔ IsSimpleOrder.{u_3} (Submodule k[G] ρ.asModule)

Tactic:
OrderIso.isSimpleOrder_iff Subrepresentation.subrepresentationSubmoduleOrderIso

Premises used: Subrepresentation.subrepresentationSubmoduleOrderIso, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
⊢ ρ.IsIrreducible ↔ IsSimpleOrder.{u_3} (Submodule k[G] ρ.asModule)

Tactic:
exact OrderIso.isSimpleOrder_iff Subrepresentation.subrepresentationSubmoduleOrderIso

Premises used: Subrepresentation.subrepresentationSubmoduleOrderIso, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
inst : Monoid G
inst_1 : Field k
M : Type u_5
inst_2 : AddCommGroup M
inst_3 : Module k[G] M
rw :
  IsSimpleOrder.{u_5} (Submodule k[G] M) ↔
    IsIrreducible.{u_1, u_2, u_5} (G := G) (k := k) (V := RestrictScalars k k[G] M) (ofModule M)
⊢ IsSimpleModule k[G] M ↔ IsIrreducible.{u_1, u_2, u_5} (G := G) (k := k) (V := RestrictScalars k k[G] M) (ofModule M)

Tactic:
rw [isSimpleModule_iff]

Premises used: isSimpleModule_iff
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
inst : Monoid G
inst_1 : Field k
M : Type u_5
inst_2 : AddCommGroup M
inst_3 : Module k[G] M
⊢ IsSimpleOrder.{u_5} (Submodule k[G] M) ↔
    IsIrreducible.{u_1, u_2, u_5} (G := G) (k := k) (V := RestrictScalars k k[G] M) (ofModule M)

Tactic:
OrderIso.isSimpleOrder_iff Subrepresentation.submoduleSubrepresentationOrderIso

Premises used: Subrepresentation.submoduleSubrepresentationOrderIso, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
inst : Monoid G
inst_1 : Field k
M : Type u_5
inst_2 : AddCommGroup M
inst_3 : Module k[G] M
⊢ IsSimpleOrder.{u_5} (Submodule k[G] M) ↔
    IsIrreducible.{u_1, u_2, u_5} (G := G) (k := k) (V := RestrictScalars k k[G] M) (ofModule M)

Tactic:
exact OrderIso.isSimpleOrder_iff Subrepresentation.submoduleSubrepresentationOrderIso

Premises used: Subrepresentation.submoduleSubrepresentationOrderIso, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field k
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 σ
inst_6 : ρ.IsIrreducible
⊢ IsSimpleModule k[G] ρ.asModule

Tactic:
(irreducible_iff_isSimpleModule_asModule ρ).mp inferInstance

Premises used: inferInstance, Iff.mp, Representation.irreducible_iff_isSimpleModule_asModule
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field k
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 σ
inst_6 : ρ.IsIrreducible
rw :
  Injective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨
    Eq (α := LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      ((equivLinearMapAsModule ρ σ : (a : ρ.IntertwiningMap σ) → ρ.asModule →ₗ[k[G]] σ.asModule) f :
        LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      (0 : LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
⊢ Injective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨ f = 0

Tactic:
rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule ρ σ)]

Premises used: Representation.IntertwiningMap.equivLinearMapAsModule, LinearEquiv.map_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field k
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 σ
inst_6 : ρ.IsIrreducible
⊢ Injective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨
    Eq (α := LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      ((equivLinearMapAsModule ρ σ : (a : ρ.IntertwiningMap σ) → ρ.asModule →ₗ[k[G]] σ.asModule) f :
        LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      (0 : LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)

Tactic:
LinearMap.injective_or_eq_zero (equivLinearMapAsModule ρ σ f)

Premises used: Representation.instAddCommMonoidAsModule._aux_4, Representation.asModule, Representation.instAddCommMonoidAsModule._aux_1, Representation.IntertwiningMap.equivLinearMapAsModule, DFunLike.coe, LinearMap.injective_or_eq_zero
-- Module: Mathlib.RepresentationTheory.Irreducible
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field k
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 σ
inst_6 : ρ.IsIrreducible
⊢ Injective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨
    Eq (α := LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      ((equivLinearMapAsModule ρ σ : (a : ρ.IntertwiningMap σ) → ρ.asModule →ₗ[k[G]] σ.asModule) f :
        LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      (0 : LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)

Tactic:
exact LinearMap.injective_or_eq_zero (equivLinearMapAsModule ρ σ f)

Premises used: Representation.IntertwiningMap.equivLinearMapAsModule, DFunLike.coe, LinearMap.injective_or_eq_zero