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

Goal state before:
pp: case succ.refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
⊢ (Submodule.map (↑R φ.toLinearMap) ⊤).FG

Tactic:
simpa using

Goal state after:
case succ.refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
⊢ ⊤.FG
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case succ.refine_1
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
c₁' : S ⧸ P ^ i.succ
hc₁' : c₁' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
c₂' : S ⧸ P ^ i.succ
hc₂' : c₂' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
h : (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₁', hc₁'⟩ = (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₂', hc₂'⟩
⊢ f (k c₁' hc₁') ⋯ - f (k c₂' hc₂') ⋯ ∈ P

Tactic:
simpa using

Goal state after:
case succ.refine_1
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
c₁' : S ⧸ P ^ i.succ
hc₁' : c₁' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
c₂' : S ⧸ P ^ i.succ
hc₂' : c₂' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
h : (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₁', hc₁'⟩ = (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₂', hc₂'⟩
⊢ f (k c₁' hc₁') ⋯ - f (k c₂' hc₂') ⋯ ∈ P
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ I • Submodule.map (Submodule.subtype (I ^ n)) ⊤ ≤
    (Submodule.subtype (I ^ n)).range ⊓ (Submodule.mkQ (I ^ (n + 1))).ker

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ I * I ^ n ≤ I ^ n
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
⊢ (algebraMap R (Localization p.primeCompl)) r = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
⊢ (algebraMap R (Localization p.primeCompl)) r = 1
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case e'_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
ψ : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1) := ⋯
e_3✝ : inst✝⁵.toSemiring = CommRing.toCommSemiring.toSemiring
e_4✝ : (Submodule.Quotient.addCommGroup (I ^ (n + 1))).toAddCommMonoid = Submodule.Quotient.addCommMonoid (I ^ (n + 1))
e_5✝ : Submodule.Quotient.module' (I ^ (n + 1)) ≍ Submodule.Quotient.module' (I ^ (n + 1))
⊢ Submodule.comap (Submodule.mkQ (I ^ (n + 1))) φ.toLinearMap.ker =
    Submodule.comap (Submodule.mkQ (I ^ (n + 1))) (Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n))

Tactic:
simpa using

Goal state after:
case e'_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
ψ : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1) :=
  (I • ⊤).liftQ (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n)) ⋯ ∘ₗ ↑(quotTensorEquivQuotSMul (↥(I ^ n)) I)
e_3✝ : inst✝⁵.toSemiring = CommRing.toCommSemiring.toSemiring
e_4✝ : (Submodule.Quotient.addCommGroup (I ^ (n + 1))).toAddCommMonoid = Submodule.Quotient.addCommMonoid (I ^ (n + 1))
e_5✝ : Submodule.Quotient.module' (I ^ (n + 1)) ≍ Submodule.Quotient.module' (I ^ (n + 1))
⊢ I ^ (n + 1) ≤ I ^ n
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
⊢ (algebraMap R (Localization.AtPrime q)) r = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
⊢ (algebraMap R (Localization.AtPrime q)) r = 0
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Irreducible (absNorm I)
h : IsUnit I
⊢ IsUnit (absNorm I)

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Irreducible (absNorm I)
h : IsUnit I
⊢ I = ⊤
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
a b : Ideal S
hI : Irreducible (absNorm (a * b))
⊢ IsUnit a ∨ IsUnit b

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
a b : Ideal S
hI : Irreducible (absNorm (a * b))
⊢ a = ⊤ ∨ b = ⊤
Module: Mathlib.RingTheory.Jacobson.Artinian

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
this : IsNoetherianRing A
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A

Tactic:
finite_iff_isArtinianRing,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
this : IsNoetherianRing A
⊢ IsArtinianRing A ↔ Ring.KrullDimLE 0 A
Module: Mathlib.RingTheory.Jacobson.Artinian

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
this : IsNoetherianRing A
⊢ IsArtinianRing A ↔ Ring.KrullDimLE 0 A

Tactic:
isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
this : IsNoetherianRing A
⊢ IsNoetherianRing A ∧ Ring.KrullDimLE 0 A ↔ Ring.KrullDimLE 0 A
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
I : Ideal S
hI : p ∣ ↑(absNorm I)
this✝ : IsAddTorsionFree S
this : CharZero S
⊢ span {p} ≠ ⊥

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
I : Ideal S
hI : p ∣ ↑(absNorm I)
this✝ : IsAddTorsionFree S
this : CharZero S
⊢ ¬p = 0
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
I : Ideal S
hI' : IsUnit I
hI : p ∣ ↑(absNorm I)
⊢ I = ⊤

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
I : Ideal S
hI' : IsUnit I
hI : p ∣ ↑(absNorm I)
⊢ I = ⊤
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
hI' : IsUnit ⊤
hI : p ∣ ↑(absNorm ⊤)
⊢ p ∣ 1

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
hI' : IsUnit ⊤
hI : p ∣ ↑(absNorm ⊤)
⊢ p ∣ 1
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S.leftInv.leftInv = S

Tactic:
refine le_antisymm S.leftInv_leftInv_le ?_
  intro x hx
  have : x = ((hS hx).unit⁻¹⁻¹ : Mˣ) := by
    rw [inv_inv (hS hx).unit]
    rfl
  rw [this]
  exact S.leftInv.unit_mem_leftInv _ (S.unit_mem_leftInv _ hx)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm P)
this : P.IsMaximal
⊢ under ℤ P ≠ ⊤

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm P)
this : P.IsMaximal
⊢ ¬P = ⊤
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
⊢ ↑((S.leftInvEquiv hS) x) * ↑x = 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
⊢ ↑(S.fromLeftInv x) * ↑x = 1
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ ↑x * ↑((S.leftInvEquiv hS).symm x) = 1

Tactic:
convert! S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ x = (S.leftInvEquiv hS) ((S.leftInvEquiv hS).symm x)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp✝ : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
h : m = 0
⊢ IsUnit p

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp✝ : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
h : m = 0
⊢ IsUnit p
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ ((Algebra.norm ℤ) ↑n).natAbs ≠ 0

Tactic:
simpa using

Goal state after:
case inr.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ ¬n = 0
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
⊢ closure[inst✝¹] (closedPoints X) = Set.univ

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
⊢ closure[inst✝¹] (closedPoints X) = Set.univ
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm I ≤ n}.Finite

Tactic:
show {I : Ideal S | Ideal.absNorm I ≤ n} =
    (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | Ideal.absNorm I = i}) by ext; simp

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ (⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}).Finite
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
x : X
hx : x ∈ S ∩ closedPoints X
⊢ f x ∈ closedPoints Y

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
x : X
hx : x ∈ S ∩ closedPoints X
⊢ IsClosed[inst✝¹] {f x}
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsArtinianRing R ↔ Ring.KrullDimLE 0 R

Tactic:
isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing R ∧ Ring.KrullDimLE 0 R ↔ Ring.KrullDimLE 0 R
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos.succ
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
i : Fin s.length
hi : length A ↥(s.toFun i.castSucc) = ↑↑i.castSucc * length (ResidueField A) (ResidueField B)
⊢ length A ↥(s.toFun i.succ) = ↑↑i.succ * length (ResidueField A) (ResidueField B)

Tactic:
simpa using

Goal state after:
case pos.succ
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
i : Fin s.length
hi : length A ↥(s.toFun i.castSucc) = ↑↑i.castSucc * length (ResidueField A) (ResidueField B)
⊢ length A ↥(s.toFun i.succ) = ↑↑i * length (ResidueField A) (ResidueField B) + length (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
⊢ length (ResidueField A) (ResidueField B) ≠ 0

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
⊢ ¬length (ResidueField A) (ResidueField B) = 0
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
q : Ideal S
inst✝⁶ : Module.Finite R S
inst✝⁵ : q.IsPrime
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ R
inst✝¹ : Module.Free ℤ S
inst✝ : q.LiesOver ⊥
⊢ absNorm ⊥ ^ q.inertiaDeg R = absNorm q

Tactic:
simpa using

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
q : Ideal S
inst✝⁶ : Module.Finite R S
inst✝⁵ : q.IsPrime
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ R
inst✝¹ : Module.Free ℤ S
inst✝ : q.LiesOver ⊥
⊢ ¬⊥.inertiaDeg R = 0
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
inst✝³ : Module.Free ℤ R
inst✝² : Module.Finite ℤ R
p : ℤ
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver (span {p})
⊢ p.natAbs ^ P.inertiaDeg ℤ = absNorm P

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
inst✝³ : Module.Free ℤ R
inst✝² : Module.Finite ℤ R
p : ℤ
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver (span {p})
⊢ p.natAbs ^ P.inertiaDeg ℤ = absNorm P
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
h : ¬map f p ≤ P
⊢ ¬map f p ≤ P ^ (0 + 1)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
h : ¬map f p ≤ P
⊢ ¬map f p ≤ P
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos.succ
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
i : Fin s.length
hi :
  length B ↥(Submodule.baseChange B (s.toFun i.castSucc)) =
    ↑↑i.castSucc * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B ↥(Submodule.baseChange B (s.toFun i.succ)) =
    ↑↑i.succ * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
simpa using

Goal state after:
case pos.succ
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
i : Fin s.length
hi :
  length B ↥(Submodule.baseChange B (s.toFun i.castSucc)) =
    ↑↑i.castSucc * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B ↥(Submodule.baseChange B (s.toFun i.succ)) =
    ↑↑i * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A)) +
      length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
⊢ length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A)) ≠ 0

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
⊢ ¬Ideal.map (algebraMap A B) (maximalIdeal A) = ⊤