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
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
inst_4 : Nontrivial M
h : IsIsotypic R M
⊢ ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
have have : ∀ (S : Submodule R M) (hS : IsAtom S),
  ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
Tactic: have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule R M)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
inst_4 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsAtom S
⊢ ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
have hS₁ : IsSimpleModule.{u_2, u} R ↥S
Tactic: rw [← isSimpleModule_iff_isAtom] at hS
Cleared hypotheses: hS
-- 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
inst_4 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
⊢ ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
have have : ∀ (ι : Type u) (e : Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)),
  ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] ι →₀ ↥S)
Tactic: have ⟨ι, e⟩ := (h S).linearEquiv_finsupp
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
S : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup S
inst_3 : Module R M
inst_4 : Module R S
inst_5 : IsSemisimpleModule R M
inst_6 : Module.Finite R M
h : IsIsotypicOfType R M S
⊢ ∃ (n : ℕ), Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) M (Fin n → S))
have have : ∀ (n : ℕ) (S_1 : Fin n → Submodule R M) (e : M ≃ₗ[R] Π₀ (i : Fin n), ↥(S_1 i))
  (hs : ∀ (i : Fin n), IsSimpleModule.{u_2, u} R ↥(S_1 i)),
  ∃ (n : ℕ), Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) M (Fin n → S))
Tactic: have ⟨n, S, e, hs⟩ := IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp R M
-- 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
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
⊢ ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)
have have : ∀ (S : Submodule R M) (hS : IsAtom S),
  ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)
Tactic: have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule R M)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsAtom S
⊢ ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)
have hS₁ : IsSimpleModule.{u_2, u} R ↥S
Tactic: rw [← isSimpleModule_iff_isAtom] at hS
Cleared hypotheses: hS
-- 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
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule.{u_2, u} R ↥S
⊢ ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)
have have : ∀ (n : ℕ) (e : Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)),
  ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule.{u_2, u} R ↥S ∧ Nonempty.{u + 1} (M ≃ₗ[R] Fin n → ↥S)
Tactic: have ⟨n, e⟩ := (h S).linearEquiv_fun
-- 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
have obtain : ∀ (w : Submodule R M), IsSimpleModule.{u_2, u} R ↥w → LT.lt (α := Submodule R M) ⊥ (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 : IsSemisimpleModule R S
⊢ IsSemisimpleModule.{u_2, u} R ↥(isotypicComponent R M S)
have rw : IsSemisimpleModule.{u_2, u} R
  ↥(⨆ (a : Submodule R M),
      ⨆ (_ :
        Membership.mem (γ := Set (Submodule R M))
          {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} a),
        a)
Tactic: rw [isotypicComponent, sSup_eq_iSup]
-- 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 : IsSemisimpleModule R S
⊢ IsSemisimpleModule.{u_2, u} R
    ↥(⨆ (a : Submodule R M),
        ⨆ (_ :
          Membership.mem (γ := Set (Submodule R M))
            {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} a),
          a)
have refine : ∀ (m : Submodule R M),
  Membership.mem (γ := Set (Submodule R M))
      {m : Submodule R M | Nonempty (LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S)} m →
    ∀ (e : LinearEquiv.{u_2, u_2, u, u_4} (RingHom.id R) (↥m) S), IsSemisimpleModule.{u_2, u} R ↥m
Tactic: refine isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m ⟨e⟩ ↦ ?_
-- 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
c : (↑(isotypicComponents R M) : Type u)
⊢ IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
have obtain : ∀ (S : Submodule R M) (left : IsSimpleModule.{u_2, u} R ↥S),
  IsSemisimpleModule.{u_2, u} R
    ↥(↑(Subtype.mk (p := fun (x : Submodule R M) ↦ Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) x)
            (isotypicComponent R M ↥S) sorry) :
        Submodule R M)
Tactic: obtain ⟨c, S, _, rfl⟩ := c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have this : Nontrivial.{u} ↥N
Tactic: have := IsSimpleModule.nontrivial R N
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial.{u} ↥N
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have have : ∀ (w : Submodule R M) (compl : IsCompl N w), ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
Tactic: have ⟨_, compl⟩ := exists_isCompl N
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial.{u} ↥N
w : Submodule R M
compl : IsCompl N w
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have have : ∀ (m : Submodule R M) (hm : m ∈ s) (ne : N.projectionOnto w compl ∘ₗ m.subtype ≠ 0),
  ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
Tactic: have ⟨m, hm, ne⟩ := exists_ne_zero_of_sSup_eq_top (ne_zero_of_surjective
    (projectionOnto_surjective compl)) _ hs
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
inst_4 : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial.{u} ↥N
w : Submodule R M
compl : IsCompl N w
m : Submodule R M
hm : m ∈ s
ne : N.projectionOnto w compl ∘ₗ m.subtype ≠ 0
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have have : ∀ (S : Submodule R ↥m) (e : ↥N ≃ₗ[R] ↥S), ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
Tactic: have ⟨S, ⟨e⟩⟩ := linearEquiv_of_ne_zero ne
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ sSup s
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have hN₁ : N ≤ ⨆ a ∈ s, a
Tactic: rw [sSup_eq_iSup] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have have : ∀ (e : ↥N ≃ₗ[R] ↥(inclusion hN).range), ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
Tactic: have e := LinearEquiv.ofInjective _ (inclusion_injective hN)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have this : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
Tactic: have := IsSimpleModule.congr e.symm
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have this₁ : IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)
Tactic: have := isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m hm ↦ hs ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this_1 : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
this : IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)
⊢ Eq (α := Submodule R ↥(⨆ a ∈ s, a)) (sSup (comap (Submodule.subtype (⨆ i ∈ s, i)) '' s)) ⊤
have rw : Eq.{u + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) (⨆ a ∈ s, comap (Submodule.subtype (⨆ i ∈ s, i)) a) ⊤
Tactic: rw [sSup_image, biSup_comap_subtype_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this_1 : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
this : IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)
rw : Eq.{u + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) (⨆ a ∈ s, comap (Submodule.subtype (⨆ i ∈ s, i)) a) ⊤
⊢ Eq (α := Submodule R ↥(⨆ a ∈ s, a)) (sSup (comap (Submodule.subtype (⨆ i ∈ s, i)) '' s)) ⊤
have rw₁ : Eq.{u + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) ⊤ ⊤
Tactic: rw [sSup_image, biSup_comap_subtype_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥N
s : Set (Submodule R M)
hs : ∀ (m : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑m : Submodule R M)
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this_1 : IsSimpleModule.{u_2, u} R ↥(inclusion hN).range
this : IsSemisimpleModule.{u_2, u} R ↥(⨆ i ∈ s, i)
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
have obtain : ∀ (m : Submodule R M) (hm : m ∈ s) (S : Submodule R ↥(⨆ a ∈ s, a)) (le : S ≤ comap (Submodule.subtype (⨆ i ∈ s, i)) m)
  (e' : ↥(inclusion hN).range ≃ₗ[R] ↥S), ∃ m ∈ s, ∃ S ≤ m, Nonempty.{u + 1} (↥N ≃ₗ[R] ↥S)
Tactic: obtain ⟨_, ⟨m, hm, rfl⟩, S, le, ⟨e'⟩⟩ := LinearMap.range (inclusion hN)
      |>.le_linearEquiv_of_sSup_eq_top (comap (⨆ i ∈ s, i).subtype '' s) <| by
    rw [sSup_image, biSup_comap_subtype_eq_top]
-- 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
⊢ IsIsotypic.{u, u_2} R ↥m
have obtain : ∀ (w : Submodule R M), IsSimpleModule.{u_2, u} R ↥w → IsIsotypic.{u, u_2} R ↥(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_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
inst_3 : IsSimpleModule.{u_2, u} R ↥S
le : S ≤ c
⊢ c = isotypicComponent R M ↥S
have obtain : ∀ (S' : Submodule R M),
  IsSimpleModule.{u_2, u} R ↥S' →
    ∀ (le : S ≤ isotypicComponent R M ↥S'),
      Eq (α := Submodule R M) (isotypicComponent R M ↥S') (isotypicComponent R M ↥S)
Tactic: obtain ⟨S', _, rfl⟩ := hc
Cleared hypotheses: c, hc, le
-- 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
S : Submodule R M
inst_3 : IsSimpleModule.{u_2, u} R ↥S
S' : Submodule R M
left : IsSimpleModule.{u_2, u} R ↥S'
le : S ≤ isotypicComponent R M ↥S'
⊢ Eq (α := Submodule R M) (isotypicComponent R M ↥S') (isotypicComponent R M ↥S)
have have : ∀ (e : ↥S ≃ₗ[R] ↥S'), Eq (α := Submodule R M) (isotypicComponent R M ↥S') (isotypicComponent R M ↥S)
Tactic: have ⟨e⟩ := isIsotypicOfType_submodule_iff.mp (.isotypicComponent R M S') _ le
-- 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
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
⊢ IsSemisimpleModule.{u_2, u} R ↥c
have obtain : ∀ (S : Submodule R M),
  IsSimpleModule.{u_2, u} R ↥S →
    let s : Set (Submodule R M) := isotypicComponents R M \ {isotypicComponent R M ↥S};
    ∀ (ne : ¬isotypicComponent R M ↥S ⊓ sSup s = ⊥), IsSemisimpleModule.{u_2, u} R ↥(isotypicComponent R M ↥S)
Tactic: obtain ⟨S, _, rfl⟩ := hc
Cleared hypotheses: c, hc, s, ne
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
⊢ False
have this : IsSemisimpleModule.{u_2, u} R ↥c
Tactic: have : IsSemisimpleModule R c := by obtain ⟨S, _, rfl⟩ := hc; infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this : IsSemisimpleModule.{u_2, u} R ↥c
⊢ False
have this₁ : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
Tactic: have := IsSemisimpleModule.of_injective _
      (Submodule.inclusion_injective (inf_le_left : c ⊓ sSup s ≤ c))
-- 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
c_1 : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c_1
s : Set (Submodule R M) := isotypicComponents R M \ {c_1}
ne : ¬c_1 ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c_1
this : IsSemisimpleModule.{u_2, u} R ↥(c_1 ⊓ sSup s)
c : (↑s : Type u)
⊢ IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
have obtain : ∀ (w : Submodule R M) (left : IsSimpleModule.{u_2, u} R ↥w) (right : isotypicComponent R M ↥w ∉ {c_1}),
  IsSemisimpleModule.{u_2, u} R
    ↥(↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ s) (isotypicComponent R M ↥w) sorry) : Submodule R M)
Tactic: obtain ⟨_, ⟨_, _, rfl⟩, _⟩ := c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
⊢ False
have this₁ : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
Tactic: have (c : s) : IsSemisimpleModule R c := by obtain ⟨_, ⟨_, _, rfl⟩, _⟩ := c; infer_instance
-- 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
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
⊢ False
have have : ∀ (S : Submodule R M) (le : S ≤ c ⊓ sSup s), IsSimpleModule.{u_2, u} R ↥S → False
Tactic: have ⟨S, le, _⟩ := (IsSemisimpleModule.eq_bot_or_exists_simple_le _).resolve_left ne
-- 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
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
⊢ False
have have : ∀ (c' : Submodule R M) (hc' : c' ∈ s) (S' : Submodule R M) (le' : S' ≤ c') (e : ↥S ≃ₗ[R] ↥S'), False
Tactic: have ⟨c', hc', S', le', ⟨e⟩⟩ := S.le_linearEquiv_of_le_sSup _ (le.trans inf_le_right)
-- Lean 4 proof step from Mathlib.RingTheory.SimpleModule.Isotypic (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
⊢ False
have this₁ : IsSimpleModule.{u_2, u} R ↥S'
Tactic: have := IsSimpleModule.congr 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
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this_3 : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule.{u_2, u} R ↥S'
⊢ False
have refine : Membership.mem (γ := Set (Submodule R M)) {c} c'
Tactic: refine hc'.2 ?_
-- 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
c : Submodule R M
hc : Membership.mem (γ := Set (Submodule R M)) (isotypicComponents R M) c
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this_1 : IsSemisimpleModule.{u_2, u} R ↥c
this_2 : IsSemisimpleModule.{u_2, u} R ↥(c ⊓ sSup s)
this_3 : ∀ (c : (↑s : Type u)), IsSemisimpleModule.{u_2, u} R ↥(↑c : Submodule R M)
S : Submodule R M
le : S ≤ c ⊓ sSup s
right : IsSimpleModule.{u_2, u} R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule.{u_2, u} R ↥S'
⊢ Membership.mem (γ := Set (Submodule R M)) {c} c'
have rw : Membership.mem (γ := Set (Submodule R M)) {isotypicComponent R M ↥S} (isotypicComponent R M ↥S')
Tactic: rw [eq_isotypicComponent_of_le hc (le.trans inf_le_left), eq_isotypicComponent_of_le hc'.1 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
| map f S
have rw : (f ∘ₗ S.subtype).range
Tactic: rw [← S.range_subtype, ← LinearMap.range_comp]
-- 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
⊢ map f S ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
have conv_lhs : (f ∘ₗ S.subtype).range ≤ isotypicComponent.{u_3, u_2, u} R N ↥S
Tactic: conv_lhs => rw [← S.range_subtype, ← LinearMap.range_comp]