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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
a b : R
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
a b : R
⊢ ∃ c, a * c = b ∨ b * c = a
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 ⊥ ^ 0 • ⊤]

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
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f (n + 1) ≡ f 1 [SMOD ⊥ ^ (n + 1) • ⊤]

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 ⊥ ^ 0 • ⊤]
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
hx : 0 ∈ S
⊢ v.leSubmodule (v 0) ≤ S

pp: case inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
hx0 : x ≠ 0
⊢ v.leSubmodule (v x) ≤ S

Tactic:
·

Goal state after:
case inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
hx : 0 ∈ S
⊢ v.leSubmodule (v 0) ≤ S
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mp
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
⊢ ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

pp: case mpr
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
⊢ (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R

Tactic:
·

Goal state after:
case mp
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
⊢ ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mp.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 : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) (x * s)) ∨
    IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) (x * s))⁻¹

pp: case mp.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 : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y) ∨
    IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y)⁻¹

Tactic:
·

Goal state after:
case mp.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 : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) (x * s)) ∨
    IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) (x * s))⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mp.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 : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y) ∨
    IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y)⁻¹

Tactic:
·

Goal state after:
case mp.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 : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y) ∨
    IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y)⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mpr
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
⊢ (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R

Tactic:
·

Goal state after:
case mpr
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
⊢ (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case pos
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 : a = 0
⊢ ∃ c, a * c = b ∨ b * c = a

pp: case neg
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 : ¬a = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
·

Goal state after:
case pos
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 : a = 0
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.Valuation.Integers

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

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

Tactic:
·

Goal state after:
case mp
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ (∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x) → v x ≤ min 1 γ
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 : ℕ
⊢ f n ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
Subsingleton.elim (f n) 0

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
inst✝ : Subsingleton M
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
n : ℕ
⊢ 0 ≡ 0 [SMOD I ^ n • ⊤]
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 : ℕ
⊢ f n ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
by rw [Subsingleton.elim (f n) 0]

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

Goal state before:
pp: case pos
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 : ¬a = 0
hb : b = 0
⊢ ∃ c, a * c = b ∨ b * c = a

pp: case neg
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 : ¬a = 0
hb : ¬b = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
·

Goal state after:
case pos
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 : ¬a = 0
hb : b = 0
⊢ ∃ c, a * c = b ∨ b * c = a
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) ≤ min 1 γ

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) ≤ min 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) ≤ min 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) ≤ min 1 γ

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) ≤ min 1 γ
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 : (algebraMap R K) c = (algebraMap R K) a / (algebraMap R K) b
⊢ ∃ c, a * c = b ∨ b * c = a

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 : (algebraMap R K) c = ((algebraMap R K) a / (algebraMap R K) b)⁻¹
⊢ ∃ 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 : (algebraMap R K) c = (algebraMap R K) a / (algebraMap R K) b
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.Valuation.Integers

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

Tactic:
·

Goal state after:
case mpr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ v x ≤ min 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 : (algebraMap R K) c = ((algebraMap R K) a / (algebraMap R K) 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 : (algebraMap R K) c = ((algebraMap R K) a / (algebraMap R K) b)⁻¹
⊢ ∃ c, a * c = b ∨ b * c = a
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

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.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.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.Valuation.Integers

Goal state before:
pp: case inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
hx : 0 ∈ I
⊢ v.leIdeal (v ↑0) ≤ I

pp: case inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
hx0 : x ≠ 0
⊢ v.leIdeal (v ↑x) ≤ I

Tactic:
·

Goal state after:
case inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
hx : 0 ∈ I
⊢ v.leIdeal (v ↑0) ≤ I
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_1
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
x✝¹ : AdicCompletion I M
h : ∀ (n : ℕ), x✝¹ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
x✝ : x ∈ ⊤
⊢ ↑(r • x) n = ↑0 n

pp: case refine_2
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
x✝ : AdicCompletion I M
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
x y : AdicCompletion I M
hx : ↑x n = ↑0 n
hy : ↑y n = ↑0 n
⊢ ↑(x + y) n = ↑0 n

Tactic:
·

Goal state after:
case refine_1
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
x✝¹ : AdicCompletion I M
h : ∀ (n : ℕ), x✝¹ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
x✝ : x ∈ ⊤
⊢ ↑(r • x) n = ↑0 n
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_2
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
x✝ : AdicCompletion I M
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
x y : AdicCompletion I M
hx : ↑x n = ↑0 n
hy : ↑y n = ↑0 n
⊢ ↑(x + y) n = ↑0 n

Tactic:
·

Goal state after:
case refine_2
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
x✝ : AdicCompletion I M
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
x y : AdicCompletion I M
hx : ↑x n = ↑0 n
hy : ↑y n = ↑0 n
⊢ ↑(x + y) n = ↑0 n
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ IsDiscreteValuationRing R → IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

pp: case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime) → IsDiscreteValuationRing R

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ IsDiscreteValuationRing R → IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime
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 (max (Ideal.span {x}) (Ideal.span {y}))

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

Goal state before:
pp: case mp.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R

pp: case mp.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
·

Goal state after:
case mp.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R)

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 ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Tactic:
·

Goal state after:
case h.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) (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 ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = 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 ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ IsAdicCauchy I M f → ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ (∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) → IsAdicCauchy I M f

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ IsAdicCauchy I M f → ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ (∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) → IsAdicCauchy I M f

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ (∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) → IsAdicCauchy I M f
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 (max (Ideal.span {x}) (Ideal.span {y}))

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 (max (Ideal.span {x}) (Ideal.span {y}))
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 : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ f m ≡ ?m.68 [SMOD I ^ m • ⊤]

pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ ?m.68 ≡ f (n + 1) [SMOD I ^ m • ⊤]

pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ M

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 : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ f m ≡ ?m.68 [SMOD I ^ m • ⊤]
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime) → IsDiscreteValuationRing R

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime) → IsDiscreteValuationRing R