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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (valuation K v) ↑1 = ↑1

Tactic:
exact map_one _

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' (r * ↑(t * s) - ↑t * r * ↑s) (s * (t * s)) = 0

Tactic:
Submonoid.coe_mul

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' (r * (↑t * ↑s) - ↑t * r * ↑s) (s * (t * s)) = 0
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v' i' : R
vi✝ : (algebraMap R K) v' * (algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : (algebraMap R K) i' * (algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  (powMonoidHom n) { val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  (algebraMap R K) (v' ^ n) = (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := (algebraMap R K) i', inv := (algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ (powMonoidHom n) { val := v', inv := i', val_inv := vi, inv_val := iv } =
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }

Tactic:
by
      simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
         FaithfulSMul.algebraMap_injective R K hv

Goal state after:
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
⊢ False

Tactic:
have ntr : Nontrivial Nₚ' :=
      Submodule.Quotient.nontrivial_iff.mpr <| .symm <|
        Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator <|
          IsLocalRing.maximalIdeal_le_jacobson _

Goal state after:
case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
⊢ False
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
⊢ (if x✝¹ * 0 = 0 ∧ n = 0 then 1 else 0) = x✝¹ ^ n * if 0 = 0 ∧ n = 0 then 1 else 0

Tactic:
simp only [mul_zero, true_and, mul_ite, mul_one]

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
⊢ (if n = 0 then 1 else 0) = if n = 0 then x✝¹ ^ n else 0
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsWeaklyRegular M (r :: rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r :: rs = []

Tactic:
isWeaklyRegular_cons_iff

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r :: rs = []
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
have hxmk : x ^ (m + k) = 0 := Ideal.pow_eq_zero_of_mem hnI hkm hx
    rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

Tactic:
by_cases! hmk : m * k < n

Goal state after:
case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : m * k < n
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : ↑n ! = ↑n ! • 1
this : (↑n !)⁻¹ * ↑n ! = 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1

Tactic:
this,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : ↑n ! = ↑n ! • 1
this : (↑n !)⁻¹ * ↑n ! = 1
⊢ 1 = 1 • 1
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ y ∈ ↑I

Tactic:
exact hxy ▸ hI.dpow_mem hn (hS hx)

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I

Tactic:
by
  rw [span_le]
  rintro y ⟨n, hn, x, hx, hxy⟩
  exact hxy ▸ hI.dpow_mem hn (hS hx)

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
f : R →ₐ[k] k
x✝ : R
this : (RingHom.ker f).IsPrime
⊢ (Ideal.Quotient.mk (RingHom.ker f)) x✝ = (algebraMap k (R ⧸ RingHom.ker f)) (f x✝)

Tactic:
IsScalarTower.algebraMap_apply k R

Goal state after:
k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
f : R →ₐ[k] k
x✝ : R
this : (RingHom.ker f).IsPrime
⊢ (Ideal.Quotient.mk (RingHom.ker f)) x✝ = (algebraMap R (R ⧸ RingHom.ker f)) ((algebraMap k R) (f x✝))
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝³ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝² : IsScalarTower S (S × U) U
this✝¹ : Etale S U
this✝ : Module.Finite S U
this : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
p : PrimeSpectrum S
⊢ Module.rankAtStalk U p = ↑n p

Tactic:
simp only [Pi.natCast_def, Nat.cast_id]

Goal state after:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝³ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝² : IsScalarTower S (S × U) U
this✝¹ : Etale S U
this✝ : Module.Finite S U
this : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
p : PrimeSpectrum S
⊢ Module.rankAtStalk U p = n
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
k : ℕ
N₁ N₂ : G(k, M; R)
h : N₁.toSubmodule = N₂.toSubmodule
⊢ N₁ = N₂

Tactic:
cases N₁; cases N₂; congr 1

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
this,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (x : Fin (Nat.succ 0).succ →₀ ℕ),
    x ≠ single 1 1 → (coeff x) F.toPowerSeries • (coeff (single () 1)) (x.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

Tactic:
intro d hd
    by_cases hd₁ : d 0 = 0
    · by_cases hd₀ : d 1 = 0
      · simp [hd₀, hd₁]
      simp [hd₁, PowerSeries.coeff_X_pow]
      grind
    simp [hd₁]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
have h :=
      SummableFamily.one_sub_self_mul_hsum_powers
        (unit_aux x (inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr x0)) _ (neg_add_cancel x.order))
    rw [sub_sub_cancel] at h
    rw [inv_def, ← mul_assoc, mul_comm x, h]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
⊢ Polynomial.eval (c 0) f ∈ I ^ (0 + 1)

Tactic:
simpa only [Nat.rec_zero, zero_add, pow_one] using! h₁

Goal state after:
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.head.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (l.cons q lt).head.asIdeal
⊢ ∃ L,
    L.length = (l.cons q lt).length ∧
      RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = (l.cons q lt).toList

Tactic:
simp only [RelSeries.head_cons] at lo
    obtain ⟨Q, PQlt, hQ, Qlo⟩ :=
      Ideal.exists_ideal_gt_liesOver_of_lt P lt
    obtain ⟨L, len, head, spec⟩ := ih Q
    refine ⟨L.cons ⟨P, inferInstance⟩ (by
      simp_all only [Set.mem_ofPred_eq]
      exact PQlt), by simpa using len, rfl, ?_⟩
    simpa [spec, PrimeSpectrum.ext_iff] using lo.over.symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ ↑q.height = ↑0

Tactic:
← IsLocalization.AtPrime.ringKrullDim_eq_height q (Localization.AtPrime q),

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ ringKrullDim (Localization.AtPrime q) = ↑0
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsNoetherianRing R
x : R
hx : Prime x
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
⊢ UniqueFactorizationMonoid R ↔ UniqueFactorizationMonoid S

Tactic:
by
  have : IsDomain S := IsLocalization.Away.isDomain S hx.ne_zero
  refine ⟨fun _ ↦ of_isLocalization (Submonoid.powers x) S, fun _ ↦ ?_⟩
  rw [iff_forall_isPrincipal_of_height_eq_one]
  intro p hp h1
  by_cases hxp : x ∈ p
  · exact ⟨x, p.eq_span_singleton_of_height_eq_one h1 hxp hx⟩
  · have hd := by rwa [← Ideal.disjoint_powers_iff_notMem_of_isPrime x] at hxp
    have := IsLocalization.isPrime_of_isPrime_disjoint (Submonoid.powers x) S p hp hd
    refine p.isPrincipal_of_isPrincipal_isLocalizationAway_of_prime hx hxp S
      (isPrincipal_of_height_eq_one ?_)
    rw [← IsLocalization.height_under (Submonoid.powers x),
      IsLocalization.under_map_of_isPrime_disjoint (Submonoid.powers x) S hp hd, h1]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsLocalRing R
dim : Module.supportDim R N = 0
⊢ Module.support R N = PrimeSpectrum.zeroLocus ↑(maximalIdeal R)

Tactic:
by
  let _ : Nontrivial N := by simp [← Module.supportDim_ne_bot_iff_nontrivial R, dim]
  rw [PrimeSpectrum.zeroLocus_eq_singleton]
  apply le_antisymm
  · intro p hp
    by_contra nmem
    push _ ∈ _ at nmem
    have : p < ⟨maximalIdeal R, IsMaximal.isPrime' (maximalIdeal R)⟩ :=
      lt_of_le_of_ne (IsLocalRing.le_maximalIdeal IsPrime.ne_top') nmem
    have : Module.supportDim R N > 0 := by
      simp only [Module.supportDim, gt_iff_lt, Order.krullDim_pos_iff, Subtype.exists,
        Subtype.mk_lt_mk, exists_prop]
      use p
      simpa [hp] using! ⟨_, IsLocalRing.closedPoint_mem_support R N, this⟩
    exact (ne_of_lt this) dim.symm
  · simpa using! IsLocalRing.closedPoint_mem_support R N

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
⊢ span ↑t = map (algebraMap R S) (span ↑s) ⊔ span ↑o

Tactic:
simp [t, Ideal.map_span]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
⊢ supportDim R (QuotSMulTop x M) + 1 ≤ supportDim R M

Tactic:
by
  nontriviality M
  nontriviality (QuotSMulTop x M)
  have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype
  have : Nonempty (Module.support R (QuotSMulTop x M)) := nonempty_support_of_nontrivial.to_subtype
  simp only [supportDim, Order.krullDim_eq_iSup_length]
  apply WithBot.coe_le_coe.mpr
  simp only [ENat.iSup_add, iSup_le_iff]
  intro p
  have hp := p.head.2
  simp only [support_quotSMulTop, Set.mem_inter_iff, mem_zeroLocus, Set.singleton_subset_iff] at hp
  have le : support R (QuotSMulTop x M) ⊆ support R M := by simp
  -- Since `Supp(M/xM) ⊆ Supp M`, `p` can be viewed as a chain of prime ideals in `Supp M`,
  -- which we denote by `q`.
  let q : LTSeries (support R M) :=
    p.map (Set.MapsTo.restrict id (support R (QuotSMulTop x M)) (support R M) le) (fun _ _ h ↦ h)
  obtain ⟨r, hrm, hr⟩ := exists_minimalPrimes_le (mem_support_iff_of_finite.mp q.head.2)
  let r : support R M := ⟨⟨r, hrm.isPrime⟩, mem_support_iff_of_finite.mpr hrm.1.2⟩
  have hr : r < q.head := lt_of_le_of_ne hr (fun h ↦ hn q.head.1.1 (by rwa [← h]) hp.2)
  exact le_of_eq_of_le (by simp [q]) (le_iSup _ (q.cons r hr))

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
hx : x ∈ maximalIdeal R
⊢ supportDim R R ≤ supportDim R (R ⧸ x • ⊤) + 1

Tactic:
exact supportDim_le_supportDim_quotSMulTop_succ hx

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ f.coeff n = 0

Tactic:
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (neg_le_iff_add_nonneg.mp (hs ▸ h_n_ord))

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
⊢ f.coeff n = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
⊢ f.coeff n = 0

Tactic:
obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D + s) (by lia)

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ f.coeff n = 0
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ IsLocalization.IsInteger ℤ q ↔ q ∈ Set.range Int.cast

Tactic:
by
  simp [IsLocalization.IsInteger]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
⊢ Valued.v f ≤ exp (-D)

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat <| neg_nonpos_of_nonneg ord_nonpos.le

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ Valued.v f ≤ exp (-D)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := mem_prod_iff.mp <| Filter.le_def.mp hℱ.2 entourage
    <| (Valued.hasBasis_uniformity K⸨X⸩ ℤᵐ⁰).mem_of_mem (i := ζ) (by tauto)

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case zero
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
⊢ leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) 0 r) = r

Tactic:
esymmAlgHom_zero,

Goal state after:
case zero
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
⊢ leadingCoeff (⇑toLex) (C r) = r