awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∀ (x : M), ∀ r ∈ (↑(Jac ^ (n + 1)) : Set R), r • x ∈ HSMul.hSMul (β := Submodule R M) Jac ⊤

Tactic:
fun m i hi ↦ Submodule.smul_mem_smul (Ideal.pow_le_self n.succ_ne_zero hi) trivial

Premises used: trivial, Set.Mem, Ideal.pow_le_self, Nat.succ_ne_zero, Submodule.smul_mem_smul
-- 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
⊢ ∀ (x : M), ∀ r ∈ (↑(Jac ^ (n + 1)) : Set R), r • x ∈ HSMul.hSMul (β := Submodule R M) Jac ⊤

Tactic:
exact fun m i hi ↦ Submodule.smul_mem_smul (Ideal.pow_le_self n.succ_ne_zero hi) trivial
-- 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
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

Tactic:
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 ↦ ?_)

Premises used: IsSemiprimaryRing.induction
-- 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
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
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
⊢ 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 ↦ ?_)

Premises used: IsSemiprimaryRing.induction
-- 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
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, 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)
-- 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
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.{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

Premises used: Function.bijective_id, Module.IsTorsionBySet.semilinearMap, List.TFAE.out, or_self, LinearMap.finite_iff_of_bijective, OfNat.ofNat
-- 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
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)
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
h : Module.Finite.{u_2, u} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R)) M
⊢ Module.Finite R₀ M

Tactic:
.trans (R ⧸ Ring.jacobson R) M

Premises used: HasQuotient.Quotient, Module.Finite.trans, Ring.jacobson
-- 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
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)
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
h : Module.Finite.{u_2, u} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R)) M
⊢ Module.Finite R₀ M

Tactic:
exact .trans (R ⧸ Ring.jacobson R) M
-- 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
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

Tactic:
hs (h.imp ?_ ?_)

Premises used: iInf, Set.Mem, iSup, Set.iInter, Submodule.restrictScalars, setOf, Or.imp
-- 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
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) ⊤)
refine_2 : IsArtinian R M → IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
⊢ Module.Finite.{u_1, u} R₀ ↥N

Tactic:
refine hs (h.imp ?_ ?_)

Premises used: Or.imp
-- 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
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) ⊤)
h_2 : IsNoetherian R M
⊢ IsNoetherian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)

Tactic:
infer_instance
-- 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
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) ⊤)
h_2 : IsArtinian R M
⊢ IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)

Tactic:
infer_instance
-- 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
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

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

Tactic:
hq (h.imp ?_ ?_)

Premises used: iInf, iSup, Set.iInter, Submodule.restrictScalars, setOf, Submodule.quotientRel, Or.imp
-- 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
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) ⊤)
refine_2 :
  IsArtinian R M → IsArtinian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
⊢ Module.Finite.{u_1, u} R₀ (M ⧸ N)

Tactic:
refine hq (h.imp ?_ ?_)

Premises used: Or.imp
-- 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
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
h_2 : IsNoetherian R M
⊢ IsNoetherian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)

Tactic:
infer_instance
-- 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
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
h_2 : IsArtinian R M
⊢ IsArtinian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)

Tactic:
infer_instance
-- 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
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)

Tactic:
have : Module.Finite R₀ (M ⧸ N) := by refine hq (h.imp ?_ ?_) <;> (intro; infer_instance)
-- 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
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_1 : Module.Finite.{u_1, u} R₀ ↥N
this : Module.Finite.{u_1, u} R₀ (M ⧸ N)
⊢ Module.Finite R₀ M

Tactic:
.of_submodule_quotient N

Premises used: Module.Finite.of_submodule_quotient