mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ ↑t
x : M
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ ∀ b ∈ {x_1 ∈ t | x ∉ x_1}.erase q, (q.colon Set.univ).radical ≤ (b.colon Set.univ).radical

Tactic:
]

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ ↑t
x : M
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ ∀ b ∈ {x_1 ∈ t | x ∉ x_1}.erase q, (q.colon Set.univ).radical ≤ (b.colon Set.univ).radical
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ False

Tactic:
]

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ False
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
x : M
hp : ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical).IsPrime
⊢ ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical) ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t

Tactic:
]

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
x : M
hp : ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical).IsPrime
⊢ ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical) ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
q : Submodule R M
hq : q ∈ t
⊢ (q.colon Set.univ).radical ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
q : Submodule R M
hq : q ∈ t
⊢ (q.colon Set.univ).radical ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
hb : b ∈ q
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
⊢ x ∈ q

Tactic:
]

Goal state after:
case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
hb : b ∈ q
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
⊢ x ∈ q
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
c : ↥S
hc : c • b = c • a • x
hb : (c * a) • x ∈ q
⊢ x ∈ q

Tactic:
]

Goal state after:
case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
c : ↥S
hc : c • b = c • a • x
hb : (c * a) • x ∈ q
⊢ x ∈ q
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : ↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
r : ↑N.associatedPrimes
hrs : r ∈ s₀
h : ↑p ≤ ↑r
⊢ p ∈ s₀

Tactic:
]

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : ↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
r : ↑N.associatedPrimes
hrs : r ∈ s₀
h : ↑p ≤ ↑r
⊢ p ∈ s₀
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case refine_3
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
r : ↥Z
x✝ : r • x ∈ ⊤
s : ↥Z
⊢ (r * s) • (x * x) = (r * s) • (x * x)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case neg
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
⊢ (mkLinearMap S M).range ≤ localized₀ S (mkLinearMap S M) q

Tactic:
]

Goal state after:
case neg
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
⊢ (mkLinearMap S M).range ≤ localized₀ S (mkLinearMap S M) q
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
⊢ eval (↑q) Φₙ ∣ ∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, ↑x.carrier.toFinset.card

Tactic:
]

Goal state after:
case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
⊢ eval (↑q) Φₙ ∣ ∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, ↑x.carrier.toFinset.card
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) ((⇑(localized₀FrameHom S (mkLinearMap S M)) ∘ id) i)) = ⨅ q ∈ s, q

Tactic:
]

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) ((⇑(localized₀FrameHom S (mkLinearMap S M)) ∘ id) i)) = ⨅ q ∈ s, q
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
⊢ eval (↑q) Φₙ ∣ ↑((q ^ n - 1) / card (↥Zx)ˣ)

Tactic:
]

Goal state after:
case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
⊢ eval (↑q) Φₙ ∣ ↑((q ^ n - 1) / card (↥Zx)ˣ)
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
this : ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤
⊢ ⨅ a ∈ s, a = ⨅ q ∈ s, q

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝¹ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝ : Field ↥Zx := hD.field ⋯
this : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
⊢ 1 ≤ card ↥Zx

Tactic:
]

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝¹ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝ : Field ↥Zx := hD.field ⋯
this : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
⊢ 1 ≤ card ↥Zx
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ t.inf radical ≤ p.radical

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ t.inf radical ≤ p.radical
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ t.inf radical ≤ t.inf (⇑radicalInfTopHom ∘ id)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ t.inf radical ≤ t.inf (⇑radicalInfTopHom ∘ id)
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
⊢ eval (↑q) Φₙ ∣ ↑((q ^ n - 1) / (q ^ d - 1))

Tactic:
]

Goal state after:
case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
⊢ eval (↑q) Φₙ ∣ ↑((q ^ n - 1) / (q ^ d - 1))
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
⊢ N ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ N → x ∈ N ∨ ∃ n, r ^ n • ⊤ ≤ N

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
⊢ N ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ N → x ∈ N ∨ ∃ n, r ^ n • ⊤ ≤ N
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ eval (↑q) ((X ^ d - 1) * Φₙ) ∣ eval (↑q) (X ^ n - 1)

Tactic:
]

Goal state after:
case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ eval (↑q) ((X ^ d - 1) * Φₙ) ∣ eval (↑q) (X ^ n - 1)
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)
⊢ x + a ^ n • y ∈ N

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)
⊢ x + a ^ n • y ∈ N
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ card ↥Zx < card D

Tactic:
]

Goal state after:
case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ card ↥Zx < card D
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)
⊢ a ^ n • (x + a ^ n • y) ∈ N

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)
⊢ a ^ n • (x + a ^ n • y) ∈ N