-- Mathlib/RingTheory/HopkinsLevitzki.lean
theorem induction
    {P : ∀ (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M], Prop}
    (h0 : ∀ (M) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M]
      [IsSemisimpleModule R M], Module.IsTorsionBySet R M (Ring.jacobson R) → P M)
    (h1 : ∀ (M) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M],
      let N := Ring.jacobson R • (⊤ : Submodule R M); P N → P (M ⧸ N) → P M) :
    P M

Proof state:
R₀ : Type u_1
R : Type u_2
M : Type u
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R₀ M
inst✝² : Module R M
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M]
    [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑(Ring.jacobson R) → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Ring.jacobson R • ⊤;
    P ↥N → P (M ⧸ N) → P M
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
hn : Ring.jacobson R ^ n = 0
⊢ P M

Tactic:
set Jac := Ring.jacobson R

Result:
R₀ : Type u_1
R : Type u_2
M : Type u
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R₀ M
inst✝² : Module R M
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M]
    [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n = 0
⊢ P M

Proof state:
case succ.succ.refine_1
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M]
    [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    Jac ^ (n + 1) ≤ Module.annihilator R M → P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
⊢ Jac ^ (n + 1) ≤ Module.annihilator R ↥(Jac • ⊤)

Tactic:
rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ,
  Submodule.mul_smul, ← Submodule.le_annihilator_iff] at hn

Result:
no goals

Proof state:
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝¹¹ : Ring R₀
inst✝¹⁰ : Ring R
inst✝⁹ : Module R₀ R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R₀ M✝
inst✝⁶ : Module R M✝
inst✝⁵ : IsScalarTower R₀ R M✝
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M]
    [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
h : Module.IsTorsionBySet R M ↑Jac
x✝ : Module (R ⧸ Jac) M := h.module
this : IsSemisimpleModule R M
⊢ P M

Tactic:
exact h0 _ h

Result:
no goals

Proof state:
R₀ : Type u_1
R : Type u_2
M : Type u
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R₀ M
inst✝² : Module R M
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M]
    [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ 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

Result:
R₀ : Type u_1
R : Type u_2
M : Type u
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R₀ M
inst✝² : Module R M
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M]
    [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
⊢ P M