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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
have : ∀ (p : M →ₗ[R] M) (eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')), S' ≤ m
⊢ S' ≤ m

Tactic:
have ⟨p, eq⟩ := extension_property _ S.subtype_injective (S'.subtype ∘ₗ 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
⊢ S' ≤ m

Tactic:
le_trans ?_ (Submodule.map_le_iff_le_comap.mpr (le.trans (h p)))

Premises used: Iff.mpr, LE.le.trans, Submodule.map_le_iff_le_comap, le_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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
refine : S' ≤ Submodule.map p S
⊢ S' ≤ m

Tactic:
refine le_trans ?_ (Submodule.map_le_iff_le_comap.mpr (le.trans (h p)))

Premises used: Iff.mpr, LE.le.trans, Submodule.map_le_iff_le_comap, le_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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
rw : S' ≤ Submodule.map p S.subtype.range
rw₁ : S' ≤ (p ∘ₗ S.subtype).range
rw₂ : S' ≤ (S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')).range
rw₃ : S' ≤ S'.subtype.range
rw₄ rw₅ : S' ≤ S'
⊢ S' ≤ Submodule.map p S

Tactic:
rw [← S.range_subtype, ← LinearMap.range_comp, eq, e.symm.range_comp, S'.range_subtype]

Premises used: LinearEquiv.symm, LinearEquiv.range_comp, LinearMap.range_comp, Submodule.range_subtype
-- 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
inst_6 : IsSemisimpleModule R M
ne : Ne (α := Submodule R M) (isotypicComponent R M S) ⊥
⊢ IsIsotypicOfType.{u, u_2, u_4} R (↥(isotypicComponent R M S)) S ∧ Submodule.IsFullyInvariant (isotypicComponent R M S)

Tactic:
⟨.isotypicComponent R M S, .isotypicComponent R M S⟩

Premises used: Submodule.IsFullyInvariant.isotypicComponent, And.intro, IsIsotypicOfType.isotypicComponent
-- 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
inst_6 : IsSemisimpleModule R M
ne : Ne (α := Submodule R M) (isotypicComponent R M S) ⊥
⊢ IsIsotypicOfType.{u, u_2, u_4} R (↥(isotypicComponent R M S)) S ∧ Submodule.IsFullyInvariant (isotypicComponent R M S)

Tactic:
exact ⟨.isotypicComponent R M S, .isotypicComponent R M S⟩
-- 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
inst_3 : IsSemisimpleModule R M
S : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥S
⊢ IsIsotypic.{u, u_2} R ↥(isotypicComponent R M ↥S) ∧
    Submodule.IsFullyInvariant (isotypicComponent R M ↥S) ∧ Ne (α := Submodule R M) (isotypicComponent R M ↥S) ⊥

Tactic:
⟨.isotypicComponent R M S,
    .isotypicComponent R M S, (bot_lt_isotypicComponent S).ne'⟩

Premises used: bot_lt_isotypicComponent, Submodule.IsFullyInvariant.isotypicComponent, IsIsotypic.isotypicComponent, Membership.mem, Subtype, LT.lt.ne', And.intro
-- 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
inst_3 : IsSemisimpleModule R M
S : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥S
⊢ IsIsotypic.{u, u_2} R ↥(isotypicComponent R M ↥S) ∧
    Submodule.IsFullyInvariant (isotypicComponent R M ↥S) ∧ Ne (α := Submodule R M) (isotypicComponent R M ↥S) ⊥

Tactic:
exact ⟨.isotypicComponent R M S,
    .isotypicComponent R M S, (bot_lt_isotypicComponent S).ne'⟩
-- 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 : IsSemisimpleModule R M
m : ↥(fullyInvariantSubmodule R M)
x : (↑(isotypicComponents R M) : Type u)
⊢ ∀
    (j :
      Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
        ((fun (m : ↥(fullyInvariantSubmodule R M)) ↦
            ({c : (↑(isotypicComponents R M) : Type u) | (↑c : Submodule R M) ≤ (↑m : Submodule R M)} :
              Set (↑(isotypicComponents R M) : Type u)))
          m)
        x),
    Subtype.mk (p := fun (x : Submodule R M) ↦
        Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) (↑x : Submodule R M)
        ⋯ ≤
      m

Tactic:
id

Premises used: Set.Mem, setOf, id
-- 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 : IsSemisimpleModule R M
m : ↥(fullyInvariantSubmodule R M)
x : (↑(isotypicComponents R M) : Type u)
⊢ ∀
    (j :
      Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
        ((fun (m : ↥(fullyInvariantSubmodule R M)) ↦
            ({c : (↑(isotypicComponents R M) : Type u) | (↑c : Submodule R M) ≤ (↑m : Submodule R M)} :
              Set (↑(isotypicComponents R M) : Type u)))
          m)
        x),
    Subtype.mk (p := fun (x : Submodule R M) ↦
        Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) (↑x : Submodule R M)
        ⋯ ≤
      m

Tactic:
exact id

Premises used: id
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S_1 : 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_1
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S_1
inst_9 : IsSemisimpleModule R M
m : ↥(fullyInvariantSubmodule R M)
S : Submodule R M
h :
  Membership.mem (γ := Set (Submodule R M))
    {m_1 : Submodule R M | IsSimpleModule.{u_2, u} R ↥m_1 ∧ m_1 ≤ (↑m : Submodule R M)} S
simple : IsSimpleModule.{u_2, u} R ↥S
le : S ≤ (↑m : Submodule R M)
c : (↑(isotypicComponents R M) : Type u) :=
  Subtype.mk (p := fun (x : Submodule R M) ↦ Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x)
    (isotypicComponent R M ↥S) ⋯
simp_rw :
  (↑c : Submodule R M) ≤
    ⨆ (i : (↑(isotypicComponents R M) : Type u)),
      ⨆ (_ :
        Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
          {c : (↑(isotypicComponents R M) : Type u) | (↑c : Submodule R M) ≤ (↑m : Submodule R M)} i),
        (↑i : Submodule R M)
⊢ LE.le (α := Submodule R M) (isotypicComponent R M ↥S)
    (↑(⨆ (i : (↑(isotypicComponents R M) : Type u)),
          ⨆ (_ :
            Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
              ((fun (m : ↥(fullyInvariantSubmodule R M)) ↦
                  ({c : (↑(isotypicComponents R M) : Type u) | (↑c : Submodule R M) ≤ (↑m : Submodule R M)} :
                    Set (↑(isotypicComponents R M) : Type u)))
                m)
              i),
            Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x)
              (↑i : Submodule R M) ⋯) :
      Submodule R M)

Tactic:
simp_rw [← show c.1 = isotypicComponent R M S from rfl, CompleteSublattice.coe_iSup]

Premises used: CompleteSublattice.coe_iSup, rfl
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S_1 : 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_1
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S_1
inst_9 : IsSemisimpleModule R M
m : ↥(fullyInvariantSubmodule R M)
S : Submodule R M
h :
  Membership.mem (γ := Set (Submodule R M))
    {m_1 : Submodule R M | IsSimpleModule.{u_2, u} R ↥m_1 ∧ m_1 ≤ (↑m : Submodule R M)} S
simple : IsSimpleModule.{u_2, u} R ↥S
le : S ≤ (↑m : Submodule R M)
c : (↑(isotypicComponents R M) : Type u) :=
  Subtype.mk (p := fun (x : Submodule R M) ↦ Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x)
    (isotypicComponent R M ↥S) ⋯
⊢ (↑c : Submodule R M) ≤
    ⨆ (i : (↑(isotypicComponents R M) : Type u)),
      ⨆ (_ :
        Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
          {c : (↑(isotypicComponents R M) : Type u) | (↑c : Submodule R M) ≤ (↑m : Submodule R M)} i),
        (↑i : Submodule R M)

Tactic:
le_biSup _ (isFullyInvariant_iff_le_imp_isotypicComponent_le.mp m.2 _ le)

Premises used: Set.Mem, setOf, Iff.mp, le_biSup, isFullyInvariant_iff_le_imp_isotypicComponent_le, Subtype.property
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S_1 : 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_1
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S_1
inst_9 : IsSemisimpleModule R M
m : ↥(fullyInvariantSubmodule R M)
S : Submodule R M
h :
  Membership.mem (γ := Set (Submodule R M))
    {m_1 : Submodule R M | IsSimpleModule.{u_2, u} R ↥m_1 ∧ m_1 ≤ (↑m : Submodule R M)} S
simple : IsSimpleModule.{u_2, u} R ↥S
le : S ≤ (↑m : Submodule R M)
c : (↑(isotypicComponents R M) : Type u) :=
  Subtype.mk (p := fun (x : Submodule R M) ↦ Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x)
    (isotypicComponent R M ↥S) ⋯
⊢ (↑c : Submodule R M) ≤
    ⨆ (i : (↑(isotypicComponents R M) : Type u)),
      ⨆ (_ :
        Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
          {c : (↑(isotypicComponents R M) : Type u) | (↑c : Submodule R M) ≤ (↑m : Submodule R M)} i),
        (↑i : Submodule R M)

Tactic:
exact le_biSup _ (isFullyInvariant_iff_le_imp_isotypicComponent_le.mp m.2 _ le)

Premises used: le_biSup
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
⊢ m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s

Tactic:
⟨fun h ↦ ⟨OrderIso.setIsotypicComponents.symm ⟨m, h⟩, ⟨?_, ?_⟩⟩, ?_⟩

Premises used: OrderIso.setIsotypicComponents, OrderIso.symm, Subtype.mk, And.intro, Iff.intro, Exists.intro, Set.image, Subtype.val, DFunLike.coe
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
refine_1 :
  ∀ (h : m.IsFullyInvariant),
    Subset (α := Set (Submodule R M))
      (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
        (Subtype.val (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
        ((OrderIso.symm OrderIso.setIsotypicComponents :
            (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))
      (isotypicComponents R M)
refine_2 :
  ∀ (h : m.IsFullyInvariant),
    m =
      sSup
        (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
          (Subtype.val (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
          ((OrderIso.symm OrderIso.setIsotypicComponents :
              (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))
refine_3 : (∃ s ⊆ isotypicComponents R M, m = sSup s) → m.IsFullyInvariant
⊢ m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s

Tactic:
refine ⟨fun h ↦ ⟨OrderIso.setIsotypicComponents.symm ⟨m, h⟩, ⟨?_, ?_⟩⟩, ?_⟩
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
c : { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x }
left :
  Membership.mem (γ :=
    Set { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
    ((OrderIso.symm OrderIso.setIsotypicComponents :
          (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h) :
      Set (↑(isotypicComponents R M) : Type u))
    c
⊢ Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) (↑c : Submodule R M)

Tactic:
c.2

Premises used: Subtype.property
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
c : { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x }
left :
  Membership.mem (γ :=
    Set { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
    ((OrderIso.symm OrderIso.setIsotypicComponents :
          (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h) :
      Set (↑(isotypicComponents R M) : Type u))
    c
⊢ Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) (↑c : Submodule R M)

Tactic:
exact c.2

Premises used: Subtype.property
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h) :
      Submodule R M) =
    (↑(Equiv.toFun
          (RelIso.toEquiv (r := fun (x1 x2 : Set (↑(isotypicComponents R M) : Type u)) ↦ x1 ≤ x2) (s :=
            fun (x1 x2 : ↥(fullyInvariantSubmodule R M)) ↦ x1 ≤ x2) OrderIso.setIsotypicComponents)
          (Equiv.invFun
            (RelIso.toEquiv (r := fun (x1 x2 : Set (↑(isotypicComponents R M) : Type u)) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : ↥(fullyInvariantSubmodule R M)) ↦ x1 ≤ x2) OrderIso.setIsotypicComponents)
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h))) :
      Submodule R M)

Tactic:
Subtype.ext_iff.mp (OrderIso.setIsotypicComponents.right_inv ⟨m, h⟩).symm

Premises used: Equiv.right_inv, OrderIso.setIsotypicComponents, Subtype.ext_iff, Subtype.mk, Iff.mp, RelIso.toEquiv, Eq.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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
h₁ :
  sSup
      (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
        (Subtype.val (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
        ((OrderIso.symm OrderIso.setIsotypicComponents :
            (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h))) =
    (↑(Equiv.toFun
          (RelIso.toEquiv (r := fun (x1 x2 : Set (↑(isotypicComponents R M) : Type u)) ↦ x1 ≤ x2) (s :=
            fun (x1 x2 : ↥(fullyInvariantSubmodule R M)) ↦ x1 ≤ x2) OrderIso.setIsotypicComponents)
          (Equiv.invFun
            (RelIso.toEquiv (r := fun (x1 x2 : Set (↑(isotypicComponents R M) : Type u)) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : ↥(fullyInvariantSubmodule R M)) ↦ x1 ≤ x2) OrderIso.setIsotypicComponents)
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h))) :
      Submodule R M)
⊢ m =
    sSup
      (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
        (Subtype.val (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
        ((OrderIso.symm OrderIso.setIsotypicComponents :
            (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))

Tactic:
convert! Subtype.ext_iff.mp (OrderIso.setIsotypicComponents.right_inv ⟨m, h⟩).symm

Premises used: Equiv.right_inv, OrderIso.setIsotypicComponents, Subtype.ext_iff, Subtype.mk, Iff.mp, RelIso.toEquiv, Eq.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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ sSup
      (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
        (Subtype.val (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
        ((OrderIso.symm OrderIso.setIsotypicComponents :
            (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h))) =
    (↑(Equiv.toFun
          (RelIso.toEquiv (r := fun (x1 x2 : Set (↑(isotypicComponents R M) : Type u)) ↦ x1 ≤ x2) (s :=
            fun (x1 x2 : ↥(fullyInvariantSubmodule R M)) ↦ x1 ≤ x2) OrderIso.setIsotypicComponents)
          (Equiv.invFun
            (RelIso.toEquiv (r := fun (x1 x2 : Set (↑(isotypicComponents R M) : Type u)) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : ↥(fullyInvariantSubmodule R M)) ↦ x1 ≤ x2) OrderIso.setIsotypicComponents)
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h))) :
      Submodule R M)

Tactic:
simp [sSup_image, OrderIso.setIsotypicComponents, OrderIso.symm]

Premises used: OrderIso.setIsotypicComponents, OrderIso.symm, 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
inst_3 : IsSemisimpleModule R M
w : Set (Submodule R M)
hs : w ⊆ isotypicComponents R M
⊢ (sSup w).IsFullyInvariant

Tactic:
(fullyInvariantSubmodule R M).sSupClosed fun _ h ↦ .of_mem_isotypicComponents (hs h)

Premises used: Set.Mem, setOf, CompleteSublattice.sSupClosed, Submodule.IsFullyInvariant.of_mem_isotypicComponents, Submodule.IsFullyInvariant
-- 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
inst_3 : IsSemisimpleModule R M
w : Set (Submodule R M)
hs : w ⊆ isotypicComponents R M
⊢ (sSup w).IsFullyInvariant

Tactic:
exact (fullyInvariantSubmodule R M).sSupClosed fun _ h ↦ .of_mem_isotypicComponents (hs h)

Premises used: CompleteSublattice.sSupClosed, Submodule.IsFullyInvariant.of_mem_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
inst_3 : IsSemisimpleModule R M
⊢ Eq (α := Submodule R M) (sSup (isotypicComponents R M)) ⊤

Tactic:
have ⟨_, h, eq⟩ := isFullyInvariant_iff_sSup_isotypicComponents.mp
    (fullyInvariantSubmodule R M).top_mem
  top_unique <| eq.le.trans (sSup_le_sSup h)

Premises used: isFullyInvariant_iff_sSup_isotypicComponents, CompleteSublattice.top_mem, _private.0.sSup_isotypicComponents.match_1, Eq.le, top_unique, Iff.mp, LE.le.trans, Top.top, Eq, sSup_le_sSup, SupSet.sSup, isotypicComponents
-- Module: Mathlib.RingTheory.SimpleModule.Rank
Goal:
R : Type u_1
M : Type u_2
inst : DivisionRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsSimpleModule R M ↔ Module.finrank R M = 1

Tactic:
⟨fun h ↦ have := h.nontrivial; have ⟨v, hv⟩ := exists_ne (0 : M)
    (finrank_eq_one_iff_of_nonzero' v hv).mpr (IsSimpleModule.toSpanSingleton_surjective R hv),
  (isSimpleModule_iff ..).mpr ∘ is_simple_module_of_finrank_eq_one⟩

Premises used: Iff.mpr, _private.0.isSimpleModule_iff_finrank_eq_one.match_1, IsSimpleModule.nontrivial, IsSimpleModule.toSpanSingleton_surjective, Function.comp, exists_ne, isSimpleModule_iff, Iff.intro, is_simple_module_of_finrank_eq_one, OfNat.ofNat, Eq, finrank_eq_one_iff_of_nonzero', Module.finrank
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
⊢ IsSemisimpleRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
⊢ IsArtinianRing R

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
⊢ ∀ (a : IsSemisimpleRing R), IsArtinianRing R

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
⊢ ∀ (a : IsSemisimpleRing R), IsArtinianRing R

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
⊢ IsArtinianRing R

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false