awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial.{u} ↥N
have : ∀ (w : Submodule R M) (compl : IsCompl N w), ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
have ⟨_, compl⟩ := exists_isCompl N
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial.{u} ↥N
w : Submodule R M
compl : IsCompl N w
have :
  ∀ (m : Submodule R M) (hm : m ∈ s) (ne : N.projectionOnto w compl ∘ₗ m.subtype ≠ 0),
    ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
have ⟨m, hm, ne⟩ := exists_ne_zero_of_sSup_eq_top (ne_zero_of_surjective
    (projectionOnto_surjective compl)) _ hs
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial.{u} ↥N
w : Submodule R M
compl : IsCompl N w
m : Submodule R M
hm : m ∈ s
ne : N.projectionOnto w compl ∘ₗ m.subtype ≠ 0
have : ∀ (S : Submodule R ↥m) (e : ↥N ≃ₗ[R] ↥S), ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
have ⟨S, ⟨e⟩⟩ := linearEquiv_of_ne_zero ne
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial.{u} ↥N
w : Submodule R M
compl : IsCompl N w
m : Submodule R M
hm : m ∈ s
ne : N.projectionOnto w compl ∘ₗ m.subtype ≠ 0
S : Submodule R ↥m
e : ↥N ≃ₗ[R] ↥S
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
⟨m, hm, _, m.map_subtype_le S, ⟨e.trans (S.equivMapOfInjective _ m.subtype_injective)⟩⟩

Premises used: Submodule.equivMapOfInjective, Nonempty.intro, And.intro, Exists.intro, Submodule.subtype_injective, LinearEquiv.trans, Submodule.map_subtype_le
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial.{u} ↥N
w : Submodule R M
compl : IsCompl N w
m : Submodule R M
hm : m ∈ s
ne : N.projectionOnto w compl ∘ₗ m.subtype ≠ 0
S : Submodule R ↥m
e : ↥N ≃ₗ[R] ↥S
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
exact ⟨m, hm, _, m.map_subtype_le S, ⟨e.trans (S.equivMapOfInjective _ m.subtype_injective)⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
h : ∀ (m : (↑s : Type u)), IsSimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hs : sSup s = ⊤
⊢ ∃ S ∈ s, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
have := isSemisimpleModule_of_isSemisimpleModule_submodule' (fun _ ↦ inferInstance)
    (sSup_eq_iSup' s ▸ hs)
  have ⟨m, hm, _S, le, ⟨e⟩⟩ := N.le_linearEquiv_of_sSup_eq_top _ hs
  have := isSimpleModule_iff_isAtom.mp (IsSimpleModule.congr e.symm)
  have := ((isSimpleModule_iff_isAtom.mp <| h ⟨m, hm⟩).le_iff_eq this.1).mp le
  ⟨m, hm, ⟨e.trans (.ofEq _ _ this)⟩⟩

Premises used: LinearEquiv.symm, Submodule.le_linearEquiv_of_sSup_eq_top, isSimpleModule_iff_isAtom, Membership.mem, Exists, inferInstance, Subtype, LinearEquiv.ofEq, Nonempty.intro, Subtype.mk, _private.0.Submodule.linearEquiv_of_sSup_eq_top.match_1, And, isSemisimpleModule_of_isSemisimpleModule_submodule', And.left, And.intro, LinearEquiv, Exists.intro, Iff.mp, Nonempty, IsAtom.le_iff_eq, RingHom.id, LinearEquiv.trans, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ sSup s
⊢ N ≤ ⨆ a ∈ s, a

Tactic:
rw [sSup_eq_iSup] at hN

Premises used: sSup_eq_iSup
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
have : ∀ (e : ↥N ≃ₗ[R] ↥(inclusion hN).range), ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
have e := LinearEquiv.ofInjective _ (inclusion_injective hN)
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
⊢ IsSimpleModule.{u_2, u} R ↥(inclusion hN).range

Tactic:
have := IsSimpleModule.congr e.symm
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
⊢ IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)

Tactic:
have := isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m hm ↦ hs ⟨m, hm⟩
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this_1 : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
this : IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)
rw : Eq.{u + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) (⨆ a ∈ s, comap (Submodule.subtype (⨆ i ∈ s, i)) a) ⊤
rw₁ rw₂ : Eq.{u + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) ⊤ ⊤
⊢ Eq (α := Submodule R ↥(⨆ a ∈ s, a)) (sSup (comap (Submodule.subtype (⨆ i ∈ s, i)) '' s)) ⊤

Tactic:
rw [sSup_image, biSup_comap_subtype_eq_top]

Premises used: Submodule.biSup_comap_subtype_eq_top, sSup_image
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this_1 : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
this : IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)
obtain :
  ∀ (m : Submodule R M) (hm : m ∈ s) (S : Submodule R ↥(⨆ a ∈ s, a)) (le : S ≤ comap (Submodule.subtype (⨆ i ∈ s, i)) m)
    (e' : ↥(inclusion hN).range ≃ₗ[R] ↥S), ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
obtain ⟨_, ⟨m, hm, rfl⟩, S, le, ⟨e'⟩⟩ := LinearMap.range (inclusion hN)
      |>.le_linearEquiv_of_sSup_eq_top (comap (⨆ i ∈ s, i).subtype '' s) <| by
    rw [sSup_image, biSup_comap_subtype_eq_top]

Premises used: Submodule.le_linearEquiv_of_sSup_eq_top, iSup, LinearMap.range, Submodule.inclusion, Submodule.comap, Submodule.subtype, Set.image, rfl
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this_1 : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
this : IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)
m : Submodule R M
hm : m ∈ s
S : Submodule R ↥(⨆ a ∈ s, a)
le : S ≤ comap (Submodule.subtype (⨆ i ∈ s, i)) m
e' : ↥(inclusion hN).range ≃ₗ[R] ↥S
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
⟨m, hm, _, map_le_iff_le_comap.mpr le,
    ⟨(e.trans e').trans (equivMapOfInjective _ (subtype_injective _) _)⟩⟩

Premises used: Iff.mpr, Submodule.equivMapOfInjective, Nonempty.intro, And.intro, Exists.intro, Submodule.map_le_iff_le_comap, Submodule.subtype_injective, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this_1 : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
this : IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)
m : Submodule R M
hm : m ∈ s
S : Submodule R ↥(⨆ a ∈ s, a)
le : S ≤ comap (Submodule.subtype (⨆ i ∈ s, i)) m
e' : ↥(inclusion hN).range ≃ₗ[R] ↥S
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
exact ⟨m, hm, _, map_le_iff_le_comap.mpr le,
    ⟨(e.trans e').trans (equivMapOfInjective _ (subtype_injective _) _)⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
simple : ∀ (m : (↑s : Type u)), IsSimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hs : N ≤ sSup s
⊢ ∃ S ∈ s, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)

Tactic:
have ⟨m, hm, _S, le, ⟨e⟩⟩ := N.le_linearEquiv_of_le_sSup _ hs
  have := isSimpleModule_iff_isAtom.mp (.congr e.symm)
  have := ((isSimpleModule_iff_isAtom.mp <| simple ⟨m, hm⟩).le_iff_eq this.1).mp le
  ⟨m, hm, ⟨e.trans (.ofEq _ _ this)⟩⟩

Premises used: LinearEquiv.symm, isSimpleModule_iff_isAtom, Membership.mem, Exists, Subtype, Submodule.le_linearEquiv_of_le_sSup, LinearEquiv.ofEq, Nonempty.intro, Subtype.mk, _private.0.Submodule.linearEquiv_of_sSup_eq_top.match_1, And, And.left, And.intro, LinearEquiv, Exists.intro, Iff.mp, Nonempty, IsAtom.le_iff_eq, RingHom.id, LinearEquiv.trans, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : IsSimpleModule R S
m : (↑{m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} : Type u)
⊢ IsSimpleModule.{u_2, u} R ↥(↑m : Submodule R M)

Tactic:
.congr m.2.some

Premises used: Nonempty.some, Subtype.property, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
inst_5 : IsSimpleModule R S
⊢ IsIsotypicOfType.{u, u_2, u_4} R (↥(isotypicComponent R M S)) S

Tactic:
isIsotypicOfType_submodule_iff.mpr fun m h _ ↦
    have ⟨_, ⟨e⟩, ⟨e'⟩⟩ := m.linearEquiv_of_le_sSup _ h
    ⟨e'.trans e⟩

Premises used: _private.0.IsIsotypicOfType.isotypicComponent.match_1, Iff.mpr, Submodule.linearEquiv_of_le_sSup, isIsotypicOfType_submodule_iff, setOf, Membership.mem, Subtype, Nonempty.intro, LinearEquiv, Nonempty, RingHom.id, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
inst_5 : IsSimpleModule R S
⊢ IsIsotypic.{u, u_2} R ↥(isotypicComponent R M S)

Tactic:
(IsIsotypicOfType.isotypicComponent R M S).isIsotypic

Premises used: IsIsotypicOfType.isIsotypic, IsIsotypicOfType.isotypicComponent
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : Submodule R M
h : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) m
obtain : ∀ (w : Submodule R M), IsSimpleModule.{u_2, u} R ↥w → IsIsotypic.{u, u_2} R ↥(isotypicComponent R M ↥w)
⊢ IsIsotypic.{u, u_2} R ↥m

Tactic:
obtain ⟨_, _, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
w : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥w
⊢ IsIsotypic.{u, u_2} R ↥(isotypicComponent R M ↥w)

Tactic:
.isotypicComponent R M _

Premises used: IsIsotypic.isotypicComponent
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
w : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥w
⊢ IsIsotypic.{u, u_2} R ↥(isotypicComponent R M ↥w)

Tactic:
exact .isotypicComponent R M _
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
inst_3 : IsSimpleModule.{u_2, u} R ↥S
le : S ≤ c
obtain :
  ∀ (S' : Submodule R M),
    IsSimpleModule.{u_2, u} R ↥S' →
      ∀ (le : S ≤ isotypicComponent R M ↥S'),
        Eq (α := Submodule R M) (isotypicComponent R M ↥S') (isotypicComponent R M ↥S)
⊢ c = isotypicComponent R M ↥S

Tactic:
obtain ⟨S', _, rfl⟩ := hc

Premises used: rfl
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥S'
le : S ≤ isotypicComponent R M ↥S'
have : ∀ (e : ↥S ≃ₗ[R] ↥S'), Eq (α := Submodule R M) (isotypicComponent R M ↥S') (isotypicComponent R M ↥S)
⊢ Eq (α := Submodule R M) (isotypicComponent R M ↥S') (isotypicComponent R M ↥S)

Tactic:
have ⟨e⟩ := isIsotypicOfType_submodule_iff.mp (.isotypicComponent R M S') _ le
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥S'
le : S ≤ isotypicComponent R M ↥S'
e : ↥S ≃ₗ[R] ↥S'
⊢ Eq (α := Submodule R M) (isotypicComponent R M ↥S') (isotypicComponent R M ↥S)

Tactic:
e.symm.isotypicComponent_eq

Premises used: LinearEquiv.symm, LinearEquiv.isotypicComponent_eq
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥S'
le : S ≤ isotypicComponent R M ↥S'
e : ↥S ≃ₗ[R] ↥S'
⊢ Eq (α := Submodule R M) (isotypicComponent R M ↥S') (isotypicComponent R M ↥S)

Tactic:
exact e.symm.isotypicComponent_eq

Premises used: LinearEquiv.symm, LinearEquiv.isotypicComponent_eq
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
ne : ¬c ⊓ sSup (isotypicComponents R M \ {c}) = ⊥
⊢ let s : Set (Submodule R M) := isotypicComponents R M \ {c};
  ¬c ⊓ sSup s = ⊥

Tactic:
set s := isotypicComponents R M \ {c}

Premises used: isotypicComponents
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
obtain :
  ∀ (S : Submodule R M),
    IsSimpleModule.{u_2, u} R ↥S →
      let s : Set (Submodule R M) := isotypicComponents R M \ {isotypicComponent R M ↥S};
      ∀ (ne : ¬isotypicComponent R M ↥S ⊓ sSup s = ⊥), IsSemisimpleModule.{u_2, u} R ↥(isotypicComponent R M ↥S)
⊢ IsSemisimpleModule.{u_2, u} R ↥c

Tactic:
obtain ⟨S, _, rfl⟩ := hc

Premises used: rfl
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥S
s : Set (Submodule R M) := isotypicComponents R M \ {isotypicComponent R M ↥S}
ne : ¬isotypicComponent R M ↥S ⊓ sSup s = ⊥
⊢ IsSemisimpleModule.{u_2, u} R ↥(isotypicComponent R M ↥S)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
⊢ IsSemisimpleModule.{u_2, u} R ↥c

Tactic:
have : IsSemisimpleModule R c := by obtain ⟨S, _, rfl⟩ := hc; infer_instance
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this : IsSemisimpleModule.{u_2, u} R ↥c
⊢ IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)

Tactic:
have := IsSemisimpleModule.of_injective _
      (Submodule.inclusion_injective (inf_le_left : c ⊓ sSup s ≤ c))
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c_1 : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c_1
s : Set (Submodule R M) := isotypicComponents R M \ {c_1}
ne : ¬c_1 ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c_1
this : IsSemisimpleModule.{u_2, u} R ↥(c_1 ⊓ sSup s)
c : (↑s : Type u)
obtain :
  ∀ (w : Submodule R M) (left : IsSimpleModule.{u_2, u} R ↥w) (right : isotypicComponent R M ↥w ∉ {c_1}),
    IsSemisimpleModule.{u_2, u} R
      ↥(↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ s) (isotypicComponent R M ↥w) ⋯) : Submodule R M)
⊢ IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)

Tactic:
obtain ⟨_, ⟨_, _, rfl⟩, _⟩ := c

Premises used: rfl
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
w : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥w
right : isotypicComponent R M ↥w ∉ {c}
⊢ IsSemisimpleModule.{u_2, u} R
    ↥(↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ s) (isotypicComponent R M ↥w) ⋯) : Submodule R M)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
⊢ ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)

Tactic:
have (c : s) : IsSemisimpleModule R c := by obtain ⟨_, ⟨_, _, rfl⟩, _⟩ := c; infer_instance
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
have : ∀ (S : Submodule R M) (le : S ≤ c ⊓ sSup s), IsSimpleModule.{u_2, u} R ↥S → False
⊢ False

Tactic:
have ⟨S, le, _⟩ := (IsSemisimpleModule.eq_bot_or_exists_simple_le _).resolve_left ne
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
have : ∀ (c' : Submodule R M) (hc' : c' ∈ s) (S' : Submodule R M) (le' : S' ≤ c') (e : ↥S ≃ₗ[R] ↥S'), False
⊢ False

Tactic:
have ⟨c', hc', S', le', ⟨e⟩⟩ := S.le_linearEquiv_of_le_sSup _ (le.trans inf_le_right)
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
⊢ IsSimpleModule.{u_2, u} R ↥S'

Tactic:
have := IsSimpleModule.congr e.symm
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this_3 : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule.{u_2, u} R ↥S'
⊢ False

Tactic:
hc'.2 ?_

Premises used: And.right
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this_3 : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule.{u_2, u} R ↥S'
refine : Membership.mem (γ := Set (Submodule R M)) {c} c'
⊢ False

Tactic:
refine hc'.2 ?_

Premises used: And.right