-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
lemma adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (v : HeightOneSpectrum R)
    (a : v.adicCompletion K) : ∃ b ∈ R⁰, a * b ∈ v.adicCompletionIntegers K

Proof state:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
hϖ0 : ϖ ≠ 0
⊢ d + d * -1 ≤ 0

Tactic:
omega

Result:
no goals

Proof state:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
hϖ0 : ϖ ≠ 0
⊢ a * ↑(ϖ ^ d.natAbs) ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers, algebraMap.coe_pow, map_mul, hd, map_pow,
  valuedAdicCompletion_eq_valuation, valuation_eq_intValuationDef, hϖ, ← WithZero.coe_pow,
  ← WithZero.coe_mul, WithZero.coe_le_one, ← toAdd_le, toAdd_mul, toAdd_ofAdd, toAdd_pow,
  toAdd_ofAdd, toAdd_one,
  show d.natAbs • (-1) = (d.natAbs : ℤ) • (-1) by simp only [nsmul_eq_mul,
    Int.natCast_natAbs, smul_eq_mul],
  ← Int.eq_natAbs_of_zero_le ha.le, smul_eq_mul]

Result:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
hϖ0 : ϖ ≠ 0
⊢ d + d * -1 ≤ 0

Proof state:
case neg.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
obtain ⟨ϖ, hϖ⟩ := intValuation_exists_uniformizer v

Result:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : 1 < Valued.v a
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
obtain ⟨d, hd⟩ : ∃ d : ℤ, Valued.v a = ofAdd d :=
  Option.ne_none_iff_exists'.mp <| (lt_trans zero_lt_one ha).ne'

Result:
case neg.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : 1 < Valued.v a
d : ℤ
hd : Valued.v a = ↑(ofAdd d)
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Proof state:
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : a ∈ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
use 1

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : a ∈ adicCompletionIntegers K v
⊢ 1 ∈ R⁰ ∧ a * ↑1 ∈ adicCompletionIntegers K v

Proof state:
case neg.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : 1 < Valued.v a
d : ℤ
hd : Valued.v a = ↑(ofAdd d)
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
rw [hd, WithZero.one_lt_coe, ← ofAdd_zero, ofAdd_lt] at ha

Result:
case neg.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : a ∈ adicCompletionIntegers K v
⊢ 1 ∈ R⁰ ∧ a * ↑1 ∈ adicCompletionIntegers K v

Tactic:
simp [ha, Submonoid.one_mem]

Result:
no goals

Proof state:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
have hϖ0 : ϖ ≠ 0 := by rintro rfl; simp at hϖ

Result:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
hϖ0 : ϖ ≠ 0
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : a ∉ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
rw [not_mem_adicCompletionIntegers] at ha

Result:
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : 1 < Valued.v a
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Proof state:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
hϖ0 : ϖ ≠ 0
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
refine ⟨ϖ^d.natAbs, pow_mem (mem_nonZeroDivisors_of_ne_zero hϖ0) _, ?_⟩

Result:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
hϖ0 : ϖ ≠ 0
⊢ a * ↑(ϖ ^ d.natAbs) ∈ adicCompletionIntegers K v

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
by_cases ha : a ∈ v.adicCompletionIntegers K

Result:
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : a ∈ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : a ∉ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v