-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem isSemisimpleModule_iff_exists_linearEquiv_dfinsupp : IsSemisimpleModule R M ↔
    ∃ (s : Set (Submodule R M)) (_ : M ≃ₗ[R] Π₀ m : s, m.1), ∀ m : s, IsSimpleModule R m.1

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Tactic:
have ⟨s, ind, sSup, simple⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : sSupIndep s
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : sSupIndep s
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Tactic:
rw [sSupIndep_iff] at ind

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m

Tactic:
exact .symm <| .trans (.ofInjective _ ind.dfinsupp_lsum_injective) <| .trans (.ofEq _ ⊤ <|
  by rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']) Submodule.topEquiv

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m

Tactic:
classical
exact .symm <| .trans (.ofInjective _ ind.dfinsupp_lsum_injective) <| .trans (.ofEq _ ⊤ <|
  by rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']) Submodule.topEquiv

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSemisimpleModule R M ↔ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Tactic:
refine ⟨fun _ ↦ ?_, fun ⟨s, e, h⟩ ↦ .congr e⟩

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

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

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ LinearMap.range ((DFinsupp.lsum ℕ) fun i => (↑i).subtype) = ⊤

Tactic:
rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']

Result:
no goals