-- Mathlib/RingTheory/SimpleModule/Basic.lean
lemma isSemisimpleModule_biSup_of_isSemisimpleModule_submodule {s : Set ι} {p : ι → Submodule R M}
    (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) :
    IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Proof state:
case a
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
⊢ Submodule.map q.subtype (⨆ i ∈ s, p' i) = Submodule.map q.subtype ⊤

Tactic:
simp_rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_iSup]

Result:
case a
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
⊢ ⨆ i ∈ s, Submodule.map q.subtype (p' i) = q

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
let p' : ι → Submodule R q := fun i ↦ (p i).comap q.subtype

Result:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
hp₂ : ⨆ i ∈ s, p' i = ⊤
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
exact isSemisimpleModule_of_isSemisimpleModule_submodule hp₁ hp₂

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
⊢ ⨆ i ∈ s, p' i = ⊤

Tactic:
apply Submodule.map_injective_of_injective q.injective_subtype

Result:
case a
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
⊢ Submodule.map q.subtype (⨆ i ∈ s, p' i) = Submodule.map q.subtype ⊤

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
i : ι
hi : i ∈ s
e : ↥(p' i) ≃ₗ[R] ↥(p i) := Submodule.comap_equiv_self_of_inj_of_le ⋯ ⋯
⊢ IsSemisimpleModule R ↥(p' i)

Tactic:
exact (Submodule.orderIsoMapComap e).complementedLattice_iff.mpr <| hp i hi

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
i : ι
hi : i ∈ s
⊢ IsSemisimpleModule R ↥(p' i)

Tactic:
let e : p' i ≃ₗ[R] p i := (p i).comap_equiv_self_of_inj_of_le q.injective_subtype (hp₀ i hi)

Result:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
i : ι
hi : i ∈ s
e : ↥(p' i) ≃ₗ[R] ↥(p i) := Submodule.comap_equiv_self_of_inj_of_le ⋯ ⋯
⊢ IsSemisimpleModule R ↥(p' i)

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
have hp₁ : ∀ i ∈ s, IsSemisimpleModule R (p' i) := fun i hi ↦ by
  let e : p' i ≃ₗ[R] p i := (p i).comap_equiv_self_of_inj_of_le q.injective_subtype (hp₀ i hi)
  exact (Submodule.orderIsoMapComap e).complementedLattice_iff.mpr <| hp i hi

Result:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Proof state:
case a
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
⊢ ⨆ i ∈ s, Submodule.map q.subtype (p' i) = q

Tactic:
exact biSup_congr fun i hi ↦ Submodule.map_comap_eq_of_le (hp₀ i hi)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
i : ι
hi : i ∈ s
⊢ p i ≤ LinearMap.range q.subtype

Tactic:
simpa only [Submodule.range_subtype] using le_biSup _ hi

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
let q := ⨆ i ∈ s, p i

Result:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)