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
s : Set (Submodule R M)
ind :
  iSupIndep.{u_4 + 1, u_4} (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule.{u_2, u_4} R ↥m
rw :
  Eq.{u_4 + 1} (α := Submodule R M)
    (iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s))) ⊤
rw₁ : iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s)) = SupSet.sSup s
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (LinearMap.range (R := R) (M := Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)) (τ₁₂ := RingHom.id R)
      ((DFinsupp.lsum ℕ (M := fun (i : { x : Submodule R M // x ∈ s }) ↦ ↥(↑i : Submodule R M)) :
          (a : (i : { x : Submodule R M // x ∈ s }) → ↥(↑i : Submodule R M) →ₗ[R] M) →
            (Π₀ (i : { x : Submodule R M // x ∈ s }), ↥(↑i : Submodule R M)) →ₗ[R] M)
        fun (i : { x : Submodule R M // x ∈ s }) ↦ (↑i : Submodule R M).subtype))
    ⊤
have rw₂ : Eq.{u_4 + 1} (α := Submodule R M)
  (iSup (ι := { x : Submodule R M // x ∈ s }) (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ s)))
  (⨆ (a : (↑s : Type u_4)), (↑a : Submodule R M))
Tactic: rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']
-- 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
⊢ IsSemisimpleModule R M ↔
    ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
      ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
have refine : IsSemisimpleModule R M →
  ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
Tactic: refine ⟨fun _ ↦ ?_, fun ⟨s, e, h⟩ ↦ .congr e⟩
-- 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
h : IsSemisimpleModule R M
⊢ ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
have have : ∀ (s : Set (Submodule R M)) (e : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M))
  (h : sSupIndep s ∧ ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)),
  ∃ (s : Set (Submodule R M)) (x : M ≃ₗ[R] Π₀ (m : (↑s : Type u_4)), ↥(↑m : Submodule R M)),
    ∀ (m : (↑s : Type u_4)), IsSimpleModule.{u_2, u_4} R ↥(↑m : Submodule R M)
Tactic: have ⟨s, e, h⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M_1 : Type u_4
inst_2 : AddCommGroup M_1
inst_3 : Module R M_1
m : Submodule R M_1
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_7
inst_6 : Finite ι
M : ι → Type u_6
inst_7 : (i : ι) → AddCommGroup (M i)
inst_8 : (i : ι) → Module.{u_2, u_6} R (M i)
inst_9 : ∀ (i : ι), IsSemisimpleModule.{u_2, u_6} R (M i)
simp_rw simp_rw₁ :
  Eq (α := Submodule R ((i : ι) → M i)) (⨆ (i : ι), range (R := R) (M := M i) (τ₁₂ := RingHom.id R) (single R M i)) ⊤
⊢ Eq (α := Submodule R ((i : ι) → M i))
    (⨆ (i : ι),
      (fun (x : ι) ↦ (range (R := R) (M := M x) (τ₁₂ := RingHom.id R) (single R M x) : Submodule R ((i : ι) → M i))) i)
    ⊤
have simp_rw₂ : Eq (α := Submodule R ((i : ι) → M i))
  (⨆ (i : ι), Submodule.map (R := R) (M := M i) (σ₁₂ := RingHom.id R) (single R M i) ⊤) ⊤
Tactic: simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
ι_1 : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M_1 : Type u_4
inst_2 : AddCommGroup M_1
inst_3 : Module R M_1
m : Submodule R M_1
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_7
inst_6 : Finite ι
M : ι → Type u_6
inst_7 : (i : ι) → AddCommGroup (M i)
inst_8 : (i : ι) → Module.{u_2, u_6} R (M i)
inst_9 : ∀ (i : ι), IsSemisimpleModule.{u_2, u_6} R (M i)
simp_rw simp_rw₁ :
  Eq (α := Submodule R ((i : ι) → M i)) (⨆ (i : ι), range (R := R) (M := M i) (τ₁₂ := RingHom.id R) (single R M i)) ⊤
simp_rw₂ :
  Eq (α := Submodule R ((i : ι) → M i))
    (⨆ (i : ι), Submodule.map (R := R) (M := M i) (σ₁₂ := RingHom.id R) (single R M i) ⊤) ⊤
⊢ Eq (α := Submodule R ((i : ι) → M i))
    (⨆ (i : ι),
      (fun (x : ι) ↦ (range (R := R) (M := M x) (τ₁₂ := RingHom.id R) (single R M x) : Submodule R ((i : ι) → M i))) i)
    ⊤
have simp_rw₃ : Eq (α := Submodule R ((i : ι) → M i)) (Submodule.pi (φ := M) Set.univ fun (i : ι) ↦ ⊤ : Submodule R ((i : ι) → M i)) ⊤
Tactic: simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top]
-- 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
p q : Submodule R M
h : IsSemisimpleModule.{u_2, u_4} R ↥p
h_1 : IsSemisimpleModule.{u_2, u_4} R ↥q
f : Bool → Submodule R M := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ Submodule R M) q p t
⊢ p ⊔ q = ⨆ (i : Bool), ⨆ (_ : Membership.mem (γ := Set Bool) Set.univ i), f i
have rw : p ⊔ q = ⨆ (x : Bool), f x
Tactic: rw [iSup_univ, iSup_bool_eq]
-- 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
p q : Submodule R M
h : IsSemisimpleModule.{u_2, u_4} R ↥p
h_1 : IsSemisimpleModule.{u_2, u_4} R ↥q
f : Bool → Submodule R M := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ Submodule R M) q p t
rw : p ⊔ q = ⨆ (x : Bool), f x
⊢ p ⊔ q = ⨆ (i : Bool), ⨆ (_ : Membership.mem (γ := Set Bool) Set.univ i), f i
have rw₁ : p ⊔ q = f true ⊔ f false
Tactic: rw [iSup_univ, iSup_bool_eq]
-- 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
p q : Submodule R M
h : IsSemisimpleModule.{u_2, u_4} R ↥p
h_1 : IsSemisimpleModule.{u_2, u_4} R ↥q
f : Bool → Submodule R M := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ Submodule R M) q p t
⊢ IsSemisimpleModule.{u_2, u_4} R ↥(p ⊔ q)
have rw : IsSemisimpleModule.{u_2, u_4} R ↥(⨆ (i : Bool), ⨆ (_ : Membership.mem (γ := Set Bool) Set.univ i), f i)
Tactic: rw [show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
Goal:
ι_1 : 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
ι : Type u_7
inst_6 : Finite ι
R : ι → Type u_6
inst_7 : (i : ι) → Ring (R i)
inst_8 : ∀ (i : ι), IsSemisimpleRing.{u_6} (R i)
x : (i : ι) → Module ((i : ι) → R i) (R i) := fun (i : ι) ↦ Module.compHom (R := R i) (R i) (Pi.evalRingHom R i)
e : (i : ι) → LinearMap (R := (i : ι) → R i) (S := R i) (Pi.evalRingHom R i) (R i) (R i) :=
  fun (i : ι) ↦
    let __src : R i →+ R i := AddMonoidHom.id (R i);
    { toFun := (↑__src : ZeroHom (R i) (R i)).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing ((i : ι) → R i)
have this : ∀ (i : ι), IsSemisimpleModule ((i : ι) → R i) (R i)
Tactic: have (i : _) : IsSemisimpleModule (Π i, R i) (R i) :=
    ((e i).isSemisimpleModule_iff_of_bijective Function.bijective_id).mpr inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
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
hR : IsSemisimpleRing R
hS : IsSemisimpleRing S
this_1 : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S)
this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R 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' := ⋯ }
hS₁ : IsSemisimpleRing S
⊢ IsSemisimpleRing (R × S)
have hR₁ : let this : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S);
IsSemisimpleModule (R × S) R
Tactic: rw [IsSemisimpleRing, ← _e₁.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hR
Cleared hypotheses: hR, hS, this_1, this, _e₁, _e₂
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
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
hS : IsSemisimpleRing S
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)
_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' := ⋯ }
hR₁ :
  let this : Module (R × S) R := Module.compHom (R := R) R (RingHom.fst R S);
  IsSemisimpleModule (R × S) R
⊢ IsSemisimpleRing (R × S)
have hS₁ : let this : Module (R × S) S := Module.compHom (R := S) S (RingHom.snd R S);
IsSemisimpleModule (R × S) S
Tactic: rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS
Cleared hypotheses: hS, this_1, hR, this, _e₁, _e₂
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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' := ⋯ }
⊢ IsSemisimpleRing (R × S)
have rw : 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: rw [IsSemisimpleRing, ← Submodule.topEquiv.isSemisimpleModule_iff_of_bijective
    (LinearEquiv.bijective _), ← LinearMap.sup_range_inl_inr]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (hypothesis)
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
⊢ IsSemisimpleRing S
have this₁ : RingHomSurjective f
Tactic: haveI : RingHomSurjective f := ⟨hf⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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' := ⋯ }
⊢ IsSemisimpleRing S
have rw : IsSemisimpleModule R S
Tactic: rw [IsSemisimpleRing, ← e.isSemisimpleModule_iff_of_bijective Function.bijective_id]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : IsSemisimpleRing R
I : Ideal R
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = Ideal.span {e}
have obtain : ∀ (J : Ideal R) (h : IsCompl I J), ∃ (e : R), IsIdempotentElem e ∧ I = Ideal.span {e}
Tactic: obtain ⟨J, h⟩ := exists_isCompl I
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : IsSemisimpleRing R
I J : Ideal R
h : IsCompl I J
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = Ideal.span {e}
have 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}
Tactic: obtain ⟨f, idem, rfl⟩ := I.isIdempotentElemEquiv.symm (I.isComplEquivProj ⟨J, h⟩)
Cleared hypotheses: I, h
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ LinearMap.range f = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
have rw : Submodule.map 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]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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))
⊢ LinearMap.range f = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
have rw₁ : Submodule.map f (Ideal.span 1) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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))
⊢ LinearMap.range f = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
have rw₂ : Submodule.map f (Submodule.span R 1) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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))
⊢ LinearMap.range f = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
have 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)))
Tactic: rw [LinearMap.range_eq_map, ← Ideal.span_one, ← Ideal.submodule_span_eq, LinearMap.map_span,
      Set.image_one, Ideal.submodule_span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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)))
⊢ LinearMap.range f = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
have 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)))
Tactic: rw [LinearMap.range_eq_map, ← Ideal.span_one, ← Ideal.submodule_span_eq, LinearMap.map_span,
      Set.image_one, Ideal.submodule_span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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)))
⊢ LinearMap.range f = Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R))
have rw₅ : Eq (α := Ideal R) (Ideal.span (singleton (α := R) ((f : (a : R) → R) 1 : R)))
  (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]
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R M
f : M →ₗ[R] N
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∨ f = 0
have rw : f.ker = ⊥ ∨ f.ker = ⊤
Tactic: rw [← ker_eq_bot, ← ker_eq_top]
-- 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
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∨ f = 0
have rw : f.range = ⊥ ∨ f.range = ⊤
Tactic: rw [← range_eq_top, ← range_eq_bot, or_comm]
-- 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
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)
⊢ IsCoatom f.ker
have rw : IsSimpleModule.{u_2, u_4} R (M ⧸ f.ker)
Tactic: rw [← isSimpleModule_iff_isCoatom]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ (a * if h : a = 0 then 0 else (↑(LinearEquiv.symm (LinearEquiv.ofBijective a ⋯)) : M →ₗ[R] M)) = 1
have simp_rw : a * (↑(LinearEquiv.symm (LinearEquiv.ofBijective a sorry)) : M →ₗ[R] M) = 1
Tactic: simp_rw [dif_neg a0]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ a * (↑(LinearEquiv.symm (LinearEquiv.ofBijective a ⋯)) : M →ₗ[R] M) = 1
have h : ∀ (x : M),
  Eq (α := M) ((a * (↑(LinearEquiv.symm (LinearEquiv.ofBijective a sorry)) : M →ₗ[R] M) : (a : M) → M) x : M)
    ((1 : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ (↥(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
have 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
Tactic: rw [sup_comm, inf_comm]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Basic (goal)
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
⊢ (↥(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
have val : (↥(Y ⊔ X) ⧸ Submodule.comap (Y ⊔ X).subtype X) ≃ₗ[R] ↥Y ⧸ Submodule.comap Y.subtype Y ⊓ Submodule.comap Y.subtype X
Tactic: dsimp
-- 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
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) ((f : (a : ↥s →₀ M) → ↥s →₀ M) x : ↥s →₀ M)
have 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)
Tactic: rw [← this, map_smul, End.smul_def]
-- 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
⊢ 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)
have 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)
Tactic: have ⟨s, hs⟩ := Module.Finite.fg_top (R := End R M) (M := M)