awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
this_1 : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S)
hS : IsSemisimpleModule (R × S) S
_e₁ : LinearMap (R := R × S) (S := R) (RingHom.fst R S) R R :=
  let __src : R →+ R := AddMonoidHom.id R;
  { toFun := (↑__src : ZeroHom R R).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : LinearMap (R := R × S) (S := S) (RingHom.snd R S) S S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleModule (R × S)
    ↥(LinearMap.range (LinearMap.inl (R × S) R S) ⊔ LinearMap.range (LinearMap.inr (R × S) R S) :
        Submodule (R × S) (R × S))

Tactic:
.sup (.range _) (.range _)

Premises used: Set.Mem, setOf, IsSemisimpleModule.sup, IsSemisimpleModule.range
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
this_1 : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S)
hS : IsSemisimpleModule (R × S) S
_e₁ : LinearMap (R := R × S) (S := R) (RingHom.fst R S) R R :=
  let __src : R →+ R := AddMonoidHom.id R;
  { toFun := (↑__src : ZeroHom R R).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : LinearMap (R := R × S) (S := S) (RingHom.snd R S) S S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleModule (R × S)
    ↥(LinearMap.range (LinearMap.inl (R × S) R S) ⊔ LinearMap.range (LinearMap.inr (R × S) R S) :
        Submodule (R × S) (R × S))

Tactic:
exact .sup (.range _) (.range _)
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsSemisimpleRing R
this : Module R S := Module.compHom S f
⊢ RingHomSurjective f

Tactic:
haveI : RingHomSurjective f := ⟨hf⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsSemisimpleRing R
this_1 : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
rw : IsSemisimpleModule R S
⊢ IsSemisimpleRing S

Tactic:
rw [IsSemisimpleRing, ← e.isSemisimpleModule_iff_of_bijective Function.bijective_id]

Premises used: Function.bijective_id, LinearMap.isSemisimpleModule_iff_of_bijective, IsSemisimpleRing
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsSemisimpleRing R
this_1 : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src : S →+ S := AddMonoidHom.id S;
  { toFun := (↑__src : ZeroHom S S).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleModule R S

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
inst_1 : IsSemisimpleRing R
I : Ideal R
obtain : ∀ (J : Ideal R) (h : IsCompl I J), ∃ (e : R), IsIdempotentElem e ∧ I = Ideal.span {e}
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = Ideal.span {e}

Tactic:
obtain ⟨J, h⟩ := exists_isCompl I

Premises used: ComplementedLattice.exists_isCompl
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
inst_1 : IsSemisimpleRing R
I J : Ideal R
h : IsCompl I J
obtain :
  ∀ (f : Module.End R R) (idem : IsIdempotentElem f) (h : IsCompl (LinearMap.range f) J),
    ∃ (e : R), IsIdempotentElem e ∧ LinearMap.range f = Ideal.span {e}
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = Ideal.span {e}

Tactic:
obtain ⟨f, idem, rfl⟩ := I.isIdempotentElemEquiv.symm (I.isComplEquivProj ⟨J, h⟩)

Premises used: Subtype.mk, Submodule.isComplEquivProj, Equiv.symm, DFunLike.coe, Submodule.isIdempotentElemEquiv, rfl
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
inst_1 : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
rw : Submodule.map f ⊤ = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
rw₁ : Submodule.map f (Ideal.span 1) = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
rw₂ : Submodule.map f (Submodule.span R 1) = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
rw₃ :
  Eq (α := Ideal R) (Submodule.span R (Set.image (α := R) (⇑f : (a : R) → R) 1))
    (Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R)))
rw₄ :
  Eq (α := Ideal R) (Submodule.span R (singleton (α := R) ((f : (a : R) → R) 1 : R)))
    (Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R)))
rw₅ rw₆ :
  Eq (α := Ideal R) (Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R)))
    (Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R)))
⊢ LinearMap.range f = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))

Tactic:
rw [LinearMap.range_eq_map, ← Ideal.span_one, ← Ideal.submodule_span_eq, LinearMap.map_span,
      Set.image_one, Ideal.submodule_span_eq]

Premises used: Ideal.submodule_span_eq, Set.image_one, Ideal.span_one, LinearMap.map_span, LinearMap.range_eq_map
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
inst_1 : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ ∃ (e : R), IsIdempotentElem e ∧ LinearMap.range f = Ideal.span {e}

Tactic:
exact ⟨f 1, LinearMap.isIdempotentElem_map_one_iff.mpr idem, by
    rw [LinearMap.range_eq_map, ← Ideal.span_one, ← Ideal.submodule_span_eq, LinearMap.map_span,
      Set.image_one, Ideal.submodule_span_eq]⟩
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R M
f : M →ₗ[R] N
rw : f.ker = ⊥ ∨ f.ker = ⊤
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∨ f = 0

Tactic:
rw [← ker_eq_bot, ← ker_eq_top]

Premises used: LinearMap.ker_eq_top, LinearMap.ker_eq_bot
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R M
f : M →ₗ[R] N
⊢ f.ker = ⊥ ∨ f.ker = ⊤

Tactic:
apply eq_bot_or_eq_top

Premises used: IsSimpleOrder.eq_bot_or_eq_top
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R M
f : M →ₗ[R] N
h : f ≠ 0
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
f.injective_or_eq_zero.resolve_right h

Premises used: Or.resolve_right, LinearMap.injective_or_eq_zero
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R N
f : M →ₗ[R] N
rw : f.range = ⊥ ∨ f.range = ⊤
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∨ f = 0

Tactic:
rw [← range_eq_top, ← range_eq_bot, or_comm]

Premises used: LinearMap.range_eq_bot, LinearMap.range_eq_top, or_comm
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R N
f : M →ₗ[R] N
⊢ f.range = ⊥ ∨ f.range = ⊤

Tactic:
apply eq_bot_or_eq_top

Premises used: IsSimpleOrder.eq_bot_or_eq_top
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R N
f : M →ₗ[R] N
h : f ≠ 0
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
f.surjective_or_eq_zero.resolve_right h

Premises used: LinearMap.surjective_or_eq_zero, Or.resolve_right
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R M
inst_6 : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Bijective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∨ f = 0

Tactic:
or_iff_not_imp_right.mpr fun h ↦ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, And.intro, LinearMap.surjective_of_ne_zero, LinearMap.injective_of_ne_zero
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R M
inst_6 : IsSimpleModule R N
f : M →ₗ[R] N
h : f ≠ 0
⊢ Function.Bijective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
f.bijective_or_eq_zero.resolve_right h

Premises used: LinearMap.bijective_or_eq_zero, Or.resolve_right
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw : IsSimpleModule.{u_2, u_4} R (M ⧸ f.ker)
⊢ IsCoatom f.ker

Tactic:
rw [← isSimpleModule_iff_isCoatom]

Premises used: isSimpleModule_iff_isCoatom
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsSimpleModule.{u_2, u_4} R (M ⧸ f.ker)

Tactic:
IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)

Premises used: LinearMap.quotKerEquivOfSurjective, IsSimpleModule.congr
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsSimpleModule.{u_2, u_4} R (M ⧸ f.ker)

Tactic:
exact IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)

Premises used: LinearMap.quotKerEquivOfSurjective, IsSimpleModule.congr
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
inst_6 : IsSimpleModule R N
f : M →ₗ[R] N
h : f ≠ 0
⊢ ∃ (S : Submodule R M), Nonempty (LinearEquiv.{u_2, u_2, u_5, u_4} (RingHom.id R) N ↥S)

Tactic:
have ⟨m, (_ : IsSimpleModule R m), ne⟩ :=
    exists_ne_zero_of_sSup_eq_top h _ (IsSemisimpleModule.sSup_simples_eq_top ..)
  ⟨m, ⟨.symm <| .ofBijective _ ((bijective_or_eq_zero _).resolve_right ne)⟩⟩

Premises used: LinearMap.exists_ne_zero_of_sSup_eq_top, LinearEquiv.symm, setOf, Membership.mem, Exists, Subtype, _private.0.LinearMap.linearEquiv_of_ne_zero.match_1, IsSimpleModule, Nonempty.intro, LinearMap.comp, IsSemisimpleModule.sSup_simples_eq_top, LinearMap.bijective_or_eq_zero, LinearEquiv, Exists.intro, Submodule.subtype, Nonempty, Or.resolve_right, RingHom.id, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : DecidableEq (Module.End R M)
inst_7 : IsSimpleModule R M
a : Module.End R M
a0 : a ≠ 0
simp_rw : a * (↑(LinearEquiv.symm (LinearEquiv.ofBijective a ⋯)) : M →ₗ[R] M) = 1
⊢ (a * if h : a = 0 then 0 else (↑(LinearEquiv.symm (LinearEquiv.ofBijective a ⋯)) : M →ₗ[R] M)) = 1

Tactic:
simp_rw [dif_neg a0]

Premises used: dif_neg
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : DecidableEq (Module.End R M)
inst_7 : IsSimpleModule R M
a : Module.End R M
a0 : a ≠ 0
h :
  ∀ (x : M),
    Eq (α := M) ((a * (↑(LinearEquiv.symm (LinearEquiv.ofBijective a ⋯)) : M →ₗ[R] M) : (a : M) → M) x : M)
      ((1 : (a : M) → M) x : M)
⊢ a * (↑(LinearEquiv.symm (LinearEquiv.ofBijective a ⋯)) : M →ₗ[R] M) = 1

Tactic:
ext
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : DecidableEq (Module.End R M)
inst_7 : IsSimpleModule R M
a : Module.End R M
a0 : a ≠ 0
x : M
⊢ Eq (α := M) ((a * (↑(LinearEquiv.symm (LinearEquiv.ofBijective a ⋯)) : M →ₗ[R] M) : (a : M) → M) x : M)
    ((1 : (a : M) → M) x : M)

Tactic:
(LinearEquiv.ofBijective _ <| bijective_of_ne_zero a0).right_inv _

Premises used: LinearEquiv.right_inv, Classical.choose, LinearMap.bijective_of_ne_zero, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : DecidableEq (Module.End R M)
inst_7 : IsSimpleModule R M
a : Module.End R M
a0 : a ≠ 0
x : M
⊢ Eq (α := M) ((a * (↑(LinearEquiv.symm (LinearEquiv.ofBijective a ⋯)) : M →ₗ[R] M) : (a : M) → M) x : M)
    ((1 : (a : M) → M) x : M)

Tactic:
exact (LinearEquiv.ofBijective _ <| bijective_of_ne_zero a0).right_inv _

Premises used: LinearEquiv.right_inv, LinearMap.bijective_of_ne_zero, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Ring R_1
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
m : Submodule R_1 M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R_1 N
R : Type u_6
inst_6 : DivisionRing R
inst_7 : Module R M
inst_8 : Nontrivial M
v : M
hv : v ≠ 0
w : M
f : M →ₗ[R] M
eq : f ∘ₗ toSpanSingleton R M v = toSpanSingleton R M w
⊢ (toSpanSingleton (Module.End R M) M v : (a : Module.End R M) → M) f = w

Tactic:
simpa using congr($eq 1)
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
X Y : Submodule R M
h : X ⋖ X ⊔ Y
val :
  (↥(X, X ⊔ Y).2 ⧸ Submodule.comap (X, X ⊔ Y).2.subtype (X, X ⊔ Y).1) ≃ₗ[R]
    ↥(X ⊓ Y, Y).2 ⧸ Submodule.comap (X ⊓ Y, Y).2.subtype (X ⊓ Y, Y).1
⊢ Nonempty.{u_4 + 1}
    ((↥(X, X ⊔ Y).2 ⧸ Submodule.comap (X, X ⊔ Y).2.subtype (X, X ⊔ Y).1) ≃ₗ[R]
      ↥(X ⊓ Y, Y).2 ⧸ Submodule.comap (X ⊓ Y, Y).2.subtype (X ⊓ Y, Y).1)

Tactic:
constructor
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
X Y : Submodule R M
h : X ⋖ X ⊔ Y
val :
  (↥(X, Y ⊔ X).2 ⧸ Submodule.comap (X, Y ⊔ X).2.subtype (X, Y ⊔ X).1) ≃ₗ[R]
    ↥(Y ⊓ X, Y).2 ⧸ Submodule.comap (Y ⊓ X, Y).2.subtype (Y ⊓ X, Y).1
⊢ (↥(X, X ⊔ Y).2 ⧸ Submodule.comap (X, X ⊔ Y).2.subtype (X, X ⊔ Y).1) ≃ₗ[R]
    ↥(X ⊓ Y, Y).2 ⧸ Submodule.comap (X ⊓ Y, Y).2.subtype (X ⊓ Y, Y).1

Tactic:
rw [sup_comm, inf_comm]

Premises used: inf_comm, sup_comm
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
X Y : Submodule R M
h : X ⋖ X ⊔ Y
val :
  (↥(Y ⊔ X) ⧸ Submodule.comap (Y ⊔ X).subtype X) ≃ₗ[R] ↥Y ⧸ Submodule.comap Y.subtype Y ⊓ Submodule.comap Y.subtype X
⊢ (↥(X, Y ⊔ X).2 ⧸ Submodule.comap (X, Y ⊔ X).2.subtype (X, Y ⊔ X).1) ≃ₗ[R]
    ↥(Y ⊓ X, Y).2 ⧸ Submodule.comap (Y ⊓ X, Y).2.subtype (Y ⊓ X, Y).1

Tactic:
dsimp
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
X Y : Submodule R M
h : X ⋖ X ⊔ Y
⊢ (↥(Y ⊔ X) ⧸ Submodule.comap (Y ⊔ X).subtype X) ≃ₗ[R] ↥Y ⧸ Submodule.comap Y.subtype Y ⊓ Submodule.comap Y.subtype X

Tactic:
exact (LinearMap.quotientInfEquivSupQuotient Y X).symm

Premises used: LinearEquiv.symm, LinearMap.quotientInfEquivSupQuotient
-- 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
f_1 : End (End R M) M
s : Finset M
x : ↥s →₀ M := (Equiv.symm Finsupp.equivFunOnFinite : (a : ↥s → M) → ↥s →₀ M) fun (x : ↥s) ↦ (↑x : M)
w : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := projection (R ∙ x) w h
f : End (End R (↥s →₀ M)) (↥s →₀ M) :=
  (End.ringHomEndFinsupp ↥s : (a : End (End R M) M) → End (End R (↥s →₀ M)) (↥s →₀ M)) f_1
this : Eq (α := ↥s →₀ M) ((f : (a : ↥s →₀ M) → ↥s →₀ M) (p • x) : ↥s →₀ M) ((f : (a : ↥s →₀ M) → ↥s →₀ M) x : ↥s →₀ M)
rw :
  Membership.mem (α := ↥s →₀ M) (γ := Submodule R (↥s →₀ M)) (R ∙ x)
    ((p : (a : ↥s →₀ M) → ↥s →₀ M) ((f : (a : ↥s →₀ M) → ↥s →₀ M) x) : ↥s →₀ M)
⊢ Membership.mem (α := ↥s →₀ M) (γ := Submodule R (↥s →₀ M)) (R ∙ x) ((f : (a : ↥s →₀ M) → ↥s →₀ M) x : ↥s →₀ M)

Tactic:
rw [← this, map_smul, End.smul_def]

Premises used: Module.End.smul_def, 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
f_1 : End (End R M) M
s : Finset M
x : ↥s →₀ M := (Equiv.symm Finsupp.equivFunOnFinite : (a : ↥s → M) → ↥s →₀ M) fun (x : ↥s) ↦ (↑x : M)
w : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := projection (R ∙ x) w h
f : End (End R (↥s →₀ M)) (↥s →₀ M) :=
  (End.ringHomEndFinsupp ↥s : (a : End (End R M) M) → End (End R (↥s →₀ M)) (↥s →₀ M)) f_1
this : Eq (α := ↥s →₀ M) ((f : (a : ↥s →₀ M) → ↥s →₀ M) (p • x) : ↥s →₀ M) ((f : (a : ↥s →₀ M) → ↥s →₀ M) x : ↥s →₀ M)
⊢ Membership.mem (α := ↥s →₀ M) (γ := Submodule R (↥s →₀ M)) (R ∙ x)
    ((p : (a : ↥s →₀ M) → ↥s →₀ M) ((f : (a : ↥s →₀ M) → ↥s →₀ M) x) : ↥s →₀ M)

Tactic:
apply projection_apply_mem

Premises used: Submodule.projection_apply_mem
-- 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
f_1 : End (End R M) M
s : Finset M
x : ↥s →₀ M := (Equiv.symm Finsupp.equivFunOnFinite : (a : ↥s → M) → ↥s →₀ M) fun (x : ↥s) ↦ (↑x : M)
w : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := projection (R ∙ x) w h
f : End (End R (↥s →₀ M)) (↥s →₀ M) :=
  (End.ringHomEndFinsupp ↥s : (a : End (End R M) M) → End (End R (↥s →₀ M)) (↥s →₀ M)) f_1
this_1 : Eq (α := ↥s →₀ M) ((f : (a : ↥s →₀ M) → ↥s →₀ M) (p • x) : ↥s →₀ M) ((f : (a : ↥s →₀ M) → ↥s →₀ M) x : ↥s →₀ M)
this : Membership.mem (α := ↥s →₀ M) (γ := Submodule R (↥s →₀ M)) (R ∙ x) ((f : (a : ↥s →₀ M) → ↥s →₀ M) x : ↥s →₀ M)
r : R
hr : r • x = (f : (a : ↥s →₀ M) → ↥s →₀ M) x
m : M
hm : m ∈ s
⊢ (f_1 : (a : M) → M) m = r • m

Tactic:
simpa [x] using congr($hr ⟨m, hm⟩).symm

Premises used: congrArg, id, Subtype.mk, Eq.symm, DFunLike.coe
-- 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
have :
  ∀ (s : Finset M) (hs : Eq (α := Submodule (End R M) M) (span (End R M) (↑s : Set M)) ⊤),
    Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := End (End R M) M)
      (⇑(toModuleEnd (End R M) M) : (a : R) → End (End R M) M)
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := End (End R M) M)
    (⇑(toModuleEnd (End R M) M) : (a : R) → End (End R M) M)

Tactic:
have ⟨s, hs⟩ := Module.Finite.fg_top (R := End R M) (M := M)
-- 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
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
⊢ ∃ (a : R), (toModuleEnd (End R M) M : (a : R) → End (End R M) M) a = f

Tactic:
have ⟨r, hr⟩ := jacobson_density f s
-- 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
⊢ ∃ (a : R), (toModuleEnd (End R M) M : (a : R) → End (End R M) M) a = f

Tactic:
⟨r, LinearMap.ext fun m ↦ ?_⟩

Premises used: LinearMap.ext, Exists.intro
-- 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
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)
⊢ ∃ (a : R), (toModuleEnd (End R M) M : (a : R) → End (End R M) M) a = f

Tactic:
refine ⟨r, LinearMap.ext fun m ↦ ?_⟩
-- 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_1 m : M
hm : m ∈ (↑s : Set 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:
(hr m hm).symm

Premises used: Eq.symm
-- 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_1 m : M
hm : m ∈ (↑s : Set 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:
exact (hr m hm).symm

Premises used: Eq.symm