awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
P : (M : Type u) → [inst_12 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M]
    [inst_15 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M_1
M : Type u
inst_8 : AddCommGroup M
inst_9 : Module R₀ M
inst_10 : Module R M
inst_11 : IsScalarTower R₀ R M
h : Module.IsTorsionBySet R M (↑Jac : Set R)
x : Module.{u_2, u} (R ⧸ Jac) M := h.module
⊢ IsSemisimpleModule R M

Tactic:
have := (h.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).2
      inferInstance
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
P : (M : Type u) → [inst_12 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M]
    [inst_15 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M_1
M : Type u
inst_8 : AddCommGroup M
inst_9 : Module R₀ M
inst_10 : Module R M
inst_11 : IsScalarTower R₀ R M
h : Module.IsTorsionBySet R M (↑Jac : Set R)
x : Module.{u_2, u} (R ⧸ Jac) M := h.module
this : IsSemisimpleModule R M
⊢ P M

Tactic:
h0 _ h
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
P : (M : Type u) → [inst_12 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M]
    [inst_15 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M_1
M : Type u
inst_8 : AddCommGroup M
inst_9 : Module R₀ M
inst_10 : Module R M
inst_11 : IsScalarTower R₀ R M
h : Module.IsTorsionBySet R M (↑Jac : Set R)
x : Module.{u_2, u} (R ⧸ Jac) M := h.module
this : IsSemisimpleModule R M
⊢ P M

Tactic:
exact h0 _ h
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
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))
n : ℕ
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
hn : Jac ^ n ≤ Module.annihilator R M
⊢ ∀ {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

Tactic:
have {M} [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] :
      Jac ≤ Module.annihilator R M → P M := by
    rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator]
    intro h
    let _ := h.module
    have := (h.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).2
      inferInstance
    exact h0 _ h
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M
⊢ LE.le (α := Ideal R) ⊤ (Module.annihilator R M)

Tactic:
rw [Jac.pow_zero, Ideal.one_eq_top] at hn

Premises used: Submodule.pow_zero, Ideal.one_eq_top
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
hn : LE.le (α := Ideal R) ⊤ (Module.annihilator R M)
⊢ P M

Tactic:
this (le_top.trans hn)

Premises used: le_top, LE.le.trans
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
hn : LE.le (α := Ideal R) ⊤ (Module.annihilator R M)
⊢ P M

Tactic:
exact this (le_top.trans hn)

Premises used: le_top, LE.le.trans
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
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 ≤ 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
hn : Jac ^ (n + 1) ≤ Module.annihilator R M
⊢ P M

Tactic:
?_
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
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))
n : ℕ
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
hn : Jac ^ n ≤ Module.annihilator R 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
succ :
  ∀ (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 ≤ Module.annihilator R M), P M)
    (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
⊢ P M

Tactic:
induction n generalizing M with
  | zero => rw [Jac.pow_zero, Ideal.one_eq_top] at hn; exact this (le_top.trans hn)
  | succ n ih => ?_

Premises used: Submodule.pow_zero, Ideal.one_eq_top
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
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 ≤ 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
hn : Jac ^ (n + 1) ≤ Module.annihilator R M
succ :
  ∀
    (ih :
      ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
        (hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M), P M)
    (hn : Jac ^ HAdd.hAdd (α := ℕ) 0 1 ≤ Module.annihilator R M), P M
succ₁ :
  ∀ (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), P M
⊢ P M

Tactic:
obtain _ | n := n
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M), P M
hn : Jac ^ HAdd.hAdd (α := ℕ) 0 1 ≤ Module.annihilator R M
⊢ Jac ≤ Module.annihilator R M

Tactic:
rw [Jac.pow_one] at hn

Premises used: Submodule.pow_one
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M), P M
hn : Jac ≤ Module.annihilator R M
⊢ P M

Tactic:
this hn
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M), P M
hn : Jac ≤ Module.annihilator R M
⊢ P M

Tactic:
exact this hn
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
⊢ P M

Tactic:
h1 _ (ih _ ?_) (ih _ ?_)
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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 : Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
succ₁ : Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R (M ⧸ HSMul.hSMul (β := Submodule R M) Jac ⊤)
⊢ P M

Tactic:
refine h1 _ (ih _ ?_) (ih _ ?_)
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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 ⊤)
succ₄ succ₅ succ₆ 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 ⊤)
⊢ 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

Premises used: Submodule.le_annihilator_iff, Submodule.pow_succ, Submodule.mul_smul, Submodule.annihilator_top
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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 : ∀ (x : M), ∀ r ∈ (↑(Jac ^ (n + 1)) : Set R), r • x ∈ HSMul.hSMul (β := Submodule R M) Jac ⊤
⊢ Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R (M ⧸ HSMul.hSMul (β := Submodule R M) Jac ⊤)

Tactic:
rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator,
      Module.isTorsionBySet_quotient_iff]

Premises used: SetLike.coe_subset_coe, Module.isTorsionBySet_quotient_iff, Module.isTorsionBySet_iff_subset_annihilator