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

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f 0 ≡ f 1 [SMOD ⊤]

Tactic:
]

Goal state after:
case zero
R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f 0 ≡ f 1 [SMOD ⊤]
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
n : ℕ
hf : f 1 = f (n + 1)
⊢ f (n + 1) ≡ f 1 [SMOD ⊥ ^ (n + 1) • ⊤]

Tactic:
]

Goal state after:
case succ
R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
n : ℕ
hf : f 1 = f (n + 1)
⊢ f (n + 1) ≡ f 1 [SMOD ⊥ ^ (n + 1) • ⊤]
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
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ (algebraMap R K) x * (algebraMap R K) s = (algebraMap R K) x * (algebraMap R K) s

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
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ (algebraMap R K) (x * s) ≠ 0

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
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ (algebraMap R K) (x * s) ≠ 0
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
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ (algebraMap R K) y * (algebraMap R K) s = (algebraMap R K) y * (algebraMap R K) s

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
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ (algebraMap R K) y ≠ 0

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
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ (algebraMap R K) y ≠ 0
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
n : ℕ
hf : f 1 = f (n + 1)
⊢ f (n + 1) ≡ f (n + 1) [SMOD ⊥ ^ (n + 1) • ⊤]

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊤ ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD ⊤]

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊤ ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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✝ : Subsingleton M
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
n : ℕ
⊢ 0 ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
]

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

Goal state before:
pp: case mp.inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
h : min 1 γ = 1
right✝ : 1 ≤ γ
⊢ v ((algebraMap (↥v.integer) K) y) ≤ 1

Tactic:
]

Goal state after:
case mp.inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
h : min 1 γ = 1
right✝ : 1 ≤ γ
⊢ v ((algebraMap (↥v.integer) K) y) ≤ 1
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
h : min 1 γ = γ
right✝ : γ < 1
⊢ v ((algebraMap (↥v.integer) K) y) ≤ γ

Tactic:
]

Goal state after:
case mp.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
h : min 1 γ = γ
right✝ : γ < 1
⊢ v ((algebraMap (↥v.integer) K) y) ≤ γ
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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✝ b✝ : (n : ℕ) → M ⧸ I ^ n • ⊤
hf : a✝ ∈ {f | ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) (f n) = f m}
hg : b✝ ∈ {f | ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) (f n) = f m}
m n : ℕ
hmn : m ≤ n
⊢ a✝ m + b✝ m = a✝ m + b✝ m

Tactic:
]

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

Goal state before:
pp: case neg.inl
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : b * c = a
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
]

Goal state after:
case neg.inl
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : b * c = a
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case mpr.inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ 1
h : min 1 γ = 1
h' : 1 ≤ γ
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

Tactic:
]

Goal state after:
case mpr.inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ 1
h : min 1 γ = 1
h' : 1 ≤ γ
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg.inr
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : a * c = b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
]

Goal state after:
case neg.inr
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : a * c = b
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mpr.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

Tactic:
]

Goal state after:
case mpr.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
c : R
f : (n : ℕ) → M ⧸ I ^ n • ⊤
hf : f ∈ {f | ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) (f n) = f m}
m n : ℕ
hmn : m ≤ n
⊢ c • f m = c • f m

Tactic:
]

Goal state after:
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✝ : ValuationRing R
⊢ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

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✝ : ValuationRing R
⊢ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
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✝ : ValuationRing R
x y : R
⊢ Submodule.IsPrincipal (max (Ideal.span {x}) (Ideal.span {y}))

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✝ : ValuationRing R
x y : R
⊢ Submodule.IsPrincipal (max (Ideal.span {x}) (Ideal.span {y}))
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * b
ha : ∃ a_1, a_1 * ϖ = a
hb : ∃ a, a * ϖ = b
⊢ False

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * b
ha : ∃ a_1, a_1 * ϖ = a
hb : ∃ a, a * ϖ = b
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * b
ha : ∃ a_1, a_1 * ϖ = a
hb : ∃ a, a * ϖ = b
⊢ False

Tactic:
rcases ha with ⟨a, rfl⟩

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
b : R
hb : ∃ a, a * ϖ = b
a : R
hab : ϖ = a * ϖ * b
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = ϖ * (ϖ * (a * b))
⊢ False

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = ϖ * (ϖ * (a * b))
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : maximalIdeal R = span {ϖ}
e : ϖ = 0
⊢ ϖ = 0

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : maximalIdeal R = span {ϖ}
e : ϖ = 0
⊢ ϖ = 0
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case inl
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✝ : ValuationRing R
x y : R
h : Ideal.span {x} ≤ Ideal.span {y}
⊢ Submodule.IsPrincipal (Ideal.span {y})

Tactic:
]

Goal state after:
case inl
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✝ : ValuationRing R
x y : R
h : Ideal.span {x} ≤ Ideal.span {y}
⊢ Submodule.IsPrincipal (Ideal.span {y})
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hQ2 : Prime q
hq : q ≠ 0
⊢ R ∙ q = maximalIdeal R

Tactic:
]

Goal state after:
case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hQ2 : Prime q
hq : q ≠ 0
⊢ R ∙ q = maximalIdeal R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hq : q ≠ 0
hQ2 : maximalIdeal R = span {q}
⊢ R ∙ q = maximalIdeal R

Tactic:
]

Goal state after:
case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hq : q ≠ 0
hQ2 : maximalIdeal R = span {q}
⊢ R ∙ q = maximalIdeal R
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case inr
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✝ : ValuationRing R
x y : R
h : Ideal.span {y} ≤ Ideal.span {x}
⊢ Submodule.IsPrincipal (Ideal.span {x})

Tactic:
]

Goal state after:
case inr
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✝ : ValuationRing R
x y : R
h : Ideal.span {y} ≤ Ideal.span {x}
⊢ Submodule.IsPrincipal (Ideal.span {x})
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : maximalIdeal R = span {a}
hb : maximalIdeal R = span {b}
⊢ Associated a b

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : maximalIdeal R = span {a}
hb : maximalIdeal R = span {b}
⊢ Associated a b
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
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∈ Ideal.span {a, b}

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
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∈ Ideal.span {a, b}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : maximalIdeal R = span {a}
hb : maximalIdeal R = span {b}
⊢ span {b} = span {b}

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
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
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
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
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ b ∈ Ideal.span {a * g, b}

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
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ b ∈ Ideal.span {a * g, b}
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}
⊢ g ∈ Ideal.span {g}

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}
⊢ g ∈ Ideal.span {g}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
⊢ Associated p ϖ

Tactic:
]

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
⊢ Associated p ϖ
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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : ↑f m ∈ I ^ l • ⊤
⊢ Submodule.Quotient.mk (↑f m) = 0 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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : ↑f m ∈ I ^ l • ⊤
⊢ Submodule.Quotient.mk (↑f m) = 0 n
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ * ϖ ^ n)
⊢ Associated p ϖ

Tactic:
]

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ * ϖ ^ n)
⊢ Associated p ϖ
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
⊢ Prime p

Tactic:
]

Goal state after:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
⊢ Prime p
Module: Mathlib.RingTheory.AdicCompletion.Basic

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

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
a b : R
h : p ∣ a * b
ha : a = 0
⊢ p ∣ 0 ∨ p ∣ b

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
a b : R
h : p ∣ a * b
ha : a = 0
⊢ p ∣ 0 ∨ p ∣ b
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
⊢ p ∣ Classical.choose hR ^ m * ↑u ∨ p ∣ b

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
⊢ p ∣ Classical.choose hR ^ m * ↑u ∨ p ∣ b