-- Mathlib/LinearAlgebra/Semisimple.lean
lemma isSemisimple_restrict_iff (p) (hp : p ∈ invtSubmodule f) :
    IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
let e : Submodule R[X] (AEval' (f.restrict hp)) ≃o Iic (AEval.mapSubmodule R M f ⟨p, hp⟩) :=
  (Submodule.orderIsoMapComap <| AEval.restrict_equiv_mapSubmodule f p hp).trans
    (Submodule.mapIic _)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ a ∈ ((Algebra.lsmul R R M) f).invtSubmodule,
      a ≤ p → ∃ a_2 ≤ p, a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule ∧ a ⊓ a_2 = ⊥ ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
simp_rw [IsSemisimple, IsSemisimpleModule, e.complementedLattice_iff, disjoint_iff,
  ← (OrderIso.Iic _ _).complementedLattice_iff, Iic.complementedLattice_iff, Subtype.forall,
  Subtype.exists, Subtype.mk_le_mk, Sublattice.mk_inf_mk, Sublattice.mk_sup_mk, Subtype.mk.injEq,
  exists_and_left, exists_and_right, invtSubmodule.mk_eq_bot_iff, exists_prop, and_assoc]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ a ∈ ((Algebra.lsmul R R M) f).invtSubmodule,
      a ≤ p → ∃ a_2 ≤ p, a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule ∧ a ⊓ a_2 = ⊥ ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p