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
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
simp_rw :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(({
                      toFun := fun (p' : Submodule R ↥N) ↦
                        Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') ⋯,
                      invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                        Submodule.comap N.subtype (↑q : Submodule R M),
                      left_inv := ⋯, right_inv := ⋯ : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(({
                    toFun := fun (p' : Submodule R ↥N) ↦
                      Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') ⋯,
                    invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                      Submodule.comap N.subtype (↑q : Submodule R M),
                    left_inv := ⋯, right_inv := ⋯ : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
simp_rw₁ :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥(Submodule.map N.subtype a)],
      IsIsotypicOfType.{u, u_2, u} R ↥N ↥(Submodule.map N.subtype a)
simp_rw₂ :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥a],
      IsIsotypicOfType.{u, u_2, u} R ↥N ↥(Submodule.map N.subtype a)
simp_rw₃ :
  IsIsotypic.{u, u_2} R ↥N ↔ ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥a], IsIsotypicOfType.{u, u_2, u} R ↥N ↥a
⊢ IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)

Tactic:
simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff,
    ← (e _).isIsotypicOfType_iff_type, IsIsotypic]

Premises used: Submodule.MapSubtype.orderIso, LinearEquiv.isIsotypicOfType_iff_type, Equiv.coe_fn_mk, LinearEquiv.isSimpleModule_iff, IsIsotypic
-- 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 : IsSemisimpleModule R M
h : IsIsotypicOfType R M S
have :
  ∀ (s : Set (Submodule R M)) (e : M ≃ₗ[R] Π₀ (m : (↑s : Type u)), ↥(↑m : Submodule R M)),
    sSupIndep s →
      ∀ (hs : ∀ (m : (↑s : Type u)), IsSimpleModule.{u_2, u} R ↥(↑m : Submodule R M)),
        ∃ (ι : Type u), Nonempty (M ≃ₗ[R] ι →₀ S)
⊢ ∃ (ι : Type u), Nonempty (M ≃ₗ[R] ι →₀ S)

Tactic:
have ⟨s, e, _, hs⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
-- 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 : IsSemisimpleModule R M
h : IsIsotypicOfType R M S
s : Set (Submodule R M)
e : M ≃ₗ[R] Π₀ (m : (↑s : Type u)), ↥(↑m : Submodule R M)
left : sSupIndep s
hs : ∀ (m : (↑s : Type u)), IsSimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
⊢ ∃ (ι : Type u), Nonempty (M ≃ₗ[R] ι →₀ S)

Tactic:
⟨s, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun m : s ↦ (h m.1).some)
    |>.trans (finsuppLequivDFinsupp R).symm⟩⟩

Premises used: LinearEquiv.symm, Set.Elem, Nonempty.some, Nonempty.intro, finsuppLequivDFinsupp, Exists.intro, DFinsupp.mapRange.linearEquiv, Subtype.val, 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 : IsSemisimpleModule R M
h : IsIsotypicOfType R M S
s : Set (Submodule R M)
e : M ≃ₗ[R] Π₀ (m : (↑s : Type u)), ↥(↑m : Submodule R M)
left : sSupIndep s
hs : ∀ (m : (↑s : Type u)), IsSimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
⊢ ∃ (ι : Type u), Nonempty (M ≃ₗ[R] ι →₀ S)

Tactic:
exact ⟨s, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun m : s ↦ (h m.1).some)
    |>.trans (finsuppLequivDFinsupp R).symm⟩⟩
-- 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 : IsSemisimpleModule R M
h : IsIsotypicOfType R M S
s : Set (Submodule R M)
e : M ≃ₗ[R] Π₀ (m : (↑s : Type u)), ↥(↑m : Submodule R M)
left : sSupIndep s
hs : ∀ (m : (↑s : Type u)), IsSimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
⊢ ∃ (ι : Type u), Nonempty (M ≃ₗ[R] ι →₀ S)

Tactic:
classical exact ⟨s, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun m : s ↦ (h m.1).some)
    |>.trans (finsuppLequivDFinsupp R).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
inst_4 : Nontrivial M
h : IsIsotypic R M
have :
  ∀ (S : Submodule R M) (hS : IsAtom S),
    ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M),
      IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
⊢ ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)

Tactic:
have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule 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
inst_3 : IsSemisimpleModule R M
inst_4 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsAtom S
⊢ IsSimpleModule.{u_2, u} R ↥S

Tactic:
rw [← isSimpleModule_iff_isAtom] at hS

Premises used: isSimpleModule_iff_isAtom
-- 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
inst_4 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
have :
  ∀ (ι : Type u) (e : Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)),
    ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M),
      IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
⊢ ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)

Tactic:
have ⟨ι, e⟩ := (h S).linearEquiv_finsupp
-- 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
inst_4 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
ι : Type u
e : Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
⊢ ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)

Tactic:
⟨ι, (isEmpty_or_nonempty ι).resolve_left fun _ ↦ not_subsingleton _ (e.some.subsingleton),
    S, hS, e⟩

Premises used: isEmpty_or_nonempty, Nonempty.some, Or.resolve_left, LinearEquiv.toAddEquiv, And.intro, Exists.intro, not_subsingleton, AddEquiv.toEquiv, Equiv.subsingleton
-- 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
inst_4 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
ι : Type u
e : Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
⊢ ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)

Tactic:
exact ⟨ι, (isEmpty_or_nonempty ι).resolve_left fun _ ↦ not_subsingleton _ (e.some.subsingleton),
    S, hS, e⟩
-- 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 : IsSemisimpleModule R M
inst_6 : Module.Finite R M
h : IsIsotypicOfType R M S
have :
  ∀ (n : ℕ) (S_1 : Fin n → Submodule R M) (e : M ≃ₗ[R] Π₀ (i : Fin n), ↥(S_1 i))
    (hs : ∀ (i : Fin n), IsSimpleModule.{u_2, u} R ↥(S_1 i)),
    ∃ (n : ℕ), Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) M (Fin n → S))
⊢ ∃ (n : ℕ), Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) M (Fin n → S))

Tactic:
have ⟨n, S, e, hs⟩ := IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp R M
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
S_1 : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S_1
inst_3 : Module R M
inst_4 : Module R S_1
inst_5 : IsSemisimpleModule R M
inst_6 : Module.Finite R M
h : IsIsotypicOfType R M S_1
n : ℕ
S : Fin n → Submodule R M
e : M ≃ₗ[R] Π₀ (i : Fin n), ↥(S i)
hs : ∀ (i : Fin n), IsSimpleModule.{u_2, u} R ↥(S i)
⊢ ∃ (n : ℕ), Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) M (Fin n → S_1))

Tactic:
⟨n, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun i ↦ (h (S i)).some)
    |>.trans (finsuppLequivDFinsupp R).symm |>.trans (Finsupp.linearEquivFunOnFinite ..)⟩⟩

Premises used: LinearEquiv.symm, Finsupp.linearEquivFunOnFinite, Nonempty.some, Nonempty.intro, finsuppLequivDFinsupp, Exists.intro, DFinsupp.mapRange.linearEquiv, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
S_1 : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S_1
inst_3 : Module R M
inst_4 : Module R S_1
inst_5 : IsSemisimpleModule R M
inst_6 : Module.Finite R M
h : IsIsotypicOfType R M S_1
n : ℕ
S : Fin n → Submodule R M
e : M ≃ₗ[R] Π₀ (i : Fin n), ↥(S i)
hs : ∀ (i : Fin n), IsSimpleModule.{u_2, u} R ↥(S i)
⊢ ∃ (n : ℕ), Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) M (Fin n → S_1))

Tactic:
exact ⟨n, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun i ↦ (h (S i)).some)
    |>.trans (finsuppLequivDFinsupp R).symm |>.trans (Finsupp.linearEquivFunOnFinite ..)⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
S_1 : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S_1
inst_3 : Module R M
inst_4 : Module R S_1
inst_5 : IsSemisimpleModule R M
inst_6 : Module.Finite R M
h : IsIsotypicOfType R M S_1
n : ℕ
S : Fin n → Submodule R M
e : M ≃ₗ[R] Π₀ (i : Fin n), ↥(S i)
hs : ∀ (i : Fin n), IsSimpleModule.{u_2, u} R ↥(S i)
⊢ ∃ (n : ℕ), Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) M (Fin n → S_1))

Tactic:
classical exact ⟨n, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun i ↦ (h (S i)).some)
    |>.trans (finsuppLequivDFinsupp R).symm |>.trans (Finsupp.linearEquivFunOnFinite ..)⟩⟩
-- 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
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
have :
  ∀ (S : Submodule R M) (hS : IsAtom S),
    ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)
⊢ ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)

Tactic:
have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule 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
inst_3 : IsSemisimpleModule R M
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsAtom S
⊢ IsSimpleModule.{u_2, u} R ↥S

Tactic:
rw [← isSimpleModule_iff_isAtom] at hS

Premises used: isSimpleModule_iff_isAtom
-- 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
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
have :
  ∀ (n : ℕ) (e : Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)),
    ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)
⊢ ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)

Tactic:
have ⟨n, e⟩ := (h S).linearEquiv_fun
-- 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
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
e : Nonempty.{u + 1} (M ≃ₗ[R] Fin 0 → ↥S)
⊢ False

Tactic:
not_subsingleton _ (e.some.subsingleton)

Premises used: Nonempty.some, LinearEquiv.toAddEquiv, not_subsingleton, AddEquiv.toEquiv, Equiv.subsingleton
-- 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
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
e : Nonempty.{u + 1} (M ≃ₗ[R] Fin 0 → ↥S)
⊢ False

Tactic:
exact not_subsingleton _ (e.some.subsingleton)

Premises used: Nonempty.some, LinearEquiv.toAddEquiv, not_subsingleton, AddEquiv.toEquiv, Equiv.subsingleton
-- 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
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
n : ℕ
e : Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)
⊢ ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)

Tactic:
exact ⟨n, neZero_iff.2 <| by rintro rfl; exact not_subsingleton _ (e.some.subsingleton), S, hS, e⟩
-- 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
inst_4 : Module.Finite.{u_2, u} R ↥m
inst_5 : Nontrivial.{u} ↥m
h : IsIsotypic.{u, u_2} R ↥m
⊢ ∃ (n : ℕ) (_ : NeZero n), ∃ S ≤ m, IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (↥m ≃ₗ[R] Fin n → ↥S)

Tactic:
have ⟨n, hn, S, _, ⟨e⟩⟩ := h.linearEquiv_fun
  let e' := S.equivMapOfInjective _ m.subtype_injective
  ⟨n, hn, _, m.map_subtype_le S, .congr e'.symm, ⟨e.trans <| .piCongrRight fun _ ↦ e'⟩⟩

Premises used: IsIsotypic.linearEquiv_fun, LinearEquiv.symm, Membership.mem, Exists, Subtype, Submodule.equivMapOfInjective, IsSimpleModule, LE.le, Nonempty.intro, And, LinearEquiv.piCongrRight, And.intro, LinearEquiv, Exists.intro, Submodule.subtype, Nonempty, Submodule.map, Submodule.subtype_injective, RingHom.id, _private.0.IsIsotypic.submodule_linearEquiv_fun.match_1, LinearEquiv.trans, Submodule.map_subtype_le, 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
m : Submodule R M
⊢ m ≤ isotypicComponent R M ↥m

Tactic:
le_sSup ⟨.refl ..⟩

Premises used: Set.Mem, Nonempty.intro, LinearEquiv.refl, le_sSup
-- 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
⊢ LT.lt (α := Submodule R M) ⊥ (isotypicComponent R M ↥S)

Tactic:
(bot_lt_iff_ne_bot.mpr <| (S.nontrivial_iff_ne_bot).mp <| IsSimpleModule.nontrivial R S).trans_le
    S.le_isotypicComponent

Premises used: Iff.mpr, IsSimpleModule.nontrivial, Membership.mem, bot_lt_iff_ne_bot, Subtype, Submodule.le_isotypicComponent, Submodule.nontrivial_iff_ne_bot, LT.lt.trans_le, Iff.mp
-- 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 → LT.lt (α := Submodule R M) ⊥ (isotypicComponent R M ↥w)
⊢ ⊥ < 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
⊢ LT.lt (α := Submodule R M) ⊥ (isotypicComponent R M ↥w)

Tactic:
bot_lt_isotypicComponent ..

Premises used: bot_lt_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
⊢ LT.lt (α := Submodule R M) ⊥ (isotypicComponent R M ↥w)

Tactic:
exact bot_lt_isotypicComponent ..

Premises used: bot_lt_isotypicComponent
-- 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
c : (↑(isotypicComponents R M) : Type u)
⊢ Nontrivial.{u} ↥(↑c : Submodule R M)

Tactic:
Submodule.nontrivial_iff_ne_bot.mpr (bot_lt_isotypicComponents c.2).ne'

Premises used: Iff.mpr, LT.lt.ne', Submodule.nontrivial_iff_ne_bot, bot_lt_isotypicComponents, Subtype.property
-- 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 S
rw :
  IsSemisimpleModule.{u_2, u} R
    ↥(⨆ (a : Submodule R M),
        ⨆ (_ :
          Membership.mem (γ := Set (Submodule R M))
            {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} a),
          a)
⊢ IsSemisimpleModule.{u_2, u} R ↥(isotypicComponent R M S)

Tactic:
rw [isotypicComponent, sSup_eq_iSup]

Premises used: isotypicComponent, sSup_eq_iSup
-- 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 S
⊢ IsSemisimpleModule.{u_2, u} R
    ↥(⨆ (a : Submodule R M),
        ⨆ (_ :
          Membership.mem (γ := Set (Submodule R M))
            {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} a),
          a)

Tactic:
isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m ⟨e⟩ ↦ ?_

Premises used: Set.Mem, setOf, Membership.mem, Subtype, IsSemisimpleModule, isSemisimpleModule_biSup_of_isSemisimpleModule_submodule, _private.0.instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent.match_2
-- 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 S
refine :
  ∀ (m : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} m →
      ∀ (e : LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S), IsSemisimpleModule.{u_2, u} R ↥m
⊢ IsSemisimpleModule.{u_2, u} R
    ↥(⨆ (a : Submodule R M),
        ⨆ (_ :
          Membership.mem (γ := Set (Submodule R M))
            {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} a),
          a)

Tactic:
refine isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m ⟨e⟩ ↦ ?_
-- 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 S
m : Submodule R M
h :
  Membership.mem (γ := Set (Submodule R M))
    {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} m
e : LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S
⊢ IsSemisimpleModule.{u_2, u} R ↥m

Tactic:
have := IsSemisimpleModule.congr e
-- 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 S
m : Submodule R M
h :
  Membership.mem (γ := Set (Submodule R M))
    {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} m
e : LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S
this : IsSemisimpleModule.{u_2, u} R ↥m
⊢ IsSemisimpleModule.{u_2, u} R ↥m

Tactic:
infer_instance
-- 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
c : (↑(isotypicComponents R M) : Type u)
obtain :
  ∀ (S : Submodule R M) (left : IsSimpleModule.{u_2, u} R ↥S),
    IsSemisimpleModule.{u_2, u} R
      ↥(↑(Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x) (isotypicComponent R M ↥S) ⋯) :
          Submodule R M)
⊢ IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)

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

Premises used: 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
S : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥S
⊢ IsSemisimpleModule.{u_2, u} R
    ↥(↑(Subtype.mk (p := fun (x : Submodule R M) ↦ Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x)
            (isotypicComponent R M ↥S) ⋯) :
        Submodule R M)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup S
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R S
e : N ≃ₗ[R] S
⊢ Eq (α := Submodule R M) (isotypicComponent R M N) (isotypicComponent R M S)

Tactic:
congr_arg sSup <| Set.ext fun _ ↦ Nonempty.congr (·.trans e) (·.trans e.symm)

Premises used: Set.ext, LinearEquiv.symm, Nonempty.congr, isotypicComponent, congr_arg, LinearEquiv.trans, SupSet.sSup
-- 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 = ⊤
⊢ Nontrivial.{u} ↥N

Tactic:
have := IsSimpleModule.nontrivial R N