awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
inst : Ring R
inst_1 : Ring S_1
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 : IsSimpleModule R M
S : Submodule R M
inl : ∃ (a : M), Eq (α := Submodule R M) ⊥ (R ∙ a)
⊢ ∃ (a : M), S = R ∙ a
have inr : ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)
Tactic: obtain rfl | rfl := eq_bot_or_eq_top S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
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 : IsSimpleModule R M
⊢ ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)
have this : Nontrivial M
Tactic: have := IsSimpleModule.nontrivial R M
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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 : IsSimpleModule R M
this : Nontrivial M
⊢ ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)
have inr : ∀ (m : M) (hm : m ≠ 0), ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)
Tactic: have ⟨m, hm⟩ := exists_ne (0 : M)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(toSpanSingleton R M m) : (a : R) → M)
have rw : Eq (α := Submodule R M) (range (toSpanSingleton R M m)) ⊤
Tactic: rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
rw : Eq (α := Submodule R M) (range (toSpanSingleton R M m)) ⊤
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(toSpanSingleton R M m) : (a : R) → M)
have rw₁ : Eq (α := Submodule R M) (R ∙ m) ⊤
Tactic: rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
rw : Eq (α := Submodule R M) (range (toSpanSingleton R M m)) ⊤
rw₁ : Eq (α := Submodule R M) (R ∙ m) ⊤
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(toSpanSingleton R M m) : (a : R) → M)
have rw₂ : Eq.{u_4 + 1} (α := Submodule R M) ⊤ ⊤
Tactic: rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Ideal.IsMaximal (ker (toSpanSingleton R M m))
have rw : IsSimpleModule R (HasQuotient.Quotient R (B := Submodule R R) (ker (toSpanSingleton R M m)))
Tactic: rw [Ideal.isMaximal_def, ← isSimpleModule_iff_isCoatom]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsSimpleModule R M ↔ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
have refine_1 : ∀ (h : IsSimpleModule R M), ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
refine_1 : ∀ (h : IsSimpleModule R M), ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
⊢ IsSimpleModule R M ↔ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
have refine_2 : (∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)) →
  ∀ (I : Ideal R) (coatom : IsCoatom I) (equiv : M ≃ₗ[R] R ⧸ I), IsSimpleModule R M
Tactic: refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsSimpleModule R M
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
have this : Nontrivial M
Tactic: have := IsSimpleModule.nontrivial R M
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsSimpleModule R M
this : Nontrivial M
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
have refine_1 : ∀ (m : M) (hm : m ≠ 0), ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
Tactic: have ⟨m, hm⟩ := exists_ne (0 : M)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
⊢ IsSimpleModule R M
have refine_2 : IsSimpleModule R (R ⧸ I)
Tactic: convert! congr equiv
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
M : Type u_4
inst : AddCommGroup M
R : Type u_6
inst_1 : CommRing R
inst_2 : Module R M
simple : IsSimpleModule R M
⊢ Ideal.IsMaximal (Module.annihilator R M)
have have : ∀ (I : Ideal R) (max : I.IsMaximal) (e : M ≃ₗ[R] R ⧸ I), Ideal.IsMaximal (Module.annihilator R M)
Tactic: have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
M : Type u_4
inst : AddCommGroup M
R : Type u_6
inst_1 : CommRing R
inst_2 : Module R M
simple : IsSimpleModule R M
I : Ideal R
max : I.IsMaximal
e : M ≃ₗ[R] R ⧸ I
⊢ Ideal.IsMaximal (Module.annihilator R M)
have rwa : Ideal.IsMaximal (Module.annihilator R (R ⧸ I))
Tactic: rwa [e.annihilator_eq, I.annihilator_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 :
  Nontrivial M ∧
    ∀ (x : M),
      x ≠ 0 →
        Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
left : Nontrivial M
h :
  ∀ (x : M),
    x ≠ 0 → Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
m : Submodule R M
ne_bot : ¬m = ⊥
x : M
hxm : x ∈ m
hx0 : x ≠ 0
z : M
h_2 : Membership.mem (γ := Submodule R M) ⊤ z
⊢ z ∈ m
have obtain : ∀ (y : R),
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule R M) ⊤ ((LinearMap.toSpanSingleton R M x : (a : R) → M) y : M) →
    Membership.mem (α := M) m ((LinearMap.toSpanSingleton R M x : (a : R) → M) y : M)
Tactic: obtain ⟨y, rfl⟩ := h x hx0 z
Cleared hypotheses: z, h_2
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
h : Nontrivial R
⊢ (∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)) ↔
    ∀ (x : R), x ≠ 0 → IsUnit x
have refine : ∀ (h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R))
  (x : R) (hx : x ≠ 0), IsUnit x
Tactic: refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
h_1 : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)
x : R
hx : x ≠ 0
⊢ IsUnit x
have obtain : ∀ (y : R) (hyx : y * x = 1), IsUnit x
Tactic: obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
Goal:
R : Type u_2
inst : Ring R
h_1 : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
⊢ IsUnit x
have hy : y ≠ 0
Tactic: have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
h_1 : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
⊢ IsUnit x
have obtain : ∀ (z : R) (hzy : z * y = 1), IsUnit x
Tactic: obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m}) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule R M) (sSup {a : Submodule R M | IsAtom a}) ⊤
have simp_rw : Eq.{u_4 + 1} (α := Submodule R M) (sSup {a : Submodule R M | IsAtom a})
  (sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m})
Tactic: simp_rw [← h, isSimpleModule_iff_isAtom]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
⊢ N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule.{u_2, u_4} R ↥m
have rw : Eq.{u_4 + 1} (α := Submodule R ↥N) ⊥ ⊤ ∨ ∃ m ≤ N, IsSimpleModule.{u_2, u_4} R ↥m
Tactic: rw [← N.subsingleton_iff_eq_bot, ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
⊢ Eq.{u_4 + 1} (α := Submodule R ↥N) ⊥ ⊤ ∨ ∃ m ≤ N, IsSimpleModule.{u_2, u_4} R ↥m
have refine : (∃ (a : Submodule R ↥N), IsAtom a ∧ a ≤ ⊤) →
  ∀ (m : Submodule R ↥N) (h : IsAtom m), m ≤ ⊤ → IsSimpleModule.{u_2, u_4} R ↥(Submodule.map N.subtype m)
Tactic: refine (eq_bot_or_exists_atom_le _).imp .symm fun ⟨m, h, _⟩ ↦ ⟨_, N.map_subtype_le m, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
h_1 : ∃ (a : Submodule R ↥N), IsAtom a ∧ a ≤ ⊤
m : Submodule R ↥N
h : IsAtom m
right : m ≤ ⊤
⊢ IsSimpleModule.{u_2, u_4} R ↥(Submodule.map N.subtype m)
have h₁ : IsSimpleModule.{u_2, u_4} R ↥m
Tactic: rw [← isSimpleModule_iff_isAtom] at h
Cleared hypotheses: h, right
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ (g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f = g
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
have have : ∀ (m : Submodule R M) (compl : IsCompl f.ker m), ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
Tactic: have ⟨m, compl⟩ := exists_isCompl (LinearMap.ker f)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
have 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)
Tactic: refine ⟨Submodule.subtype _ ∘ₗ e.symm.toLinearMap ∘ₗ g, LinearMap.ext fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨z, eq⟩ := e.surjective (g x)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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 ∘ₗ m.subtype ∘ₗ (↑e.symm : N →ₗ[R] ↥m) ∘ₗ g : (a : P) → N) x : N) ((g : (a : P) → N) x : N)
have simp : 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 only [LinearMap.comp_apply, ← eq, LinearEquiv.coe_coe, e.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
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)), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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}) ⊤
⊢ ∃ (s : Set (Submodule R M)), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
have 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
Tactic: simp_rw [isSimpleModule_iff_isAtom] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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 (Module.annihilator R M)
have 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)
Tactic: rw [← Submodule.annihilator_top, ← sSup_simples_eq_top, sSup_eq_iSup', Submodule.annihilator_iSup]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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')
⊢ IsSemisimpleModule R M' ↔ IsSemisimpleModule S N'
have simp_rw : ComplementedLattice.{u_6} (Submodule R M') ↔ ComplementedLattice.{u_7} (Submodule S N')
Tactic: simp_rw [isSemisimpleModule_iff,
    (Submodule.orderIsoMapComapOfBijective l hl).complementedLattice_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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) ⊤
⊢ IsSemisimpleModule R M
have simp_rw : ∀ (hp : ∀ i ∈ s, ComplementedLattice.{u_4} (Submodule R ↥(p i))), ComplementedLattice.{u_4} (Submodule R M)
Tactic: simp_rw [isSemisimpleModule_iff] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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)
have refine : ∀ (i : ι) (hi : i ∈ s), ComplementedLattice.{u_4} (↑(Set.Iic (p i)) : Type u_4)
Tactic: refine complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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)
have refine : ∀ x1 ∈ s, p x1 ≤ LinearMap.range (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ 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 ..)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ p x1 ≤ LinearMap.range (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
have simp_rw : p x1 ≤ ⨆ i ∈ s, p i
Tactic: simp_rw [range_subtype, le_biSup p ‹_›]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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)) (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)
have 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)
Tactic: have ⟨s, ind, sSup, simple⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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)
have refine : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)
Tactic: refine ⟨s, ?_, ind, SetCoe.forall.mpr simple⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
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
⊢ M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)
have ind₁ : iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
Tactic: rw [sSupIndep_iff] at ind
Cleared hypotheses: ind, sSup, simple
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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 :
  iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (LinearMap.range (R := R) (M := Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)) (τ₁₂ := RingHom.id R)
      ((DFinsupp.lsum ℕ (M := fun (i : { x : Submodule R M // x ∈ s }) ↦ ↥(↑i : Submodule R M)) :
          (a : (i : { x : Submodule R M // x ∈ s }) → ↥(↑i : Submodule R M) →ₗ[R] M) →
            (Π₀ (i : { x : Submodule R M // x ∈ s }), ↥(↑i : Submodule R M)) →ₗ[R] M)
        fun (i : { x : Submodule R M // x ∈ s }) ↦ (↑i : Submodule R M).subtype))
    ⊤
have rw : Eq.{u_4 + 1} (α := Submodule R M)
  (iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))) ⊤
Tactic: rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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 :
  iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
rw :
  Eq.{u_4 + 1} (α := Submodule R M)
    (iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (LinearMap.range (R := R) (M := Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)) (τ₁₂ := RingHom.id R)
      ((DFinsupp.lsum ℕ (M := fun (i : { x : Submodule R M // x ∈ s }) ↦ ↥(↑i : Submodule R M)) :
          (a : (i : { x : Submodule R M // x ∈ s }) → ↥(↑i : Submodule R M) →ₗ[R] M) →
            (Π₀ (i : { x : Submodule R M // x ∈ s }), ↥(↑i : Submodule R M)) →ₗ[R] M)
        fun (i : { x : Submodule R M // x ∈ s }) ↦ (↑i : Submodule R M).subtype))
    ⊤
have rw₁ : iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s)) = SupSet.sSup s
Tactic: rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']