awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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) 0 : M)
    ((f : (a : M) → M) 0 : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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 x y : M
hx : Membership.mem (γ := Submodule (End R M) M) (span (End R M) (↑s : Set M)) x
hy : Membership.mem (γ := Submodule (End R M) M) (span (End R M) (↑s : Set M)) y
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)
h₂ :
  Eq (α := M) ((((toModuleEnd (End R M) M : (a : R) → End (End R M) M) r : End (End R M) M) : (a : M) → M) y : M)
    ((f : (a : M) → M) y : M)
⊢ Eq (α := M) ((((toModuleEnd (End R M) M : (a : R) → End (End R M) M) r : End (End R M) M) : (a : M) → M) (x + y) : M)
    ((f : (a : M) → M) (x + y) : M)

Tactic:
simpa using congr($h₁ + $h₂)
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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)
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)
⊢ 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)

Tactic:
simp_rw [map_smul, h]

Premises used: map_smul
-- Module: Mathlib.RingTheory.SimpleModule.Basic
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
⊢ 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]

Premises used: Eq.ge, Submodule.smul, Submodule.zero, Submodule.add, map_smul
-- Module: Mathlib.RingTheory.SimpleModule.InjectiveProjective
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)
rw₁ 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)
⊢ Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((g : (a : X) → M) x_4 : M)

Tactic:
rw [← comp, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply
-- Module: Mathlib.RingTheory.SimpleModule.InjectiveProjective
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
⊢ Projective R M

Tactic:
.of_lifting_property'' (IsSemisimpleModule.lifting_property · · _)

Premises used: LinearMap.id, IsSemisimpleModule.lifting_property, Module.Projective.of_lifting_property''
-- Module: Mathlib.RingTheory.SimpleModule.IsAlgClosed
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : IsAlgClosed F
inst_2 : Ring R
inst_3 : Algebra F R
inst_4 : IsSimpleRing R
inst_5 : FiniteDimensional F R
⊢ ∃ (n : ℕ) (_ : NeZero n), Nonempty (R ≃ₐ[F] Matrix (Fin n) (Fin n) F)

Tactic:
have := IsArtinianRing.of_finite F R
  have ⟨n, hn, D, _, _, _, ⟨e⟩⟩ := exists_algEquiv_matrix_divisionRing_finite F R
  ⟨n, hn, ⟨e.trans <| .mapMatrix <| .symm <| .ofBijective (Algebra.ofId F D)
    IsAlgClosed.algebraMap_bijective_of_isIntegral⟩⟩

Premises used: _private.0.IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed.match_1, AlgEquiv.symm, AlgEquiv.ofBijective, Matrix, Exists, AlgEquiv.mapMatrix, IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite, Nonempty.intro, IsArtinianRing.of_finite, Algebra.ofId, AlgEquiv.trans, AlgEquiv, IsAlgClosed.algebraMap_bijective_of_isIntegral, Exists.intro, Nonempty, Fin
-- Module: Mathlib.RingTheory.SimpleModule.IsAlgClosed
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : IsAlgClosed F
inst_2 : Ring R
inst_3 : Algebra F R
inst_4 : IsSemisimpleRing R
inst_5 : FiniteDimensional F R
⊢ ∃ (n : ℕ) (d : Fin n → ℕ),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[F] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) F)

Tactic:
have ⟨n, D, d, _, _, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_divisionRing_finite F R
  ⟨n, d, hd, ⟨e.trans <| .piCongrRight fun i ↦ .mapMatrix <| .symm <| .ofBijective
    (Algebra.ofId F (D i)) IsAlgClosed.algebraMap_bijective_of_isIntegral⟩⟩

Premises used: AlgEquiv.symm, AlgEquiv.ofBijective, Exists, AlgEquiv.piCongrRight, AlgEquiv.mapMatrix, Nonempty.intro, Algebra.ofId, And, AlgEquiv.trans, AlgEquiv, IsAlgClosed.algebraMap_bijective_of_isIntegral, And.intro, Exists.intro, Nonempty, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite, _private.0.IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed.match_1
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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
h : IsIsotypicOfType R M S
⊢ IsIsotypic R M

Tactic:
fun m _ m' _ ↦ ⟨(h m').some.trans (h m).some.symm⟩

Premises used: LinearEquiv.symm, Nonempty.some, Nonempty.intro, IsIsotypicOfType, IsIsotypic, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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 : Subsingleton M
⊢ IsIsotypicOfType R M S

Tactic:
fun S ↦ have := IsSimpleModule.nontrivial R S
    (not_subsingleton _ S.subtype_injective.subsingleton).elim

Premises used: IsSimpleModule.nontrivial, Function.Injective.subsingleton, False.elim, Membership.mem, Subtype, not_subsingleton, IsIsotypicOfType, Submodule.subtype_injective
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Subsingleton M
⊢ IsIsotypic R M

Tactic:
fun S ↦ (IsIsotypicOfType.of_subsingleton R M S).isIsotypic S

Premises used: IsIsotypicOfType.isIsotypic, Membership.mem, Subtype, IsIsotypicOfType.of_subsingleton, IsIsotypic
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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
⊢ S = ⊤

Tactic:
rw [isSimpleModule_iff_isAtom, isAtom_iff_eq_top] at hS

Premises used: isSimpleModule_iff_isAtom, isAtom_iff_eq_top
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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 : S = ⊤
⊢ Nonempty.{u + 1} (↥S ≃ₗ[R] M)

Tactic:
⟨.trans (.ofEq _ _ hS) Submodule.topEquiv⟩

Premises used: Submodule.topEquiv, LinearEquiv.ofEq, Nonempty.intro, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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 : S = ⊤
⊢ Nonempty.{u + 1} (↥S ≃ₗ[R] M)

Tactic:
exact ⟨.trans (.ofEq _ _ hS) Submodule.topEquiv⟩
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleRing R
h : IsIsotypic R R
⊢ IsIsotypic R M

Tactic:
fun m _ m' _ ↦
    have ⟨_, ⟨e⟩⟩ := IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule R m
    have ⟨_, ⟨e'⟩⟩ := IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule R m'
    have := IsSimpleModule.congr e.symm
    have := IsSimpleModule.congr e'.symm
    ⟨e'.trans <| (h _ _).some.trans e.symm⟩

Premises used: LinearEquiv.symm, IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule, Membership.mem, Subtype, Nonempty.some, _private.0.IsIsotypic.of_self.match_1, Nonempty.intro, LinearEquiv, IsIsotypicOfType, Nonempty, IsIsotypic, RingHom.id, LinearEquiv.trans, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup S
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R S
h : IsIsotypicOfType R M S
e : S ≃ₗ[R] N
⊢ IsIsotypicOfType R M N

Tactic:
fun m _ ↦ ⟨(h m).some.trans e⟩

Premises used: Nonempty.some, Nonempty.intro, IsIsotypicOfType, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup S
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R S
h : IsIsotypicOfType R N S
f : M →ₗ[R] N
inj : Function.Injective.{u + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsIsotypicOfType R M S

Tactic:
fun m ↦
  have em := m.equivMapOfInjective f inj
  have := IsSimpleModule.congr em.symm
  ⟨em.trans (h (m.map f)).some⟩

Premises used: LinearEquiv.symm, Submodule.equivMapOfInjective, Nonempty.some, Nonempty.intro, IsIsotypicOfType, Submodule.map, LinearEquiv.trans, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
h : IsIsotypic R N
f : M →ₗ[R] N
inj : Function.Injective.{u + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsIsotypic R M

Tactic:
fun m _ ↦
  have em := (m.equivMapOfInjective f inj).symm
  have := IsSimpleModule.congr em
  ((h (m.map f)).of_injective f inj).of_linearEquiv_type em

Premises used: LinearEquiv.symm, IsIsotypicOfType.of_injective, Submodule.equivMapOfInjective, IsIsotypicOfType.of_linearEquiv_type, IsIsotypic, Submodule.map, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup S
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R S
e : M ≃ₗ[R] N
⊢ IsIsotypicOfType R M S ↔ IsIsotypicOfType R N S

Tactic:
⟨(·.of_injective _ e.symm.injective), (·.of_injective _ e.injective)⟩

Premises used: LinearEquiv.symm, IsIsotypicOfType.of_injective, LinearEquiv.toLinearMap, Iff.intro, LinearEquiv.injective
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup S
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R S
e : N ≃ₗ[R] S
⊢ IsIsotypicOfType R M N ↔ IsIsotypicOfType R M S

Tactic:
⟨(·.of_linearEquiv_type e), (·.of_linearEquiv_type e.symm)⟩

Premises used: LinearEquiv.symm, IsIsotypicOfType.of_linearEquiv_type, Iff.intro
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ IsIsotypic R M ↔ IsIsotypic R N

Tactic:
⟨(·.of_injective _ e.symm.injective), (·.of_injective _ e.injective)⟩

Premises used: LinearEquiv.symm, IsIsotypic.of_injective, LinearEquiv.toLinearMap, Iff.intro, LinearEquiv.injective
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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
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)
⊢ 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)

Tactic:
rw [Subtype.forall', ← (Submodule.MapSubtype.orderIso N).forall_congr_right]

Premises used: Submodule.MapSubtype.orderIso, RelIso.toEquiv, Equiv.forall_congr_right, Subtype.forall'
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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
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)
⊢ 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
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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)
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)
⊢ 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:
simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff]

Premises used: Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, LinearEquiv.isSimpleModule_iff
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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 ↥a],
      Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥(Submodule.map N.subtype a)) S)

Tactic:
forall₂_congr fun m _ ↦ ⟨fun ⟨e'⟩ ↦ ⟨(e m).symm.trans e'⟩, fun ⟨e'⟩ ↦ ⟨(e m).trans e'⟩⟩

Premises used: LinearEquiv.symm, Set.Mem, _private.0.isIsotypicOfType_submodule_iff.match_4, Membership.mem, Subtype, Nonempty.intro, _private.0.isIsotypicOfType_submodule_iff.match_3, forall₂_congr, LinearEquiv, Iff.intro, Submodule.subtype, IsIsotypicOfType, Nonempty, Submodule.map, RingHom.id, LinearEquiv.trans
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
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 ↥a],
      Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥(Submodule.map N.subtype a)) S)

Tactic:
exact forall₂_congr fun m _ ↦ ⟨fun ⟨e'⟩ ↦ ⟨(e m).symm.trans e'⟩, fun ⟨e'⟩ ↦ ⟨(e m).trans e'⟩⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
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)
⊢ IsIsotypic.{u, u_2} R ↥N ↔ ∀ m ≤ N, ∀ [IsSimpleModule.{u_2, u} R ↥m], IsIsotypicOfType.{u, u_2, u} R ↥N ↥m

Tactic:
rw [Subtype.forall', ← (Submodule.MapSubtype.orderIso N).forall_congr_right]

Premises used: Submodule.MapSubtype.orderIso, RelIso.toEquiv, Equiv.forall_congr_right, Subtype.forall'
-- Module: Mathlib.RingTheory.SimpleModule.Isotypic
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
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)
⊢ 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