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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a ↦ a * g) (x * a + y * b) = (fun a ↦ a * g) 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a ↦ a * g) (x * a + y * b) = (fun a ↦ a * g) 1
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : ℕ → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = ↑u n
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I M hmn) (Submodule.Quotient.mk (x n✝)) = Submodule.Quotient.mk (x n✝)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : ℕ → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = ↑u n
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I M hmn) (Submodule.Quotient.mk (x n✝)) = Submodule.Quotient.mk (x n✝)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
c : 𝒪
hc : a = b * c
⊢ a * c = b ∨ b * c = a

Tactic:
;

Goal state after:
case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
c : 𝒪
hc : a = b * c
⊢ a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ∀ r ∈ I ^ n, ∀ (n_1 : AdicCompletion I M), r • ↑n_1 n = 0

Tactic:
intro r

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r : R
⊢ r ∈ I ^ n → ∀ (n_1 : AdicCompletion I M), r • ↑n_1 n = 0
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
c : 𝒪
hc : b = a * c
⊢ a * c = b ∨ b * c = a

Tactic:
;

Goal state after:
case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
c : 𝒪
hc : b = a * c
⊢ a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
x✝ : M
⊢ (of I N ∘ₗ lift I f ⋯) x✝ = (AdicCompletion.lift I f ⋯) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
x✝ : M
⊢ (of I N ∘ₗ lift I f ⋯) x✝ = (AdicCompletion.lift I f ⋯) x✝
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
⊢ ∃ n, p ^ n ∈ I

Tactic:
obtain ⟨n, u, rfl⟩ := H hx0

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
n : ℕ
u : Rˣ
hxI : p ^ n * ↑u ∈ I
hx0 : p ^ n * ↑u ≠ 0
⊢ ∃ n, p ^ n ∈ I
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.a
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ I ≤ span {p ^ Nat.find ex}

Tactic:
intro r

Goal state after:
case h.a
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
r : R
⊢ r ∈ I → r ∈ span {p ^ Nat.find ex}
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x✝ : M
⊢ ((I ^ n • ⊤).mkQ ∘ₗ lift I f ⋯) x✝ = (f n) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x✝ : M
⊢ ((I ^ n • ⊤).mkQ ∘ₗ lift I f ⋯) x✝ = (f n) x✝
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ sInf (comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) '' {J | ⊥ ≤ J ∧ J.IsMaximal}) ≤ ⊥.jacobson

Tactic:
refine sInf_le_sInf fun J hJ => ?_

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
⊢ J ∈ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) '' {J | ⊥ ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
f : R →*₀ Γ₀
map_add_le_max'✝ : ∀ (x y : R), (↑f).toFun (x + y) ≤ max ((↑f).toFun x) ((↑f).toFun y)
g : Valuation R Γ₀
hfg : { toMonoidWithZeroHom := f, map_add_le_max' := map_add_le_max'✝ }.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ { toMonoidWithZeroHom := f, map_add_le_max' := map_add_le_max'✝ } = g

Tactic:
;

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
f : R →*₀ Γ₀
map_add_le_max'✝ : ∀ (x y : R), (↑f).toFun (x + y) ≤ max ((↑f).toFun x) ((↑f).toFun y)
g : Valuation R Γ₀
hfg : { toMonoidWithZeroHom := f, map_add_le_max' := map_add_le_max'✝ }.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ { toMonoidWithZeroHom := f, map_add_le_max' := map_add_le_max'✝ } = g
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g
⊢ v (∑ i ∈ insert a s, f i) ≤ g

Tactic:
;

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g
⊢ v (∑ i ∈ insert a s, f i) ≤ g
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x✝ : M
⊢ ((I ^ a n • ⊤).mkQ ∘ₗ lift I ha f ⋯) x✝ = (f n) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x✝ : M
⊢ ((I ^ a n • ⊤).mkQ ∘ₗ lift I ha f ⋯) x✝ = (f n) 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 Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ i ∈ s✝, v (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g
hf : v (f a) < g ∧ ∀ x ∈ s, v (f x) < g
⊢ v (∑ i ∈ insert a s, f i) < g

Tactic:
;

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ i ∈ s✝, v (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g
hf : v (f a) < g ∧ ∀ x ∈ s, v (f x) < g
⊢ v (∑ i ∈ insert a s, f i) < g
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.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
x✝ : Ideal R
⊢ x✝ ∈ minimalPrimes R ↔ x✝ ∈ {I | I.IsMaximal}

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
x✝ : Ideal R
⊢ x✝ ∈ minimalPrimes R ↔ x✝ ∈ {I | I.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (a : R), C a ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
intro r

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
p : R[X]
r : R
⊢ C r ∈ Subring.closure (insert X {f | f.degree ≤ 0})
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✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ₀
r✝ : R
⊢ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ (map (MonoidWithZeroHom.ofClass f) ⋯ x✝)) r✝ = x✝ r✝

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✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ₀
r✝ : R
⊢ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ (map (MonoidWithZeroHom.ofClass f) ⋯ x✝)) r✝ = x✝ 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✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ'₀
r✝ : R
⊢ (map (MonoidWithZeroHom.ofClass f) ⋯ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ x✝)) r✝ = x✝ r✝

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✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ'₀
r✝ : R
⊢ (map (MonoidWithZeroHom.ofClass f) ⋯ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ x✝)) r✝ = x✝ 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
⊢ nilradical R = ⊥

Tactic:
nilradical_eq_zero,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : KrullDimLE 0 R
inst✝¹ : IsReduced R
inst✝ : IsLocalRing R
⊢ 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 = ⊤
⊢ I = maximalIdeal R ^ 0

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 = ⊤
⊢ I = maximalIdeal R ^ 0
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case neg
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 = ⊤
⊢ ∃ n, I = maximalIdeal R ^ n

Tactic:
have H : ∀ r : R, ¬IsUnit r ↔ x ∣ r := fun r =>
    (SetLike.ext_iff.mp hx r).trans Ideal.mem_span_singleton

Goal state after:
case neg
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
⊢ ∃ n, I = maximalIdeal R ^ n
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: 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
⊢ ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r

Tactic:
intro r

Goal state after:
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
r : R
⊢ r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

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

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
⊢ (addVal R) a ≤ (addVal R) b

Tactic:
· by_cases ha0 : a = 0
    · rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h
      rw [h]
      apply dvd_zero
    obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 hp.irreducible
    rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply,
      emultiplicity_le_emultiplicity_iff] at h
    exact ha.dvd.trans (h n ha.symm.dvd)

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
⊢ (addVal R) a ≤ (addVal R) b
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: 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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ r ∈ I, r = 0
⊢ False

Tactic:
;

Goal state after:
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ r ∈ I, r = 0
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: 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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ r ∈ I, r = 0
⊢ I = ⊥

Tactic:
;

Goal state after:
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ r ∈ I, r = 0
⊢ I = ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: 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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ r ∈ I, r = 0
⊢ I ≤ ⊥

Tactic:
;

Goal state after:
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ r ∈ I, r = 0
⊢ I ≤ ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case pos
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this

pp: case neg
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : ¬s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this

Tactic:
;

Goal state after:
case pos
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this

case neg
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : ¬s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case pos
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ 0 ∈ maximalIdeal R ^ Nat.find this

Tactic:
;

Goal state after:
case pos
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
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ 0 ∈ maximalIdeal R ^ Nat.find this
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
⊢ toWithBotNat x ≠ ⊥ ↔ x ≠ 0

Tactic:
;

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
⊢ toWithBotNat x ≠ ⊥ ↔ x ≠ 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case top
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vy : ℕ∞
hvy : (addVal R) y = vy
hvx : x = 0
⊢ ⊤ ≤ vy ↔ x ∣ y

Tactic:
;

Goal state after:
case top
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vy : ℕ∞
hvy : (addVal R) y = vy
hvx : x = 0
⊢ ⊤ ≤ vy ↔ x ∣ y
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case coe.top
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : (addVal R) x = ↑vx
hvy : y = 0
⊢ ↑vx ≤ ⊤ ↔ x ∣ y

Tactic:
;

Goal state after:
case coe.top
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : (addVal R) x = ↑vx
hvy : y = 0
⊢ ↑vx ≤ ⊤ ↔ x ∣ y
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal ⊥

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal ⊥