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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v x < v y ↔ v x < 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✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v x ≤ v y ↔ v x ≤ v y

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ a ∈ maximalIdeal R, a = 0
⊢ maximalIdeal R ≤ ⊥

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ a ∈ maximalIdeal R, a = 0
⊢ maximalIdeal R ≤ ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose h else 0) + if y ∣ x then 0 else x) = x

Tactic:
]

Goal state after:
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose h else 0) + if y ∣ x then 0 else x) = x
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
⊢ a ∈ ↑(maximalIdeal R)

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
⊢ a ∈ ↑(maximalIdeal R)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ v x < 1 ↔ v x < 1

Tactic:
]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ v x ≤ 1 ↔ v x ≤ 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
⊢ sInf {J | Ideal.span {a} ≤ J ∧ J.IsPrime} = maximalIdeal R

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
⊢ sInf {J | Ideal.span {a} ≤ J ∧ J.IsPrime} = maximalIdeal R
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_1.inr
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = C (p.coeff 0)
⊢ ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) (C (p.coeff 0)) =
    (φ'.comp (algebraMap (R ⧸ P') Rₘ)) ((Ideal.Quotient.mk P') (p.coeff 0))

Tactic:
]

Goal state after:
case refine_1.inr
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = C (p.coeff 0)
⊢ ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) (C (p.coeff 0)) =
    (φ'.comp (algebraMap (R ⧸ P') Rₘ)) ((Ideal.Quotient.mk P') (p.coeff 0))
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : x = 0
⊢ y * 0 + 0 = x

Tactic:
]

Goal state after:
case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : x = 0
⊢ y * 0 + 0 = x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : x = 0
⊢ 0 * 0 + 0 = 0

Tactic:
]

Goal state after:
case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : x = 0
⊢ 0 * 0 + 0 = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : ¬y ∣ x
⊢ 0 * 0 + x = x

Tactic:
]

Goal state after:
case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : ¬y ∣ x
⊢ 0 * 0 + x = x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : ¬y = 0
h₂ : y ∣ x
⊢ x + 0 = x

Tactic:
]

Goal state after:
case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : ¬y = 0
h₂ : y ∣ x
⊢ x + 0 = x
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
I : Ideal R
hI : I ∈ {J | Ideal.span {a} ≤ J ∧ J.IsPrime}
e : I = ⊥
⊢ Ideal.span {a} ≤ I

Tactic:
]

Goal state after:
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
I : Ideal R
hI : I ∈ {J | Ideal.span {a} ≤ J ∧ J.IsPrime}
e : I = ⊥
⊢ Ideal.span {a} ≤ I
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
⊢ ¬(ofClass v) x = 0

Tactic:
]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
⊢ ¬(ofClass v) x = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
⊢ toWithBotNat (if y ∣ x then 0 else x) < toWithBotNat y

Tactic:
]

Goal state after:
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
⊢ toWithBotNat (if y ∣ x then 0 else x) < toWithBotNat y
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
q : R[X] ⧸ P
hq : q ∈ M'
p : R[X]
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) ((Ideal.Quotient.mk P) p)
⊢ ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) p ∈
    Subring.closure (⇑((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) '' insert X {p | p.degree ≤ 0})

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
q : R[X] ⧸ P
hq : q ∈ M'
p : R[X]
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) ((Ideal.Quotient.mk P) p)
⊢ ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) p ∈
    Subring.closure (⇑((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) '' insert X {p | p.degree ≤ 0})
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this : (Ideal.span {a}).radical = maximalIdeal R
⊢ ∃ n, (Ideal.span {a}).radical ^ n ≤ Ideal.span {a}

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this : (Ideal.span {a}).radical = maximalIdeal R
⊢ ∃ n, (Ideal.span {a}).radical ^ n ≤ Ideal.span {a}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : y ∣ x
⊢ y ≠ 0

Tactic:
]

Goal state after:
case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : y ∣ x
⊢ y ≠ 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : ¬x = 0
⊢ x ∣ x * y

Tactic:
]

Goal state after:
case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : ¬x = 0
⊢ x ∣ x * y
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
ϖ✝ : O
h : Irreducible ϖ✝
⊢ ↑(maximalIdeal O) = ↑(maximalIdeal O)

Tactic:
]

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

Goal state before:
pp: case right
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
ha0 : v.restrict a ≠ 0
⊢ v x = v a * embedding ↑γ

Tactic:
]

Goal state after:
case right
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
ha0 : v.restrict a ≠ 0
⊢ v x = v a * embedding ↑γ
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
⊢ Function.Injective ⇑(algebraMap S Sₘ)

Tactic:
]

Goal state after:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
⊢ Function.Injective ⇑(algebraMap S Sₘ)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case right
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
ha0 : v.restrict a ≠ 0
⊢ (ofClass v) a * ↑↑u = (ofClass v) a * embedding ↑γ

Tactic:
]

Goal state after:
case right
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
ha0 : v.restrict a ≠ 0
⊢ (ofClass v) a * ↑↑u = (ofClass v) a * embedding ↑γ
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case right.e_a
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
ha0 : v.restrict a ≠ 0
⊢ ↑↑u = embedding ↑(WithZero.unzero ⋯)

Tactic:
]

Goal state after:
case right.e_a
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
ha0 : v.restrict a ≠ 0
⊢ ↑↑u = embedding ↑(WithZero.unzero ⋯)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this✝ : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
n : ℕ
this : v ((algebraMap O K) ϖ) ^ n = v ((algebraMap O K) (ϖ ^ n))
⊢ ↑(maximalIdeal O ^ n) = ↑(maximalIdeal O ^ n)

Tactic:
]

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

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this✝ = 0
this : ⊤ ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
]

Goal state after:
case neg.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this✝ = 0
this : ⊤ ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
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.Jacobson.Ring

Goal state before:
pp: S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
hϕ' : comap (algebraMap S Sₘ) ⊥ = ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ ⊥.jacobson ≤ sInf (comap (algebraMap S Sₘ) '' {J | ⊥ ≤ J ∧ J.IsMaximal})

Tactic:
]

Goal state after:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
hϕ' : comap (algebraMap S Sₘ) ⊥ = ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ ⊥.jacobson ≤ sInf (comap (algebraMap S Sₘ) '' {J | ⊥ ≤ J ∧ J.IsMaximal})
Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)
x : K
hx : IsIntegral (↥(⨅ i, S i)) x
i : ι
le : ⨅ i, S i ≤ S i
algInst✝ : Algebra ↥(⨅ i, S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ i, S i)) (↥(S i)) K
val✝ : K
hin : val✝ ∈ S i
hy : (algebraMap (↥(S i)) K) ⟨val✝, hin⟩ = x
⊢ (algebraMap (↥(S i)) K) ⟨val✝, hin⟩ ∈ S i

Tactic:
]

Goal state after:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)
x : K
hx : IsIntegral (↥(⨅ i, S i)) x
i : ι
le : ⨅ i, S i ≤ S i
algInst✝ : Algebra ↥(⨅ i, S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ i, S i)) (↥(S i)) K
val✝ : K
hin : val✝ ∈ S i
hy : (algebraMap (↥(S i)) K) ⟨val✝, hin⟩ = x
⊢ (algebraMap (↥(S i)) K) ⟨val✝, hin⟩ ∈ S i