awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
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
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
have inl : ∀ (inj : Function.Injective.{u + 1, u_3 + 1} (α := ↥S) (β := N) (⇑(f ∘ₗ S.subtype) : (a : ↥S) → N)),
  (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
Tactic: obtain inj | eq := (f ∘ₗ S.subtype).injective_or_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
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
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
inl :
  ∀ (inj : Function.Injective.{u + 1, u_3 + 1} (α := ↥S) (β := N) (⇑(f ∘ₗ S.subtype) : (a : ↥S) → N)),
    (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
have inr : ∀ (eq : f ∘ₗ S.subtype = 0), (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
Tactic: obtain inj | eq := (f ∘ₗ S.subtype).injective_or_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
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
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
have inr : LE.le (α := Submodule R N) (LinearMap.range.{u_2, u_2, u, u_3} (R := R) (M := ↥S) (τ₁₂ := RingHom.id R) 0)
  (isotypicComponent.{u_3, u_2, u} R N ↥S)
Tactic: simp_rw [eq, LinearMap.range_zero, bot_le]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
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
S : Submodule R M
inst_5 : IsSimpleModule.{u_2, u} R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
inr :
  LE.le (α := Submodule R N) (LinearMap.range.{u_2, u_2, u, u_3} (R := R) (M := ↥S) (τ₁₂ := RingHom.id R) 0)
    (isotypicComponent.{u_3, u_2, u} R N ↥S)
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
have inr₁ : LE.le (α := Submodule R N) ⊥ (isotypicComponent.{u_3, u_2, u} R N ↥S)
Tactic: simp_rw [eq, LinearMap.range_zero, bot_le]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N_1 : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N_1
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N_1
inst_8 : Module R S
inst_9 : IsSimpleModule R S
ι : Type u_5
inst_10 : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : Eq.{u + 1} (α := Submodule R M) (⨆ (i : ι), N i) ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : (i : ι) → Module.End R ↥(N i)
⊢ (fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f ⋯)
      ((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
          (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
            DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
              (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
        f) =
    f
have h : ∀ (i : ι) (x : ↥(N i)),
  Eq.{u + 1} (α := M)
    (↑(((fun (f : Module.End R M) (i : ι) ↦ LinearMap.restrict f sorry)
              ((fun (f : (i : ι) → Module.End R ↥(N i)) ↦
                  (↑(ind.linearEquiv iSup_top) : (Π₀ (i : ι), ↥(N i)) →ₗ[R] M) ∘ₗ
                    DFinsupp.mapRange.linearMap (β₁ := fun (i : ι) ↦ ↥(N i)) (β₂ := fun (i : ι) ↦ ↥(N i)) f ∘ₗ
                      (↑(ind.linearEquiv iSup_top).symm : M →ₗ[R] Π₀ (i : ι), ↥(N i)))
                f)
              i :
            (a : ↥(N i)) → ↥(N i))
          x) :
      M)
    (↑((f i : (a : ↥(N i)) → ↥(N i)) x) : M)
Tactic: ext i x
-- 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
m : Submodule R M
h : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) m
⊢ m.IsFullyInvariant
have obtain : ∀ (w : Submodule R M), IsSimpleModule.{u_2, u} R ↥w → IsFullyInvariant (isotypicComponent R M ↥w)
Tactic: obtain ⟨_, _, rfl⟩ := h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : AddCommGroup S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : IsSimpleModule R S
s : Set (↑(isotypicComponents R M) : Type u)
c : (↑(isotypicComponents R M) : Type u)
hc :
  Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
    {c : (↑(isotypicComponents R M) : Type u) |
      (↑c : Submodule R M) ≤
        (↑(⨆ c ∈ s,
              Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x)
                (↑c : Submodule R M) ⋯) :
          Submodule R M)}
    c
hcs : c ∉ s
⊢ LE.le (α := Submodule R M)
    (↑(⨆ c ∈ s,
          Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x)
            (↑c : Submodule R M) ⋯) :
      Submodule R M)
    (sSup (isotypicComponents R M \ {(↑c : Submodule R M)}))
have simp_rw : ∀ (i : (↑(isotypicComponents R M) : Type u)) (j : i ∈ s),
  (↑i : Submodule R M) ≤ sSup (isotypicComponents R M \ {(↑c : Submodule R M)})
Tactic: simp_rw [CompleteSublattice.coe_iSup, iSup₂_le_iff]
-- 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 : IsSimpleModule R S
inst_6 : IsSemisimpleModule R M
⊢ Eq (α := Submodule R M) (isotypicComponent R M S) ⊤ ↔ IsIsotypicOfType R M S
have rw : LE.le (α := Submodule R M) ⊤ (isotypicComponent R M S) ↔ IsIsotypicOfType R M S
Tactic: rw [← top_le_iff, le_isotypicComponent_iff, Submodule.topEquiv.isIsotypicOfType_iff]
-- 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 : IsSimpleModule R S
inst_6 : IsSemisimpleModule R M
rw : LE.le (α := Submodule R M) ⊤ (isotypicComponent R M S) ↔ IsIsotypicOfType R M S
⊢ Eq (α := Submodule R M) (isotypicComponent R M S) ⊤ ↔ IsIsotypicOfType R M S
have rw₁ : IsIsotypicOfType.{u, u_2, u_4} R (↥⊤) S ↔ IsIsotypicOfType R M S
Tactic: rw [← top_le_iff, le_isotypicComponent_iff, Submodule.topEquiv.isIsotypicOfType_iff]
-- 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 : IsSimpleModule R S
inst_6 : IsSemisimpleModule R M
rw : LE.le (α := Submodule R M) ⊤ (isotypicComponent R M S) ↔ IsIsotypicOfType R M S
rw₁ : IsIsotypicOfType.{u, u_2, u_4} R (↥⊤) S ↔ IsIsotypicOfType R M S
⊢ Eq (α := Submodule R M) (isotypicComponent R M S) ⊤ ↔ IsIsotypicOfType R M S
have rw₂ : IsIsotypicOfType R M S ↔ IsIsotypicOfType R M S
Tactic: rw [← top_le_iff, le_isotypicComponent_iff, Submodule.topEquiv.isIsotypicOfType_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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
⊢ S' ≤ m
have have : ∀ (p : M →ₗ[R] M) (eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')), S' ≤ m
Tactic: have ⟨p, eq⟩ := extension_property _ S.subtype_injective (S'.subtype ∘ₗ e.symm)
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
⊢ S' ≤ m
have refine : S' ≤ Submodule.map p S
Tactic: refine le_trans ?_ (Submodule.map_le_iff_le_comap.mpr (le.trans (h p)))
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
⊢ S' ≤ Submodule.map p S
have rw : S' ≤ Submodule.map p S.subtype.range
Tactic: rw [← S.range_subtype, ← LinearMap.range_comp, eq, e.symm.range_comp, S'.range_subtype]
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
rw : S' ≤ Submodule.map p S.subtype.range
⊢ S' ≤ Submodule.map p S
have rw₁ : S' ≤ (p ∘ₗ S.subtype).range
Tactic: rw [← S.range_subtype, ← LinearMap.range_comp, eq, e.symm.range_comp, S'.range_subtype]
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
rw : S' ≤ Submodule.map p S.subtype.range
rw₁ : S' ≤ (p ∘ₗ S.subtype).range
⊢ S' ≤ Submodule.map p S
have rw₂ : S' ≤ (S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')).range
Tactic: rw [← S.range_subtype, ← LinearMap.range_comp, eq, e.symm.range_comp, S'.range_subtype]
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
rw : S' ≤ Submodule.map p S.subtype.range
rw₁ : S' ≤ (p ∘ₗ S.subtype).range
rw₂ : S' ≤ (S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')).range
⊢ S' ≤ Submodule.map p S
have rw₃ : S' ≤ S'.subtype.range
Tactic: rw [← S.range_subtype, ← LinearMap.range_comp, eq, e.symm.range_comp, S'.range_subtype]
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
h_1 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
h_2 : Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | Nonempty.{u + 1} (↥m ≃ₗ[R] ↥S)} S'
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')
rw : S' ≤ Submodule.map p S.subtype.range
rw₁ : S' ≤ (p ∘ₗ S.subtype).range
rw₂ : S' ≤ (S'.subtype ∘ₗ (↑e.symm : ↥S →ₗ[R] ↥S')).range
rw₃ : S' ≤ S'.subtype.range
⊢ S' ≤ Submodule.map p S
have rw₄ : S' ≤ S'
Tactic: rw [← S.range_subtype, ← LinearMap.range_comp, eq, e.symm.range_comp, S'.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S_1 : Type u_4
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : AddCommGroup S_1
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S_1
inst_9 : IsSemisimpleModule R M
m : ↥(fullyInvariantSubmodule R M)
S : Submodule R M
h :
  Membership.mem (γ := Set (Submodule R M))
    {m_1 : Submodule R M | IsSimpleModule.{u_2, u} R ↥m_1 ∧ m_1 ≤ (↑m : Submodule R M)} S
simple : IsSimpleModule.{u_2, u} R ↥S
le : S ≤ (↑m : Submodule R M)
c : (↑(isotypicComponents R M) : Type u) :=
  Subtype.mk (p := fun (x : Submodule R M) ↦ Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x)
    (isotypicComponent R M ↥S) ⋯
⊢ LE.le (α := Submodule R M) (isotypicComponent R M ↥S)
    (↑(⨆ (i : (↑(isotypicComponents R M) : Type u)),
          ⨆ (_ :
            Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
              ((fun (m : ↥(fullyInvariantSubmodule R M)) ↦
                  ({c : (↑(isotypicComponents R M) : Type u) | (↑c : Submodule R M) ≤ (↑m : Submodule R M)} :
                    Set (↑(isotypicComponents R M) : Type u)))
                m)
              i),
            Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x)
              (↑i : Submodule R M) ⋯) :
      Submodule R M)
have simp_rw : (↑c : Submodule R M) ≤
  ⨆ (i : (↑(isotypicComponents R M) : Type u)),
    ⨆ (_ :
      Membership.mem (γ := Set (↑(isotypicComponents R M) : Type u))
        {c : (↑(isotypicComponents R M) : Type u) | (↑c : Submodule R M) ≤ (↑m : Submodule R M)} i),
      (↑i : Submodule R M)
Tactic: simp_rw [← show c.1 = isotypicComponent R M S from rfl, CompleteSublattice.coe_iSup]
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
⊢ m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s
have refine_1 : ∀ (h : m.IsFullyInvariant),
  Subset (α := Set (Submodule R M))
    (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
      (Subtype.val (p := fun (x : Submodule R M) ↦
        Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
      ((OrderIso.symm OrderIso.setIsotypicComponents :
          (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))
    (isotypicComponents R M)
Tactic: refine ⟨fun h ↦ ⟨OrderIso.setIsotypicComponents.symm ⟨m, h⟩, ⟨?_, ?_⟩⟩, ?_⟩
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
refine_1 :
  ∀ (h : m.IsFullyInvariant),
    Subset (α := Set (Submodule R M))
      (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
        (Subtype.val (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
        ((OrderIso.symm OrderIso.setIsotypicComponents :
            (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))
      (isotypicComponents R M)
⊢ m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s
have refine_2 : ∀ (h : m.IsFullyInvariant),
  m =
    sSup
      (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
        (Subtype.val (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
        ((OrderIso.symm OrderIso.setIsotypicComponents :
            (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))
Tactic: refine ⟨fun h ↦ ⟨OrderIso.setIsotypicComponents.symm ⟨m, h⟩, ⟨?_, ?_⟩⟩, ?_⟩
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
refine_1 :
  ∀ (h : m.IsFullyInvariant),
    Subset (α := Set (Submodule R M))
      (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
        (Subtype.val (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
        ((OrderIso.symm OrderIso.setIsotypicComponents :
            (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))
      (isotypicComponents R M)
refine_2 :
  ∀ (h : m.IsFullyInvariant),
    m =
      sSup
        (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
          (Subtype.val (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
          ((OrderIso.symm OrderIso.setIsotypicComponents :
              (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))
⊢ m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s
have refine_3 : (∃ s ⊆ isotypicComponents R M, m = sSup s) → m.IsFullyInvariant
Tactic: refine ⟨fun h ↦ ⟨OrderIso.setIsotypicComponents.symm ⟨m, h⟩, ⟨?_, ?_⟩⟩, ?_⟩
-- 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
inst_3 : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ m =
    sSup
      (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
        (Subtype.val (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
        ((OrderIso.symm OrderIso.setIsotypicComponents :
            (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h)))
have h₁ : sSup
    (Set.image (α := { x : Submodule R M // Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x })
      (Subtype.val (p := fun (x : Submodule R M) ↦
        Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x))
      ((OrderIso.symm OrderIso.setIsotypicComponents :
          (a : ↥(fullyInvariantSubmodule R M)) → Set (↑(isotypicComponents R M) : Type u))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h))) =
  (↑(Equiv.toFun
        (RelIso.toEquiv (r := fun (x1 x2 : Set (↑(isotypicComponents R M) : Type u)) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : ↥(fullyInvariantSubmodule R M)) ↦ x1 ≤ x2) OrderIso.setIsotypicComponents)
        (Equiv.invFun
          (RelIso.toEquiv (r := fun (x1 x2 : Set (↑(isotypicComponents R M) : Type u)) ↦ x1 ≤ x2) (s :=
            fun (x1 x2 : ↥(fullyInvariantSubmodule R M)) ↦ x1 ≤ x2) OrderIso.setIsotypicComponents)
          (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := CompleteSublattice (Submodule R M)) (fullyInvariantSubmodule R M) x) m h))) :
    Submodule R M)
Tactic: convert! Subtype.ext_iff.mp (OrderIso.setIsotypicComponents.right_inv ⟨m, h⟩).symm
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ (I : Ideal R), IsAtom I].TFAE
have tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
Tactic: tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ (I : Ideal R), IsAtom I].TFAE
have tfae_2_to_3 : ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I
Tactic: tfae_have 2 → 3 := fun _ ↦ IsAtomic.exists_atom _
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
tfae_2_to_3 : ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I
h : ∃ (I : Ideal R), IsAtom I
I : Ideal R
hI : IsAtom I
⊢ IsSemisimpleRing R
have left : Nontrivial R
Tactic: have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
tfae_2_to_3 : ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I
h : ∃ (I : Ideal R), IsAtom I
I : Ideal R
hI : IsAtom I
left : Nontrivial R
⊢ IsSemisimpleRing R
have h : ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
Tactic: have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
tfae_2_to_3 : ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I
h_1 : ∃ (I : Ideal R), IsAtom I
I : Ideal R
hI : IsAtom I
left : Nontrivial R
h : ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R
have h₁ : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
Tactic: simp_rw [← isFullyInvariant_iff_isTwoSided] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.WedderburnArtin (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : IsSimpleRing R
tfae_1_to_2 : ∀ (a : IsSemisimpleRing R), IsArtinianRing R
tfae_2_to_3 : ∀ (a : IsArtinianRing R), ∃ (I : Ideal R), IsAtom I
h_1 : ∃ (I : Ideal R), IsAtom I
I : Ideal R
hI : IsAtom I
left : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R
have this : IsSimpleModule R ↥I
Tactic: have := isSimpleModule_iff_isAtom.mpr hI