awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_4 : Module.Finite (End R M) M
s : Finset M
hs : Eq (α := Submodule (End R M) M) (span (End R M) (↑s : Set M)) ⊤
f : End (End R M) M
⊢ ∃ (a : R), (toModuleEnd (End R M) M : (a : R) → End (End R M) M) a = f
have have : ∀ (r : R) (hr : ∀ m ∈ s, (f : (a : M) → M) m = r • m),
  ∃ (a : R), (toModuleEnd (End R M) M : (a : R) → End (End R M) M) a = f
Tactic: have ⟨r, hr⟩ := jacobson_density f s
-- 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
inst_4 : Module.Finite (End R M) M
s : Finset M
hs : Eq (α := Submodule (End R M) M) (span (End R M) (↑s : Set M)) ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, (f : (a : M) → M) m = r • m
⊢ ∃ (a : R), (toModuleEnd (End R M) M : (a : R) → End (End R M) M) a = f
have refine : ∀ (m : M),
  Eq (α := M) ((((toModuleEnd (End R M) M : (a : R) → End (End R M) M) r : End (End R M) M) : (a : M) → M) m : M)
    ((f : (a : M) → M) m : M)
Tactic: refine ⟨r, LinearMap.ext fun 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
inst_4 : Module.Finite (End R M) M
s : Finset M
hs : Eq (α := Submodule (End R M) M) (span (End R M) (↑s : Set M)) ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, (f : (a : M) → M) m = r • m
m : M
g : End R M
x : M
hx : Membership.mem (γ := Submodule (End R M) M) (span (End R M) (↑s : Set M)) x
h :
  Eq (α := M) ((((toModuleEnd (End R M) M : (a : R) → End (End R M) M) r : End (End R M) M) : (a : M) → M) x : M)
    ((f : (a : M) → M) x : M)
⊢ Eq (α := M) ((((toModuleEnd (End R M) M : (a : R) → End (End R M) M) r : End (End R M) M) : (a : M) → M) (g • x) : M)
    ((f : (a : M) → M) (g • x) : M)
have smul : HSMul.hSMul (β := M) g
    ((((toModuleEnd (End R M) M : (a : R) → End (End R M) M) r : End (End R M) M) : (a : M) → M) x : M) =
  HSMul.hSMul (β := M) g ((f : (a : M) → M) x : M)
Tactic: simp_rw [map_smul, h]
-- 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
inst_4 : Module.Finite (End R M) M
s : Finset M
hs : Eq (α := Submodule (End R M) M) (span (End R M) (↑s : Set M)) ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, (f : (a : M) → M) m = r • m
m : M
⊢ Eq (α := M) ((((toModuleEnd (End R M) M : (a : R) → End (End R M) M) r : End (End R M) M) : (a : M) → M) m : M)
    ((f : (a : M) → M) m : M)
have x : Membership.mem (γ := Submodule (End R M) M) (span (End R M) (↑s : Set M)) m
Tactic: induction hs.ge (trivial : m ∈ ⊤) using Submodule.span_induction with
  | mem m hm => exact (hr m hm).symm
  | zero => simp
  | add _ _ _ _ h₁ h₂ => simpa using congr($h₁ + $h₂)
  | smul g _ _ h => simp_rw [map_smul, h]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.InjectiveProjective (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsSemisimpleRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
X Y : Type u_2
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
h : Y →ₗ[R] M
comp : h ∘ₗ f = g
x_4 : X
⊢ Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((g : (a : X) → M) x_4 : M)
have rw : Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((h ∘ₗ f : (a : X) → M) x_4 : M)
Tactic: rw [← comp, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.InjectiveProjective (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsSemisimpleRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
X Y : Type u_2
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
h : Y →ₗ[R] M
comp : h ∘ₗ f = g
x_4 : X
rw : Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((h ∘ₗ f : (a : X) → M) x_4 : M)
⊢ Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((g : (a : X) → M) x_4 : M)
have rw₁ : Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M)
Tactic: rw [← comp, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
⊢ Nonempty.{u + 1} (↥S ≃ₗ[R] M)
have hS₁ : S = ⊤
Tactic: rw [isSimpleModule_iff_isAtom, isAtom_iff_eq_top] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
N : Submodule R M
⊢ IsIsotypicOfType.{u, u_2, u_4} R (↥N) S ↔
    ∀ m ≤ N, ∀ [IsSimpleModule.{u_2, u} R ↥m], Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)
have rw : IsIsotypicOfType.{u, u_2, u_4} R (↥N) S ↔
  ∀ (a : Submodule R ↥N)
    [IsSimpleModule.{u_2, u} R
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)],
    Nonempty
      (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R)
        (↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M))
        S)
Tactic: rw [Subtype.forall', ← (Submodule.MapSubtype.orderIso N).forall_congr_right]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
N : Submodule R M
⊢ IsIsotypicOfType.{u, u_2, u_4} R (↥N) S ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      Nonempty
        (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R)
          (↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M))
          S)
have have : ∀ (e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)),
  IsIsotypicOfType.{u, u_2, u_4} R (↥N) S ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      Nonempty
        (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R)
          (↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M))
          S)
Tactic: have e := Submodule.equivMapOfInjective _ N.subtype_injective
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypicOfType.{u, u_2, u_4} R (↥N) S ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      Nonempty
        (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R)
          (↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M))
          S)
have simp_rw : IsIsotypicOfType.{u, u_2, u_4} R (↥N) S ↔
  ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥a],
    Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥(Submodule.map N.subtype a)) S)
Tactic: simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
⊢ IsIsotypic.{u, u_2} R ↥N ↔ ∀ m ≤ N, ∀ [IsSimpleModule.{u_2, u} R ↥m], IsIsotypicOfType.{u, u_2, u} R ↥N ↥m
have rw : IsIsotypic.{u, u_2} R ↥N ↔
  ∀ (a : Submodule R ↥N)
    [IsSimpleModule.{u_2, u} R
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)],
    IsIsotypicOfType.{u, u_2, u} R ↥N
      ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
              a) :
          Submodule R M)
Tactic: rw [Subtype.forall', ← (Submodule.MapSubtype.orderIso N).forall_congr_right]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
⊢ IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
have have : ∀ (e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)),
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
Tactic: have e := Submodule.equivMapOfInjective _ N.subtype_injective
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
have simp_rw : IsIsotypic.{u, u_2} R ↥N ↔
  ∀ (a : Submodule R ↥N)
    [IsSimpleModule.{u_2, u} R
        ↥(↑(({
                    toFun := fun (p' : Submodule R ↥N) ↦
                      Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') sorry,
                    invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                      Submodule.comap N.subtype (↑q : Submodule R M),
                    left_inv := sorry, right_inv := sorry : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)],
    IsIsotypicOfType.{u, u_2, u} R ↥N
      ↥(↑(({
                  toFun := fun (p' : Submodule R ↥N) ↦
                    Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') sorry,
                  invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦ Submodule.comap N.subtype (↑q : Submodule R M),
                  left_inv := sorry, right_inv := sorry : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
              a) :
          Submodule R M)
Tactic: simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff,
    ← (e _).isIsotypicOfType_iff_type, IsIsotypic]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
simp_rw :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(({
                      toFun := fun (p' : Submodule R ↥N) ↦
                        Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') ⋯,
                      invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                        Submodule.comap N.subtype (↑q : Submodule R M),
                      left_inv := ⋯, right_inv := ⋯ : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(({
                    toFun := fun (p' : Submodule R ↥N) ↦
                      Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') ⋯,
                    invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                      Submodule.comap N.subtype (↑q : Submodule R M),
                    left_inv := ⋯, right_inv := ⋯ : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
⊢ IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
have simp_rw₁ : IsIsotypic.{u, u_2} R ↥N ↔
  ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥(Submodule.map N.subtype a)],
    IsIsotypicOfType.{u, u_2, u} R ↥N ↥(Submodule.map N.subtype a)
Tactic: simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff,
    ← (e _).isIsotypicOfType_iff_type, IsIsotypic]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
simp_rw :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(({
                      toFun := fun (p' : Submodule R ↥N) ↦
                        Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') ⋯,
                      invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                        Submodule.comap N.subtype (↑q : Submodule R M),
                      left_inv := ⋯, right_inv := ⋯ : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(({
                    toFun := fun (p' : Submodule R ↥N) ↦
                      Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') ⋯,
                    invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                      Submodule.comap N.subtype (↑q : Submodule R M),
                    left_inv := ⋯, right_inv := ⋯ : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
simp_rw₁ :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥(Submodule.map N.subtype a)],
      IsIsotypicOfType.{u, u_2, u} R ↥N ↥(Submodule.map N.subtype a)
⊢ IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
have simp_rw₂ : IsIsotypic.{u, u_2} R ↥N ↔
  ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥a], IsIsotypicOfType.{u, u_2, u} R ↥N ↥(Submodule.map N.subtype a)
Tactic: simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff,
    ← (e _).isIsotypicOfType_iff_type, IsIsotypic]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
simp_rw :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(({
                      toFun := fun (p' : Submodule R ↥N) ↦
                        Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') ⋯,
                      invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                        Submodule.comap N.subtype (↑q : Submodule R M),
                      left_inv := ⋯, right_inv := ⋯ : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(({
                    toFun := fun (p' : Submodule R ↥N) ↦
                      Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ N) (Submodule.map N.subtype p') ⋯,
                    invFun := fun (q : { p' : Submodule R M // p' ≤ N }) ↦
                      Submodule.comap N.subtype (↑q : Submodule R M),
                    left_inv := ⋯, right_inv := ⋯ : Submodule R ↥N ≃ { p' : Submodule R M // p' ≤ N } } :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
simp_rw₁ :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥(Submodule.map N.subtype a)],
      IsIsotypicOfType.{u, u_2, u} R ↥N ↥(Submodule.map N.subtype a)
simp_rw₂ :
  IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥a],
      IsIsotypicOfType.{u, u_2, u} R ↥N ↥(Submodule.map N.subtype a)
⊢ IsIsotypic.{u, u_2} R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule.{u_2, u} R
          ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                    (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                  a) :
              Submodule R M)],
      IsIsotypicOfType.{u, u_2, u} R ↥N
        ↥(↑(((Submodule.MapSubtype.orderIso N).toEquiv (r := fun (x1 x2 : Submodule R ↥N) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { p' : Submodule R M // p' ≤ N }) ↦ x1 ≤ x2) :
                  (a : Submodule R ↥N) → { p' : Submodule R M // p' ≤ N })
                a) :
            Submodule R M)
have simp_rw₃ : IsIsotypic.{u, u_2} R ↥N ↔ ∀ (a : Submodule R ↥N) [IsSimpleModule.{u_2, u} R ↥a], IsIsotypicOfType.{u, u_2, u} R ↥N ↥a
Tactic: simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff,
    ← (e _).isIsotypicOfType_iff_type, IsIsotypic]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
inst_5 : IsSemisimpleModule R M
h : IsIsotypicOfType R M S
⊢ ∃ (ι : Type u), Nonempty (M ≃ₗ[R] ι →₀ S)
have have : ∀ (s : Set (Submodule R M)) (e : M ≃ₗ[R] Π₀ (m : (↑s : Type u)), ↥(↑m : Submodule R M)),
  sSupIndep s →
    ∀ (hs : ∀ (m : (↑s : Type u)), IsSimpleModule.{u_2, u} R ↥(↑m : Submodule R M)),
      ∃ (ι : Type u), Nonempty (M ≃ₗ[R] ι →₀ S)
Tactic: have ⟨s, e, _, hs⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M