awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
N : Submodule R M
⊢ ∃ (P : Submodule R M), Nonempty.{u_4 + 1} (↥P ≃ₗ[R] M ⧸ N)

Tactic:
have ⟨P, compl⟩ := exists_isCompl N; ⟨P, ⟨(N.quotientEquivOfIsCompl P compl).symm⟩⟩

Premises used: LinearEquiv.symm, _private.0.IsSemisimpleModule.exists_submodule_linearEquiv_quotient.match_1, Membership.mem, Exists, Subtype, ComplementedLattice.exists_isCompl, Submodule.quotientEquivOfIsCompl, Nonempty.intro, HasQuotient.Quotient, LinearEquiv, Exists.intro, Nonempty, RingHom.id
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
N : Submodule R M
⊢ ∃ (P : Submodule R M), Nonempty.{u_4 + 1} (↥N ≃ₗ[R] M ⧸ P)

Tactic:
have ⟨P, compl⟩ := exists_isCompl N; ⟨P, ⟨(P.quotientEquivOfIsCompl N compl.symm).symm⟩⟩

Premises used: LinearEquiv.symm, _private.0.IsSemisimpleModule.exists_submodule_linearEquiv_quotient.match_1, Membership.mem, Exists, Subtype, ComplementedLattice.exists_isCompl, Submodule.quotientEquivOfIsCompl, Nonempty.intro, HasQuotient.Quotient, LinearEquiv, Exists.intro, Nonempty, RingHom.id, IsCompl.symm
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
P : Type u_6
inst_6 : AddCommGroup P
inst_7 : Module R P
f : N →ₗ[R] M
hf : Function.Injective.{u_5 + 1, u_4 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
g : N →ₗ[R] P
m : Submodule R M
compl : IsCompl f.range m
h :
  ∀ (x : N),
    Eq.{u_6 + 1} (α := P) (((g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f : (a : N) → P) x : P)
      ((g : (a : N) → P) x : P)
⊢ (g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f = g

Tactic:
ext
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
P : Type u_6
inst_6 : AddCommGroup P
inst_7 : Module R P
f : N →ₗ[R] M
hf : Function.Injective.{u_5 + 1, u_4 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
g : N →ₗ[R] P
m : Submodule R M
compl : IsCompl f.range m
x : N
⊢ Eq.{u_6 + 1} (α := P) (((g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f : (a : N) → P) x : P)
    ((g : (a : N) → P) x : P)

Tactic:
simp
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
P : Type u_6
inst_6 : AddCommGroup P
inst_7 : Module R P
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : P →ₗ[R] N
have : ∀ (m : Submodule R M) (compl : IsCompl f.ker m), ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
⊢ ∃ (h : P →ₗ[R] M), f ∘ₗ h = g

Tactic:
have ⟨m, compl⟩ := exists_isCompl (LinearMap.ker f)
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
P : Type u_6
inst_6 : AddCommGroup P
inst_7 : Module R P
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : LinearEquiv.{u_2, u_2, u_4, u_5} (RingHom.id R) (↥m) N :=
  (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
⊢ ∃ (h : P →ₗ[R] M), f ∘ₗ h = g

Tactic:
⟨Submodule.subtype _ ∘ₗ e.symm.toLinearMap ∘ₗ g, LinearMap.ext fun x ↦ ?_⟩

Premises used: LinearEquiv.symm, LinearMap.ext, LinearMap.comp, LinearEquiv.toLinearMap, Exists.intro, Submodule.subtype
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
P : Type u_6
inst_6 : AddCommGroup P
inst_7 : Module R P
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : LinearEquiv.{u_2, u_2, u_4, u_5} (RingHom.id R) (↥m) N :=
  (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
refine :
  ∀ (x : P),
    Eq.{u_5 + 1} (α := N) ((f ∘ₗ m.subtype ∘ₗ (↑e.symm : N →ₗ[R] ↥m) ∘ₗ g : (a : P) → N) x : N)
      ((g : (a : P) → N) x : N)
⊢ ∃ (h : P →ₗ[R] M), f ∘ₗ h = g

Tactic:
refine ⟨Submodule.subtype _ ∘ₗ e.symm.toLinearMap ∘ₗ g, LinearMap.ext fun x ↦ ?_⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
P : Type u_6
inst_6 : AddCommGroup P
inst_7 : Module R P
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : LinearEquiv.{u_2, u_2, u_4, u_5} (RingHom.id R) (↥m) N :=
  (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
x : P
obtain :
  ∀ (z : ↥m) (eq : Eq.{u_5 + 1} (α := N) ((e : (a : ↥m) → N) z : N) ((g : (a : P) → N) x : N)),
    Eq.{u_5 + 1} (α := N) ((f ∘ₗ m.subtype ∘ₗ (↑e.symm : N →ₗ[R] ↥m) ∘ₗ g : (a : P) → N) x : N)
      ((g : (a : P) → N) x : N)
⊢ Eq.{u_5 + 1} (α := N) ((f ∘ₗ m.subtype ∘ₗ (↑e.symm : N →ₗ[R] ↥m) ∘ₗ g : (a : P) → N) x : N) ((g : (a : P) → N) x : N)

Tactic:
obtain ⟨z, eq⟩ := e.surjective (g x)

Premises used: LinearEquiv.surjective, DFunLike.coe
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
P : Type u_6
inst_6 : AddCommGroup P
inst_7 : Module R P
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : LinearEquiv.{u_2, u_2, u_4, u_5} (RingHom.id R) (↥m) N :=
  (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
x : P
z : ↥m
eq : Eq.{u_5 + 1} (α := N) ((e : (a : ↥m) → N) z : N) ((g : (a : P) → N) x : N)
simp : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) ((m.subtype : (a : ↥m) → M) z : M) : N) ((e : (a : ↥m) → N) z : N)
⊢ Eq.{u_5 + 1} (α := N) ((f ∘ₗ m.subtype ∘ₗ (↑e.symm : N →ₗ[R] ↥m) ∘ₗ g : (a : P) → N) x : N) ((g : (a : P) → N) x : N)

Tactic:
simp only [LinearMap.comp_apply, ← eq, LinearEquiv.coe_coe, e.symm_apply_apply]

Premises used: LinearMap.comp_apply, LinearEquiv.symm_apply_apply, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
P : Type u_6
inst_6 : AddCommGroup P
inst_7 : Module R P
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : LinearEquiv.{u_2, u_2, u_4, u_5} (RingHom.id R) (↥m) N :=
  (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
x : P
z : ↥m
eq : Eq.{u_5 + 1} (α := N) ((e : (a : ↥m) → N) z : N) ((g : (a : P) → N) x : N)
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) ((m.subtype : (a : ↥m) → M) z : M) : N) ((e : (a : ↥m) → N) z : N)

Tactic:
simp [e]
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
N : Submodule R M
⊢ sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m ∧ m ≤ N} = N

Tactic:
simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_le_eq _

Premises used: isSimpleModule_iff_isAtom, sSup_atoms_le_eq
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
inst_4 : Nontrivial M
⊢ ∃ (m : Submodule R M), IsSimpleModule.{u_2, u_4} R ↥m

Tactic:
simpa only [isSimpleModule_iff_isAtom] using IsAtomic.exists_atom _

Premises used: isSimpleModule_iff_isAtom, IsAtomic.exists_atom
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
⊢ Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m}) ⊤

Tactic:
simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_eq_top

Premises used: isSimpleModule_iff_isAtom, sSup_atoms_eq_top
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
⊢ Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m}) ⊤

Tactic:
have := sSup_simples_eq_top R M
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
this : Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m}) ⊤
simp_rw :
  ∀ (this : Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsAtom m}) ⊤),
    ∃ (s : Set (Submodule R M)), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsAtom m
⊢ ∃ (s : Set (Submodule R M)), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m

Tactic:
simp_rw [isSimpleModule_iff_isAtom] at this ⊢

Premises used: isSimpleModule_iff_isAtom
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
this : Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsAtom m}) ⊤
⊢ ∃ (s : Set (Submodule R M)), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsAtom m

Tactic:
exists_sSupIndep_of_sSup_atoms_eq_top this

Premises used: exists_sSupIndep_of_sSup_atoms_eq_top
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
this : Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsAtom m}) ⊤
⊢ ∃ (s : Set (Submodule R M)), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsAtom m

Tactic:
exact exists_sSupIndep_of_sSup_atoms_eq_top this

Premises used: exists_sSupIndep_of_sSup_atoms_eq_top
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
M : Type u_4
inst : AddCommGroup M
R : Type u_6
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
rw :
  Ideal.IsRadical.{u_6} (R := R)
    (⨅ (i : (↑{m : Submodule R M | IsSimpleModule.{u_6, u_4} R ↥m} : Type u_4)), (↑i : Submodule R M).annihilator)
⊢ Ideal.IsRadical (Module.annihilator R M)

Tactic:
rw [← Submodule.annihilator_top, ← sSup_simples_eq_top, sSup_eq_iSup', Submodule.annihilator_iSup]

Premises used: Submodule.annihilator_iSup, IsSemisimpleModule.sSup_simples_eq_top, Submodule.annihilator_top, sSup_eq_iSup'
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
M : Type u_4
inst : AddCommGroup M
R : Type u_6
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
⊢ Ideal.IsRadical.{u_6} (R := R)
    (⨅ (i : (↑{m : Submodule R M | IsSimpleModule.{u_6, u_4} R ↥m} : Type u_4)), (↑i : Submodule R M).annihilator)

Tactic:
Ideal.isRadical_iInf _ fun i ↦ (i.2.annihilator_isMaximal).isPrime.isRadical

Premises used: Ideal.isRadical_iInf, Ideal.IsMaximal.isPrime, Ideal.IsPrime.isRadical, IsSimpleModule.annihilator_isMaximal
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
M : Type u_4
inst : AddCommGroup M
R : Type u_6
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
⊢ Ideal.IsRadical.{u_6} (R := R)
    (⨅ (i : (↑{m : Submodule R M | IsSimpleModule.{u_6, u_4} R ↥m} : Type u_4)), (↑i : Submodule R M).annihilator)

Tactic:
exact Ideal.isRadical_iInf _ fun i ↦ (i.2.annihilator_isMaximal).isPrime.isRadical

Premises used: Ideal.isRadical_iInf
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
f : N →ₗ[R] M
hf : Function.Injective.{u_5 + 1, u_4 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
⊢ IsSemisimpleModule R N

Tactic:
congr (Submodule.topEquiv.symm.trans <| Submodule.equivMapOfInjective f hf _)

Premises used: LinearEquiv.symm, Submodule.topEquiv, Submodule.equivMapOfInjective, IsSemisimpleModule.congr, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSemisimpleModule R M
⊢ IsSemisimpleModule.{u_2, u_4} R (M ⧸ m)

Tactic:
have ⟨_, ⟨e⟩⟩ := exists_submodule_linearEquiv_quotient m
  .congr e.symm

Premises used: IsSemisimpleModule.exists_submodule_linearEquiv_quotient, LinearEquiv.symm, _private.0.IsSemisimpleModule.quotient.match_1, HasQuotient.Quotient, IsSemisimpleModule, IsSemisimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
f : M →ₗ[R] N
⊢ IsSemisimpleModule.{u_2, u_5} R ↥f.range

Tactic:
congr (quotKerEquivRange _).symm

Premises used: LinearEquiv.symm, LinearMap.quotKerEquivRange, IsSemisimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsSemisimpleModule R N

Tactic:
congr (f.quotKerEquivOfSurjective hf).symm

Premises used: LinearEquiv.symm, LinearMap.quotKerEquivOfSurjective, IsSemisimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M' : Type u_6
inst_2 : AddCommGroup M'
inst_3 : Module R M'
N' : Type u_7
inst_4 : AddCommGroup N'
inst_5 : Module S N'
σ : R →+* S
l : M' →ₛₗ[σ] N'
inst_6 : RingHomSurjective σ
hl : Function.Bijective.{u_6 + 1, u_7 + 1} (α := M') (β := N') (⇑l : (a : M') → N')
simp_rw : ComplementedLattice.{u_6} (Submodule R M') ↔ ComplementedLattice.{u_7} (Submodule S N')
⊢ IsSemisimpleModule R M' ↔ IsSemisimpleModule S N'

Tactic:
simp_rw [isSemisimpleModule_iff,
    (Submodule.orderIsoMapComapOfBijective l hl).complementedLattice_iff]

Premises used: OrderIso.complementedLattice_iff, isSemisimpleModule_iff, Submodule.orderIsoMapComapOfBijective
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ IsSemisimpleModule R M ↔ IsSemisimpleModule R N

Tactic:
⟨(·.congr e.symm), (·.congr e)⟩

Premises used: LinearEquiv.symm, Iff.intro, IsSemisimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m}) ⊤ ↔
    IsSemisimpleModule R M

Tactic:
⟨.of_sSup_simples_eq_top, fun _ ↦ IsSemisimpleModule.sSup_simples_eq_top _ _⟩

Premises used: IsSemisimpleModule.of_sSup_simples_eq_top, IsSemisimpleModule.sSup_simples_eq_top, Iff.intro
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule.{u_2, u_4} R ↥(p i)
hp' : Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, p i) ⊤
simp_rw : ∀ (hp : ∀ i ∈ s, ComplementedLattice.{u_4} (Submodule R ↥(p i))), ComplementedLattice.{u_4} (Submodule R M)
⊢ IsSemisimpleModule R M

Tactic:
simp_rw [isSemisimpleModule_iff] at hp ⊢

Premises used: isSemisimpleModule_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
p : ι → Submodule R M
hp' : Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, p i) ⊤
hp : ∀ i ∈ s, ComplementedLattice.{u_4} (Submodule R ↥(p i))
⊢ ComplementedLattice.{u_4} (Submodule R M)

Tactic:
complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'

Premises used: complementedLattice_of_complementedLattice_Iic
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
p : ι → Submodule R M
hp' : Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, p i) ⊤
hp : ∀ i ∈ s, ComplementedLattice.{u_4} (Submodule R ↥(p i))
refine : ∀ (i : ι) (hi : i ∈ s), ComplementedLattice.{u_4} (↑(Set.Iic (p i)) : Type u_4)
⊢ ComplementedLattice.{u_4} (Submodule R M)

Tactic:
refine complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'

Premises used: complementedLattice_of_complementedLattice_Iic
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
p : ι → Submodule R M
hp' : Eq.{u_4 + 1} (α := Submodule R M) (⨆ i ∈ s, p i) ⊤
hp : ∀ i ∈ s, ComplementedLattice.{u_4} (Submodule R ↥(p i))
i : ι
hi : i ∈ s
⊢ ComplementedLattice.{u_4} (↑(Set.Iic (p i)) : Type u_4)

Tactic:
simpa only [← (p i).mapIic.complementedLattice_iff] using hp i hi

Premises used: OrderIso.complementedLattice_iff, Submodule.mapIic
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule.{u_2, u_4} R ↥(p i)
⊢ IsSemisimpleModule.{u_2, u_4} R ↥(⨆ i ∈ s, p i)

Tactic:
isSemisimpleModule_of_isSemisimpleModule_submodule
    ((comap_equiv_self_of_inj_of_le (injective_subtype _) ?_).isSemisimpleModule_iff.mpr <| hp · ·)
    (biSup_comap_subtype_eq_top ..)

Premises used: Iff.mpr, Submodule.biSup_comap_subtype_eq_top, isSemisimpleModule_of_isSemisimpleModule_submodule, LinearEquiv.isSemisimpleModule_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule.{u_2, u_4} R ↥(p i)
refine : ∀ x1 ∈ s, p x1 ≤ LinearMap.range (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
⊢ IsSemisimpleModule.{u_2, u_4} R ↥(⨆ i ∈ s, p i)

Tactic:
refine isSemisimpleModule_of_isSemisimpleModule_submodule
    ((comap_equiv_self_of_inj_of_le (injective_subtype _) ?_).isSemisimpleModule_iff.mpr <| hp · ·)
    (biSup_comap_subtype_eq_top ..)

Premises used: Iff.mpr, isSemisimpleModule_of_isSemisimpleModule_submodule, LinearEquiv.isSemisimpleModule_iff
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule.{u_2, u_4} R ↥(p i)
x1 : ι
x2 : x1 ∈ s
simp_rw : p x1 ≤ ⨆ i ∈ s, p i
⊢ p x1 ≤ LinearMap.range (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))

Tactic:
simp_rw [range_subtype, le_biSup p ‹_›]

Premises used: le_biSup, Submodule.range_subtype
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ι → Submodule R M
hp : ∀ (i : ι), IsSemisimpleModule.{u_2, u_4} R ↥(p i)
hp' : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), p i) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ i), p i) ⊤

Tactic:
simpa
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M_1 : Type u_4
inst_2 : AddCommGroup M_1
inst_3 : Module R M_1
m : Submodule R M_1
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_7
M : ι → Type u_6
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_2, u_6} R (M i)
inst_8 : ∀ (i : ι), IsSemisimpleModule.{u_2, u_6} R (M i)
⊢ IsSemisimpleModule R (Π₀ (i : ι), M i)

Tactic:
isSemisimpleModule_of_isSemisimpleModule_submodule'
    (fun _ ↦ .range _) DFinsupp.iSup_range_lsingle

Premises used: DFinsupp.iSup_range_lsingle, isSemisimpleModule_of_isSemisimpleModule_submodule', IsSemisimpleModule.range
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M_1 : Type u_4
inst_2 : AddCommGroup M_1
inst_3 : Module R M_1
m : Submodule R M_1
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_7
M : ι → Type u_6
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_2, u_6} R (M i)
inst_8 : ∀ (i : ι), IsSemisimpleModule.{u_2, u_6} R (M i)
⊢ IsSemisimpleModule R (Π₀ (i : ι), M i)

Tactic:
exact isSemisimpleModule_of_isSemisimpleModule_submodule'
    (fun _ ↦ .range _) DFinsupp.iSup_range_lsingle

Premises used: isSemisimpleModule_of_isSemisimpleModule_submodule', IsSemisimpleModule.range
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M_1 : Type u_4
inst_2 : AddCommGroup M_1
inst_3 : Module R M_1
m : Submodule R M_1
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_7
M : ι → Type u_6
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u_2, u_6} R (M i)
inst_8 : ∀ (i : ι), IsSemisimpleModule.{u_2, u_6} R (M i)
⊢ IsSemisimpleModule R (Π₀ (i : ι), M i)

Tactic:
classical
  exact isSemisimpleModule_of_isSemisimpleModule_submodule'
    (fun _ ↦ .range _) DFinsupp.iSup_range_lsingle

Premises used: isSemisimpleModule_of_isSemisimpleModule_submodule', IsSemisimpleModule.range
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
have :
  ∀ (s : Set (Submodule R M)) (ind : sSupIndep s) (sSup : sSup s = ⊤)
    (simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m),
    ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
      sSupIndep s ∧ ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
⊢ ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    sSupIndep s ∧ ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)

Tactic:
have ⟨s, ind, sSup, simple⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : sSupIndep s
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
⊢ ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    sSupIndep s ∧ ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)

Tactic:
⟨s, ?_, ind, SetCoe.forall.mpr simple⟩

Premises used: Iff.mpr, And.intro, Exists.intro, SetCoe.forall
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : sSupIndep s
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
refine : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)
⊢ ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    sSupIndep s ∧ ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)

Tactic:
refine ⟨s, ?_, ind, SetCoe.forall.mpr simple⟩