awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Rep.Res
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k G
x x_1 : Rep.{u_1, u, v1} k G
x_2 x_3 : x ⟶ x_1
hf :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (x_2 + x_3))) =
    (Hom.hom
        (HAdd.hAdd (α := Functor.obj (resFunctor f) x ⟶ Functor.obj (resFunctor f) x_1)
          (CategoryTheory.Functor.map (resFunctor f) x_2) (CategoryTheory.Functor.map (resFunctor f) x_3))).toLinearMap
⊢ CategoryTheory.Functor.map (resFunctor f) (x_2 + x_3) =
    HAdd.hAdd (α := Functor.obj (resFunctor f) x ⟶ Functor.obj (resFunctor f) x_1)
      (CategoryTheory.Functor.map (resFunctor f) x_2) (CategoryTheory.Functor.map (resFunctor f) x_3)

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Res
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k G
x x_1 : Rep.{u_1, u, v1} k G
x_2 x_3 : x ⟶ x_1
hf :
  Representation.IntertwiningMap.toLinearMap
      (Hom.hom
        (ofHom
          {
            toLinearMap :=
              (↑(Hom.hom x_2 + Hom.hom x_3) :
                [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                  [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                    (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
            isIntertwining' := ⋯ : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })) =
    HAdd.hAdd (α := (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1))
      (Representation.IntertwiningMap.toLinearMap
        (Hom.hom
          (ofHom
            {
              toLinearMap :=
                (↑(Hom.hom x_2) :
                  [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                    [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                      (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
              isIntertwining' := ⋯ : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })))
      (Representation.IntertwiningMap.toLinearMap
        (Hom.hom
          (ofHom
            {
              toLinearMap :=
                (↑(Hom.hom x_3) :
                  [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                    [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                      (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
              isIntertwining' := ⋯ : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })))
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (x_2 + x_3))) =
    (Hom.hom
        (HAdd.hAdd (α := Functor.obj (resFunctor f) x ⟶ Functor.obj (resFunctor f) x_1)
          (CategoryTheory.Functor.map (resFunctor f) x_2) (CategoryTheory.Functor.map (resFunctor f) x_3))).toLinearMap

Tactic:
simp only [add_hom, Representation.IntertwiningMap.add_toLinearMap]

Premises used: Rep.add_hom, Representation.IntertwiningMap.add_toLinearMap
-- Module: Mathlib.RepresentationTheory.Rep.Res
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k G
x x_1 : Rep.{u_1, u, v1} k G
x_2 x_3 : x ⟶ x_1
⊢ Representation.IntertwiningMap.toLinearMap
      (Hom.hom
        (ofHom
          {
            toLinearMap :=
              (↑(Hom.hom x_2 + Hom.hom x_3) :
                [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                  [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                    (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
            isIntertwining' := ⋯ : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })) =
    HAdd.hAdd (α := (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1))
      (Representation.IntertwiningMap.toLinearMap
        (Hom.hom
          (ofHom
            {
              toLinearMap :=
                (↑(Hom.hom x_2) :
                  [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                    [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                      (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
              isIntertwining' := ⋯ : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })))
      (Representation.IntertwiningMap.toLinearMap
        (Hom.hom
          (ofHom
            {
              toLinearMap :=
                (↑(Hom.hom x_3) :
                  [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                    [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                      (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
              isIntertwining' := ⋯ : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Res
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
hf :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (Hom.hom
        (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
          (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
⊢ CategoryTheory.Functor.map (resFunctor f) (r • l) =
    HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
      (CategoryTheory.Functor.map (resFunctor f) l)

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Res
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
hf :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (HSMul.hSMul (β := (Functor.obj (resFunctor f) X).ρ.IntertwiningMap (Functor.obj (resFunctor f) Y).ρ) r
        (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
hf₁ :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₂ :
  (Hom.hom (r • l)).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₃ :
  (r • Hom.hom l).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₄ :
  r • (Hom.hom l).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₅ hf₆ : r • (Hom.hom l).toLinearMap = r • (Hom.hom l).toLinearMap
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (Hom.hom
        (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
          (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap

Tactic:
rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap, smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap]

Premises used: Rep.res_map_hom_toLinearMap, Rep.smul_hom, Representation.IntertwiningMap.toLinearMap_smul
-- Module: Mathlib.RepresentationTheory.Semisimple
Goal:
k : Type u_1
G : 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 : ρ.IsSemisimpleRepresentation ↔ ComplementedLattice.{u_3} (Submodule k[G] ρ.asModule)
⊢ ρ.IsSemisimpleRepresentation ↔ IsSemisimpleModule k[G] ρ.asModule

Tactic:
rw [isSemisimpleModule_iff]

Premises used: isSemisimpleModule_iff
-- Module: Mathlib.RepresentationTheory.Semisimple
Goal:
k : Type u_1
G : 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
⊢ ρ.IsSemisimpleRepresentation ↔ ComplementedLattice.{u_3} (Submodule k[G] ρ.asModule)

Tactic:
OrderIso.complementedLattice_iff Subrepresentation.subrepresentationSubmoduleOrderIso

Premises used: OrderIso.complementedLattice_iff, Subrepresentation.subrepresentationSubmoduleOrderIso
-- Module: Mathlib.RepresentationTheory.Semisimple
Goal:
k : Type u_1
G : 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
⊢ ρ.IsSemisimpleRepresentation ↔ ComplementedLattice.{u_3} (Submodule k[G] ρ.asModule)

Tactic:
exact OrderIso.complementedLattice_iff Subrepresentation.subrepresentationSubmoduleOrderIso

Premises used: OrderIso.complementedLattice_iff, Subrepresentation.subrepresentationSubmoduleOrderIso
-- Module: Mathlib.RepresentationTheory.Semisimple
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Field k
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module k[G] M
rw :
  ComplementedLattice.{u_4} (Submodule k[G] M) ↔
    IsSemisimpleRepresentation.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)
⊢ IsSemisimpleModule k[G] M ↔
    IsSemisimpleRepresentation.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)

Tactic:
rw [isSemisimpleModule_iff]

Premises used: isSemisimpleModule_iff
-- Module: Mathlib.RepresentationTheory.Semisimple
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Field k
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module k[G] M
⊢ ComplementedLattice.{u_4} (Submodule k[G] M) ↔
    IsSemisimpleRepresentation.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)

Tactic:
OrderIso.complementedLattice_iff Subrepresentation.submoduleSubrepresentationOrderIso

Premises used: OrderIso.complementedLattice_iff, Subrepresentation.submoduleSubrepresentationOrderIso
-- Module: Mathlib.RepresentationTheory.Semisimple
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Field k
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module k[G] M
⊢ ComplementedLattice.{u_4} (Submodule k[G] M) ↔
    IsSemisimpleRepresentation.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)

Tactic:
exact OrderIso.complementedLattice_iff Subrepresentation.submoduleSubrepresentationOrderIso

Premises used: OrderIso.complementedLattice_iff, Subrepresentation.submoduleSubrepresentationOrderIso
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : Submodule k V
rw :
  Membership.mem (γ := Sublattice (Submodule k V)) (⨅ (g : G), Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g))
      p ↔
    ∀ (g : G),
      Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p
rw₁ rw₂ :
  (∀ (i : G),
      Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) i)) p) ↔
    ∀ (g : G),
      Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p
⊢ p ∈ ρ.invtSubmodule ↔
    ∀ (g : G),
      Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p

Tactic:
rw [invtSubmodule, Sublattice.mem_iInf]

Premises used: Representation.invtSubmodule, Sublattice.mem_iInf
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
⊢ ⊤ ∈ ρ.invtSubmodule

Tactic:
simp [invtSubmodule]

Premises used: Representation.invtSubmodule
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
⊢ ⊥ ∈ ρ.invtSubmodule

Tactic:
simp [invtSubmodule]

Premises used: Representation.invtSubmodule
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : ↥ρ.invtSubmodule
p : Submodule k V
hp : p ∈ ρ.invtSubmodule
⊢ Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule) p hp ≤
    Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule) ⊤ ⋯

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : ↥ρ.invtSubmodule
p : Submodule k V
hp : p ∈ ρ.invtSubmodule
⊢ Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule) ⊥ ⋯ ≤
    Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule) p hp

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
⊢ Eq.{u_3 + 1} (α := Submodule k V) (↑⊤ : Submodule k V) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
⊢ Eq.{u_3 + 1} (α := Submodule k V) (↑⊥ : Submodule k V) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
⊢ Nontrivial.{u_3} ↥ρ.invtSubmodule ↔ Nontrivial V

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
refine_1 : ∀ (h : Nontrivial.{u_3} ↥ρ.invtSubmodule), Nontrivial V
refine_2 : ∀ (h : Nontrivial V), Nontrivial.{u_3} ↥ρ.invtSubmodule
⊢ Nontrivial.{u_3} ↥ρ.invtSubmodule ↔ Nontrivial V

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
h : Nontrivial.{u_3} ↥ρ.invtSubmodule
refine_1 : ∀ (h : Subsingleton V), Subsingleton.{u_3 + 1} ↥ρ.invtSubmodule
⊢ Nontrivial V

Tactic:
contrapose! h
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
h : Subsingleton V
⊢ Subsingleton.{u_3 + 1} ↥ρ.invtSubmodule

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
h : Nontrivial V
⊢ Nontrivial.{u_3} ↥ρ.invtSubmodule

Tactic:
⟨⊥, ⊤, ?_⟩

Premises used: Bot.bot, Nontrivial.mk, Exists.intro, Top.top
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
h : Nontrivial V
refine_2 : Ne.{u_3 + 1} (α := ↥ρ.invtSubmodule) ⊥ ⊤
⊢ Nontrivial.{u_3} ↥ρ.invtSubmodule

Tactic:
refine ⟨⊥, ⊤, ?_⟩
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
h : Nontrivial V
refine_2 : Ne.{u_3 + 1} (α := Submodule k V) ⊥ ⊤
⊢ Ne.{u_3 + 1} (α := ↥ρ.invtSubmodule) ⊥ ⊤

Tactic:
rw [← Subtype.coe_ne_coe, invtSubmodule.coe_top, invtSubmodule.coe_bot]

Premises used: Representation.invtSubmodule.coe_top, Representation.invtSubmodule.coe_bot, Subtype.coe_ne_coe
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
h : Nontrivial V
⊢ Ne.{u_3 + 1} (α := Submodule k V) ⊥ ⊤

Tactic:
bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
h : Nontrivial V
⊢ Ne.{u_3 + 1} (α := Submodule k V) ⊥ ⊤

Tactic:
exact bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
inst_4 : Nontrivial V
⊢ Nontrivial.{u_3} ↥ρ.invtSubmodule

Tactic:
(invtSubmodule.nontrivial_iff ρ).mpr inferInstance

Premises used: Iff.mpr, Representation.invtSubmodule.nontrivial_iff, inferInstance
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, Membership.mem (α := V) p ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V)
v : V
hv : v ∈ p
x : k[G]
hM :
  ∀ (m : G),
    Membership.mem (α := V) p
      ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) ((MonoidAlgebra.of k G : (a : G) → k[G]) m) : Module.End k V) :
            (a : V) → V)
          v :
        V)
hadd :
  ∀ (x y : k[G]),
    Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V) →
      Membership.mem (α := V) p
          ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) y : Module.End k V) : (a : V) → V) v : V) →
        Membership.mem (α := V) p
          ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (x + y) : Module.End k V) : (a : V) → V) v : V)
hsmul :
  ∀ (r : k) (x : k[G]),
    Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V) →
      Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (r • x) : Module.End k V) : (a : V) → V) v : V)
⊢ Membership.mem (α := V) p ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V)

Tactic:
apply x.induction_on

Premises used: MonoidAlgebra.induction_on
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, Membership.mem (α := V) p ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V)
v : V
hv : v ∈ p
x : k[G]
⊢ ∀ (m : G),
    Membership.mem (α := V) p
      ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) ((MonoidAlgebra.of k G : (a : G) → k[G]) m) : Module.End k V) :
            (a : V) → V)
          v :
        V)

Tactic:
aesop
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, Membership.mem (α := V) p ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V)
v : V
hv : v ∈ p
x : k[G]
⊢ ∀ (x y : k[G]),
    Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V) →
      Membership.mem (α := V) p
          ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) y : Module.End k V) : (a : V) → V) v : V) →
        Membership.mem (α := V) p
          ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (x + y) : Module.End k V) : (a : V) → V) v : V)

Tactic:
aesop
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, Membership.mem (α := V) p ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V)
v : V
hv : v ∈ p
x : k[G]
⊢ ∀ (r : k) (x : k[G]),
    Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V) →
      Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (r • x) : Module.End k V) : (a : V) → V) v : V)

Tactic:
aesop
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : ↥ρ.invtSubmodule
simp :
  ∀ (c : k[G]),
    ∀ a ∈ (↑p : Submodule k V),
      ∃ x ∈ (↑p : Submodule k V),
        (ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x =
          HSMul.hSMul (β := ρ.asModule) c ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) a : ρ.asModule)
⊢ ∀ (c : k[G]) {x : ρ.asModule},
    x ∈
        AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid)) →
      c • x ∈
        AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid))

Tactic:
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
          AddSubmonoid.mem_map, Submodule.mem_toAddSubmonoid, forall_exists_index, and_imp,
          forall_apply_eq_imp_iff₂]

Premises used: and_imp, AddSubmonoid.mem_map, forall_exists_index, AddSubsemigroup.mem_carrier, Submodule.mem_toAddSubmonoid, forall_apply_eq_imp_iff₂, AddSubmonoid.mem_toSubsemigroup
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : ↥ρ.invtSubmodule
⊢ ∀ (c : k[G]),
    ∀ a ∈ (↑p : Submodule k V),
      ∃ x ∈ (↑p : Submodule k V),
        (ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x =
          HSMul.hSMul (β := ρ.asModule) c ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) a : ρ.asModule)

Tactic:
fun x v hv ↦ ⟨ρ.asModuleEquiv (x • ρ.asModuleEquiv.symm v), ?_, rfl⟩

Premises used: LinearEquiv.symm, And.intro, Exists.intro, Representation.asModuleEquiv, HSMul.hSMul, DFunLike.coe, rfl
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : ↥ρ.invtSubmodule
refine :
  ∀ (x : k[G]) (v : V) (hv : v ∈ (↑p : Submodule k V)),
    Membership.mem (α := V) (↑p : Submodule k V)
      ((ρ.asModuleEquiv : (a : ρ.asModule) → V)
          (HSMul.hSMul (β := ρ.asModule) x ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) v : ρ.asModule)) :
        V)
⊢ ∀ (c : k[G]),
    ∀ a ∈ (↑p : Submodule k V),
      ∃ x ∈ (↑p : Submodule k V),
        (ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x =
          HSMul.hSMul (β := ρ.asModule) c ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) a : ρ.asModule)

Tactic:
refine fun x v hv ↦ ⟨ρ.asModuleEquiv (x • ρ.asModuleEquiv.symm v), ?_, rfl⟩