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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 - 0 ∈ I ^ n

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 - 0 ∈ I ^ n
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < max (v x) (v y)
this : ∀ {x y : R}, v x ≠ v y → v (x + y) < max (v x) (v y) → v y < v x → False
vyx : ¬v y < v x
⊢ v (x + y) < max (v x) (v y)

Tactic:
]

Goal state after:
case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < max (v x) (v y)
this : ∀ {x y : R}, v x ≠ v y → v (x + y) < max (v x) (v y) → v y < v x → False
vyx : ¬v y < v x
⊢ v (x + y) < max (v x) (v y)
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
this : sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ Ideal.comap (algebraMap R S) P'
⊢ ⨅ I ∈ Ideal.comap (algebraMap R S) '' {J | P' ≤ J ∧ J.IsMaximal}, I ≤
    ⨅ a ∈ {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}, a

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
this : sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ Ideal.comap (algebraMap R S) P'
⊢ ⨅ I ∈ Ideal.comap (algebraMap R S) '' {J | P' ≤ J ∧ J.IsMaximal}, I ≤
    ⨅ a ∈ {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}, a
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x
vyx : v y < v x
⊢ False

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x
vyx : v y < v x
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ ¬s = ⊥

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ ¬s = ⊥
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (y + x) = v x

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (y + x) = v x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
this : span {generator s} = s
⊢ Associated (generator s) (generator s * ↑u)

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
this : span {generator s} = s
⊢ Associated (generator s) (generator s * ↑u)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v y = v y

pp: case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v x < v (-y)

Tactic:
]

Goal state after:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v x < v (-y)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v x < v y

Tactic:
]

Goal state after:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v x < v y
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ x ^ (n✝ + 1) * y ^ (n✝ + 1) ∈ I ^ (n✝ + 1)

Tactic:
]

Goal state after:
case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ x ^ (n✝ + 1) * y ^ (n✝ + 1) ∈ I ^ (n✝ + 1)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ ∃ u, p ^ m * ↑u = q ^ n

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ ∃ u, p ^ m * ↑u = q ^ n
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr
R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
h0 : v (f j) ≠ 0
⊢ v (f j + ∑ x ∈ s \ {j}, f x) = v (f j)

Tactic:
]

Goal state after:
case inr
R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
h0 : v (f j) ≠ 0
⊢ v (f j + ∑ x ∈ s \ {j}, f x) = v (f j)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v x = v x

pp: case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (-y) < v x

Tactic:
]

Goal state after:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (-y) < v x
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
I J : Ideal R
inst✝ : I.IsPrime
⊢ J ≤ I ↔ J ≤ I

pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
I J : Ideal R
inst✝ : I.IsPrime
⊢ I.IsPrime

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
I J : Ideal R
inst✝ : I.IsPrime
⊢ I.IsPrime
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ringKrullDim R ≤ 0 → 0 ≤ ringKrullDim R

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ringKrullDim R ≤ 0 → 0 ≤ ringKrullDim R
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ (∀ I_1 ∈ minimalPrimes (R ⧸ I), I_1.IsMaximal) ↔
    ∀ ⦃x : Ideal (R ⧸ I)⦄, x ∈ minimalPrimes (R ⧸ I) → (comap (Quotient.mk I) x).IsMaximal

Tactic:
]

Goal state after:
R : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ (∀ I_1 ∈ minimalPrimes (R ⧸ I), I_1.IsMaximal) ↔
    ∀ ⦃x : Ideal (R ⧸ I)⦄, x ∈ minimalPrimes (R ⧸ I) → (comap (Quotient.mk I) x).IsMaximal
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ q ^ n = q ^ n

Tactic:
]

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

Goal state before:
pp: case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v y < v x

Tactic:
]

Goal state after:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v y < v x
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: case refine_2
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : Ideal (R ⧸ I)
hJ : J ∈ minimalPrimes (R ⧸ I)
h : (comap (Quotient.mk I) J).IsMaximal
this : J = ⊤ ∨ J.IsMaximal
⊢ J.IsMaximal

Tactic:
]

Goal state after:
case refine_2
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : Ideal (R ⧸ I)
hJ : J ∈ minimalPrimes (R ⧸ I)
h : (comap (Quotient.mk I) J).IsMaximal
this : J = ⊤ ∨ J.IsMaximal
⊢ J.IsMaximal
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = v x
⊢ v y = v x

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = v x
⊢ v y = v x
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : v x = 0
⊢ v (x - y) = v y

Tactic:
by_cases hy : v y = 0
  · simpa [*] using map_sub v x y
  · simp [*, map_sub_eq_of_lt_right, zero_lt_iff]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hy : v y = 0
⊢ v x = v x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
h₁ : KrullDimLE 0 R
h₂ : IsLocalRing R
x : R
⊢ x ∈ sInf {J | 0 ≤ J ∧ J.IsPrime} ↔ x ∈ IsLocalRing.maximalIdeal R

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
h₁ : KrullDimLE 0 R
h₂ : IsLocalRing R
x : R
⊢ x ∈ sInf {J | 0 ≤ J ∧ J.IsPrime} ↔ x ∈ IsLocalRing.maximalIdeal R
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : v x = 0
⊢ v y = v y

Tactic:
]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < v 1
⊢ v (1 + x) = 1

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < v 1
⊢ v (1 + x) = 1
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ C r * X ^ n * X ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
]

Goal state after:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ C r * X ^ n * X ∈ Subring.closure (insert X {f | f.degree ≤ 0})
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 - x) = 1

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 - x) = 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 + -x) = 1

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 + -x) = 1
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m - ↑v * ϖ ^ m = 0
⊢ u = v

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m - ↑v * ϖ ^ m = 0
⊢ u = v
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0
⊢ u = v

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0
⊢ u = v
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
inst✝ : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
⊢ sInf {J | I ≤ J ∧ J.IsPrime} = IsLocalRing.maximalIdeal R

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
inst✝ : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
⊢ sInf {J | I ≤ J ∧ J.IsPrime} = IsLocalRing.maximalIdeal R
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
inst✝² : KrullDimLE 0 R
inst✝¹ : IsReduced R
inst✝ : IsLocalRing R
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u = ↑v
⊢ u = v

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u = ↑v
⊢ u = v
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I✝ : Ideal R
inst✝ : Ring.KrullDimLE 0 R
I : Ideal R
hI : I.IsRadical
⊢ I = I

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : I = ⊤
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = ↑u * ϖ ^ n
⊢ ↑n = ↑n

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : Irreducible ϖ
n : ℕ
⊢ ↑n = ↑n

Tactic:
]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
⊢ (if x = 0 then 0 else 1) ≤ 1

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
⊢ (if x = 0 then 0 else 1) ≤ 1
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
hi : Irreducible (Classical.choose ⋯)
n : ℕ
u : Rˣ
h : ¬Classical.choose ⋯ ^ n * ↑u = 0
ha : Associated (Classical.choose ⋯ ^ n * ↑u) (Classical.choose ⋯ ^ n)
⊢ ¬↑n = ⊤

Tactic:
]

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
hi : Irreducible (Classical.choose ⋯)
n : ℕ
u : Rˣ
h : ¬Classical.choose ⋯ ^ n * ↑u = 0
ha : Associated (Classical.choose ⋯ ^ n * ↑u) (Classical.choose ⋯ ^ n)
⊢ ¬↑n = ⊤
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
⊢ (if x = 0 then 0 else 1) < 1 ↔ x = 0

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
⊢ (if x = 0 then 0 else 1) < 1 ↔ x = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : b = 0
ha0 : a = 0
⊢ a ∣ b

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : b = 0
ha0 : a = 0
⊢ a ∣ b
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : b = 0
ha0 : a = 0
⊢ a ∣ 0

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : b = 0
ha0 : a = 0
⊢ a ∣ 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : ∀ (n : ℕ), Classical.choose ⋯ ^ n ∣ a → Classical.choose ⋯ ^ n ∣ b
ha0 : ¬a = 0
n : ℕ
ha : Associated a (Classical.choose ⋯ ^ n)
⊢ a ∣ b

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : ∀ (n : ℕ), Classical.choose ⋯ ^ n ∣ a → Classical.choose ⋯ ^ n ∣ b
ha0 : ¬a = 0
n : ℕ
ha : Associated a (Classical.choose ⋯ ^ n)
⊢ a ∣ b
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀
x✝ : R
x_in : x✝ ∈ {x | v x ≤ γ}
⊢ v x✝ ≤ γ

Tactic:
]

Goal state after:
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀
x✝ : R
x_in : x✝ ∈ {x | v x ≤ γ}
⊢ v x✝ ≤ γ
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : a ∣ b
⊢ emultiplicity (Classical.choose ⋯) a ≤ emultiplicity (Classical.choose ⋯) b

Tactic:
]

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : a ∣ b
⊢ emultiplicity (Classical.choose ⋯) a ≤ emultiplicity (Classical.choose ⋯) b
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑0 = 0

pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑u = ↑u * ϖ ^ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑0 = 0

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑u = ↑u * ϖ ^ 0
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
fa : R
fh : ∅ ≠ ∅ → (∀ b ∈ ∅, Associated x b) → ∃ n, Associated (x ^ n) ∅.prod
hf₂ : fa ::ₘ ∅ ≠ ∅
this : ∀ b ∈ fa ::ₘ ∅, Associated x b
⊢ Associated x fa

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
fa : R
fh : ∅ ≠ ∅ → (∀ b ∈ ∅, Associated x b) → ∃ n, Associated (x ^ n) ∅.prod
hf₂ : fa ::ₘ ∅ ≠ ∅
this : ∀ b ∈ fa ::ₘ ∅, Associated x b
⊢ Associated x fa
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : ⊤ = (addVal R) y
hx : x = 0
⊢ Associated 0 0

Tactic:
]

Goal state after: