-- Mathlib/RingTheory/HopkinsLevitzki.lean
theorem finite_of_isNoetherian_or_isArtinian :
    IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M

Proof state:
case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(Ring.jacobson R • ⊤)
hq :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this : Module.Finite R₀ ↥N
⊢ Module.Finite R₀ M

Tactic:
have : Module.Finite R₀ (M ⧸ N) := by refine hq (h.imp ?_ ?_) <;> (intro; infer_instance)

Result:
case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(Ring.jacobson R • ⊤)
hq :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this✝ : Module.Finite R₀ ↥N
this : Module.Finite R₀ (M ⧸ N)
⊢ Module.Finite R₀ M

Proof state:
case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(Ring.jacobson R • ⊤)
hq :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
⊢ Module.Finite R₀ M

Tactic:
have : Module.Finite R₀ N := by refine hs (h.imp ?_ ?_) <;> (intro; infer_instance)

Result:
case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(Ring.jacobson R • ⊤)
hq :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this : Module.Finite R₀ ↥N
⊢ Module.Finite R₀ 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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(Ring.jacobson R • ⊤)
hq :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this : Module.Finite R₀ ↥N
⊢ Module.Finite R₀ (M ⧸ N)

Tactic:
refine hq (h.imp ?_ ?_) <;> (intro; infer_instance)

Result:
no goals

Proof state:
case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(Ring.jacobson R • ⊤)
hq :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
⊢ Module.Finite R₀ M

Tactic:
let N := (Ring.jacobson R • ⊤ : Submodule R M).restrictScalars R₀

Result:
case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(Ring.jacobson R • ⊤)
hq :
  (fun M [AddCommGroup M] [Module R₀ M] [Module R M] => IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
⊢ Module.Finite R₀ M