awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
succ :
  ∀ (hn : Jac ^ (n + 1 + 1) ≤ Submodule.annihilator.{u_2, u} (M := M) ⊤),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
⊢ Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
have succ₁ : ∀ (hn : HSMul.hSMul (β := Submodule R M) (Jac ^ (n + 1 + 1)) ⊤ = ⊥),
  Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
Tactic: rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ,
      Submodule.mul_smul, ← Submodule.le_annihilator_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
succ :
  ∀ (hn : Jac ^ (n + 1 + 1) ≤ Submodule.annihilator.{u_2, u} (M := M) ⊤),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
succ₁ :
  ∀ (hn : HSMul.hSMul (β := Submodule R M) (Jac ^ (n + 1 + 1)) ⊤ = ⊥),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
⊢ Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
have succ₂ : ∀ (hn : HSMul.hSMul (β := Submodule R M) (Jac ^ (n + 1) * Jac) ⊤ = ⊥),
  Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
Tactic: rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ,
      Submodule.mul_smul, ← Submodule.le_annihilator_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
succ :
  ∀ (hn : Jac ^ (n + 1 + 1) ≤ Submodule.annihilator.{u_2, u} (M := M) ⊤),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
succ₁ :
  ∀ (hn : HSMul.hSMul (β := Submodule R M) (Jac ^ (n + 1 + 1)) ⊤ = ⊥),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
succ₂ :
  ∀ (hn : HSMul.hSMul (β := Submodule R M) (Jac ^ (n + 1) * Jac) ⊤ = ⊥),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
⊢ Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
have succ₃ : ∀ (hn : Jac ^ (n + 1) • HSMul.hSMul (β := Submodule R M) Jac ⊤ = ⊥),
  Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
Tactic: rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ,
      Submodule.mul_smul, ← Submodule.le_annihilator_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
succ :
  ∀ (hn : Jac ^ (n + 1 + 1) ≤ Submodule.annihilator.{u_2, u} (M := M) ⊤),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
succ₁ :
  ∀ (hn : HSMul.hSMul (β := Submodule R M) (Jac ^ (n + 1 + 1)) ⊤ = ⊥),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
succ₂ :
  ∀ (hn : HSMul.hSMul (β := Submodule R M) (Jac ^ (n + 1) * Jac) ⊤ = ⊥),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
succ₃ :
  ∀ (hn : Jac ^ (n + 1) • HSMul.hSMul (β := Submodule R M) Jac ⊤ = ⊥),
    Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
⊢ Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
have succ₄ : ∀ (hn : Jac ^ (n + 1) ≤ (HSMul.hSMul (β := Submodule R M) Jac ⊤).annihilator),
  Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
Tactic: rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ,
      Submodule.mul_smul, ← Submodule.le_annihilator_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
⊢ Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R (M ⧸ HSMul.hSMul (β := Submodule R M) Jac ⊤)
have succ : ∀ (x : M), ∀ r ∈ (↑(Jac ^ (n + 1)) : Set R), r • x ∈ HSMul.hSMul (β := Submodule R M) Jac ⊤
Tactic: rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator,
      Module.isTorsionBySet_quotient_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
⊢ IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M
have refine_1 : ∀ (M : Type u) (x : AddCommGroup M) (x_1 : Module R₀ M) (x_2 : Module R M),
  IsScalarTower R₀ R M →
    IsSemisimpleModule R M →
      ∀ (hJ : Module.IsTorsionBySet R M (↑(Ring.jacobson R) : Set R)) (h : IsNoetherian R M ∨ IsArtinian R M),
        Module.Finite R₀ M
Tactic: refine IsSemiprimaryRing.induction R₀ R M (P := fun M ↦ IsNoetherian R M ∨ IsArtinian R M →
    Module.Finite R₀ M) (fun M _ _ _ _ _ hJ h ↦ ?_) (fun M _ _ _ _ hs hq h ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
refine_1 :
  ∀ (M : Type u) (x : AddCommGroup M) (x_1 : Module R₀ M) (x_2 : Module R M),
    IsScalarTower R₀ R M →
      IsSemisimpleModule R M →
        ∀ (hJ : Module.IsTorsionBySet R M (↑(Ring.jacobson R) : Set R)) (h : IsNoetherian R M ∨ IsArtinian R M),
          Module.Finite R₀ M
⊢ IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M
have refine_2 : ∀ (M : Type u) (x : AddCommGroup M) (x_1 : Module R₀ M) (x_2 : Module R M) (x_3 : IsScalarTower R₀ R M)
  (hs :
    (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
        IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
      ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤))
  (hq :
    (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
        IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
      (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤))
  (h : IsNoetherian R M ∨ IsArtinian R M), Module.Finite R₀ M
Tactic: refine IsSemiprimaryRing.induction R₀ R M (P := fun M ↦ IsNoetherian R M ∨ IsArtinian R M →
    Module.Finite R₀ M) (fun M _ _ _ _ _ hJ h ↦ ?_) (fun M _ _ _ _ hs hq h ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
h_2 : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M (↑(Ring.jacobson R) : Set R)
h : IsNoetherian R M ∨ IsArtinian R M
x_3 : Module.{u_2, u} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R)) M := hJ.module
⊢ Module.Finite R₀ M
have this : [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_2, u} R ↥m].TFAE
Tactic: have := IsSemisimpleModule.finite_tfae (R := R) (M := M)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
h_2 : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M (↑(Ring.jacobson R) : Set R)
h : IsNoetherian R M ∨ IsArtinian R M
x_3 : Module.{u_2, u} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R)) M := hJ.module
this :
  [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_2, u} R ↥m].TFAE
⊢ Module.Finite R₀ M
have h₁ : Module.Finite.{u_2, u} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R)) M
Tactic: simp_rw [this.out 1 0, this.out 2 0, or_self,
      hJ.semilinearMap.finite_iff_of_bijective Function.bijective_id] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
hs :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
hq :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
⊢ Module.Finite.{u_1, u} R₀ ↥N
have refine_1 : IsNoetherian R M → IsNoetherian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
Tactic: refine hs (h.imp ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
hs :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
hq :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
refine_1 :
  IsNoetherian R M → IsNoetherian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
⊢ Module.Finite.{u_1, u} R₀ ↥N
have refine_2 : IsArtinian R M → IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
Tactic: refine hs (h.imp ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
hs :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
hq :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
⊢ Module.Finite R₀ M
have this : Module.Finite.{u_1, u} R₀ ↥N
Tactic: have : Module.Finite R₀ N := by refine hs (h.imp ?_ ?_) <;> (intro; infer_instance)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
hs :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
hq :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
this : Module.Finite.{u_1, u} R₀ ↥N
⊢ Module.Finite.{u_1, u} R₀ (M ⧸ N)
have refine_1 : IsNoetherian R M → IsNoetherian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
Tactic: refine hq (h.imp ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
hs :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
hq :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
this : Module.Finite.{u_1, u} R₀ ↥N
refine_1 :
  IsNoetherian R M → IsNoetherian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
⊢ Module.Finite.{u_1, u} R₀ (M ⧸ N)
have refine_2 : IsArtinian R M → IsArtinian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
Tactic: refine hq (h.imp ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
hs :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
hq :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
this : Module.Finite.{u_1, u} R₀ ↥N
⊢ Module.Finite R₀ M
have this₁ : Module.Finite.{u_1, u} R₀ (M ⧸ N)
Tactic: have : Module.Finite R₀ (M ⧸ N) := by refine hq (h.imp ?_ ?_) <;> (intro; infer_instance)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R : Type u_2
M_1 : Type u
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : IsSemiprimaryRing R
M : Type u
x : AddCommGroup M
x_1 x_2 : Module R M
h_1 : IsScalarTower R R M
h :
  (fun (M : Type u) [AddCommGroup M] [Module R M] [Module R M] ↦ IsNoetherian R M ↔ IsArtinian R M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h' :
  (fun (M : Type u) [AddCommGroup M] [Module R M] [Module R M] ↦ IsNoetherian R M ↔ IsArtinian R M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
N : Submodule R M := HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤
simp_rw simp_rw₁ : IsNoetherian R M ↔ IsArtinian R M
⊢ IsNoetherian R M ↔ IsArtinian R M
have simp_rw₂ : IsNoetherian.{u_2, u} R ↥N ∧ IsNoetherian.{u_2, u} R (M ⧸ N) ↔ IsArtinian R M
Tactic: simp_rw [isNoetherian_iff_submodule_quotient N, isArtinian_iff_submodule_quotient N, N, h, h']