[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ intValuationDef v x ≠ 0
[PROOFSTEP]
rw [intValuationDef, if_neg hx]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))))) ≠ 0
[PROOFSTEP]
exact WithZero.coe_ne_zero
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : { x // x ∈ nonZeroDivisors R }
⊢ 0 < intValuationDef v ↑x
[PROOFSTEP]
rw [v.intValuationDef_if_neg (nonZeroDivisors.coe_ne_zero x)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : { x // x ∈ nonZeroDivisors R }
⊢ 0 < ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {↑x}))))))
[PROOFSTEP]
exact WithZero.zero_lt_coe _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
⊢ intValuationDef v x ≤ 1
[PROOFSTEP]
rw [intValuationDef]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
⊢ (if x = 0 then 0
    else
      ↑(↑ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))))) ≤
    1
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
hx : x = 0
⊢ (if x = 0 then 0
    else
      ↑(↑ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))))) ≤
    1
[PROOFSTEP]
rw [if_pos hx]
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
hx : x = 0
⊢ 0 ≤ 1
[PROOFSTEP]
exact WithZero.zero_le 1
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
hx : ¬x = 0
⊢ (if x = 0 then 0
    else
      ↑(↑ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))))) ≤
    1
[PROOFSTEP]
rw [if_neg hx, ← WithZero.coe_one, ← ofAdd_zero, WithZero.coe_le_coe, ofAdd_le, Right.neg_nonpos_iff]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
hx : ¬x = 0
⊢ 0 ≤ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
[PROOFSTEP]
exact Int.coe_nat_nonneg _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ intValuationDef v r < 1 ↔ v.asIdeal ∣ Ideal.span {r}
[PROOFSTEP]
rw [intValuationDef]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ (if r = 0 then 0
      else
        ↑(↑ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))))))) <
      1 ↔
    v.asIdeal ∣ Ideal.span {r}
[PROOFSTEP]
split_ifs with hr
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : r = 0
⊢ 0 < 1 ↔ v.asIdeal ∣ Ideal.span {r}
[PROOFSTEP]
simp [hr]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))))) < 1 ↔
    v.asIdeal ∣ Ideal.span {r}
[PROOFSTEP]
rw [← WithZero.coe_one, ← ofAdd_zero, WithZero.coe_lt_coe, ofAdd_lt, neg_lt_zero, ← Int.ofNat_zero, Int.ofNat_lt,
  zero_lt_iff]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ≠ 0 ↔
    v.asIdeal ∣ Ideal.span {r}
[PROOFSTEP]
have h : (Ideal.span { r } : Ideal R) ≠ 0 :=
  by
  rw [Ne.def, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
  exact hr
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ Ideal.span {r} ≠ 0
[PROOFSTEP]
rw [Ne.def, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ¬r = 0
[PROOFSTEP]
exact hr
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
h : Ideal.span {r} ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ≠ 0 ↔
    v.asIdeal ∣ Ideal.span {r}
[PROOFSTEP]
apply Associates.count_ne_zero_iff_dvd h (by apply v.irreducible)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
h : Ideal.span {r} ≠ 0
⊢ Irreducible v.asIdeal
[PROOFSTEP]
apply v.irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ intValuationDef v r ≤ ↑(↑ofAdd (-↑n)) ↔ v.asIdeal ^ n ∣ Ideal.span {r}
[PROOFSTEP]
rw [intValuationDef]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ (if r = 0 then 0
      else
        ↑(↑ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))))))) ≤
      ↑(↑ofAdd (-↑n)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
[PROOFSTEP]
split_ifs with hr
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
n : ℕ
hr : r = 0
⊢ 0 ≤ ↑(↑ofAdd (-↑n)) ↔ v.asIdeal ^ n ∣ Ideal.span {r}
[PROOFSTEP]
simp_rw [hr, Ideal.dvd_span_singleton, zero_le', Submodule.zero_mem]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))))) ≤
      ↑(↑ofAdd (-↑n)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
[PROOFSTEP]
rw [WithZero.coe_le_coe, ofAdd_le, neg_le_neg_iff, Int.ofNat_le, Ideal.dvd_span_singleton, ←
  Associates.le_singleton_iff,
  Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) (by apply v.associates_irreducible)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
apply v.associates_irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ intValuationDef v 1 = 1
[PROOFSTEP]
rw [v.intValuationDef_if_neg (zero_ne_one.symm : (1 : R) ≠ 0), Ideal.span_singleton_one, ← Ideal.one_eq_top,
  Associates.mk_one, Associates.factors_one, Associates.count_zero (by apply v.associates_irreducible), Int.ofNat_zero,
  neg_zero, ofAdd_zero, WithZero.coe_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
apply v.associates_irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
⊢ intValuationDef v (x * y) = intValuationDef v x * intValuationDef v y
[PROOFSTEP]
simp only [intValuationDef]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
⊢ (if x * y = 0 then 0
    else
      ↑(↑ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y}))))))) =
    (if x = 0 then 0
      else
        ↑(↑ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))))) *
      if y = 0 then 0
      else
        ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))))
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ (if x * y = 0 then 0
    else
      ↑(↑ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y}))))))) =
    (if x = 0 then 0
      else
        ↑(↑ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))))) *
      if y = 0 then 0
      else
        ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))))
[PROOFSTEP]
rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
⊢ (if x * y = 0 then 0
    else
      ↑(↑ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y}))))))) =
    (if x = 0 then 0
      else
        ↑(↑ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))))) *
      if y = 0 then 0
      else
        ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))))
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0
    else
      ↑(↑ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y}))))))) =
    (if x = 0 then 0
      else
        ↑(↑ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))))) *
      if y = 0 then 0
      else
        ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))))
[PROOFSTEP]
rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0
    else
      ↑(↑ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y}))))))) =
    (if x = 0 then 0
      else
        ↑(↑ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))))) *
      if y = 0 then 0
      else
        ↑(↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))))
[PROOFSTEP]
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithZero.coe_mul, WithZero.coe_inj, ← ofAdd_add, ←
  Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk, ← neg_add,
  Associates.count_mul (by apply Associates.mk_ne_zero'.mpr hx) (by apply Associates.mk_ne_zero'.mpr hy)
    (by apply v.associates_irreducible)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ Associates.mk (Ideal.span {x}) ≠ 0
[PROOFSTEP]
apply Associates.mk_ne_zero'.mpr hx
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ Associates.mk (Ideal.span {y}) ≠ 0
[PROOFSTEP]
apply Associates.mk_ne_zero'.mpr hy
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
apply v.associates_irreducible
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ ↑ofAdd
      (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))) +
            Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))) =
    ↑ofAdd
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) +
          ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))))
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b c : ℕ
⊢ ↑ofAdd (-↑c) ≤ max (↑ofAdd (-↑a)) (↑ofAdd (-↑b)) ↔ min a b ≤ c
[PROOFSTEP]
rw [le_max_iff, ofAdd_le, ofAdd_le, neg_le_neg_iff, neg_le_neg_iff, Int.ofNat_le, Int.ofNat_le, ← min_le_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
⊢ intValuationDef v (x + y) ≤ max (intValuationDef v x) (intValuationDef v y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ intValuationDef v (x + y) ≤ max (intValuationDef v x) (intValuationDef v y)
[PROOFSTEP]
rw [hx, zero_add]
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ intValuationDef v y ≤ max (intValuationDef v 0) (intValuationDef v y)
[PROOFSTEP]
conv_rhs => rw [intValuationDef, if_pos (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : x = 0
| max (intValuationDef v 0) (intValuationDef v y)
[PROOFSTEP]
rw [intValuationDef, if_pos (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : x = 0
| max (intValuationDef v 0) (intValuationDef v y)
[PROOFSTEP]
rw [intValuationDef, if_pos (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : x = 0
| max (intValuationDef v 0) (intValuationDef v y)
[PROOFSTEP]
rw [intValuationDef, if_pos (Eq.refl _)]
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ intValuationDef v y ≤ max 0 (intValuationDef v y)
[PROOFSTEP]
rw [max_eq_right (WithZero.zero_le (v.intValuationDef y))]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
⊢ intValuationDef v (x + y) ≤ max (intValuationDef v x) (intValuationDef v y)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ intValuationDef v (x + y) ≤ max (intValuationDef v x) (intValuationDef v y)
[PROOFSTEP]
rw [hy, add_zero]
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ intValuationDef v x ≤ max (intValuationDef v x) (intValuationDef v 0)
[PROOFSTEP]
conv_rhs => rw [max_comm, intValuationDef, if_pos (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
| max (intValuationDef v x) (intValuationDef v 0)
[PROOFSTEP]
rw [max_comm, intValuationDef, if_pos (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
| max (intValuationDef v x) (intValuationDef v 0)
[PROOFSTEP]
rw [max_comm, intValuationDef, if_pos (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
| max (intValuationDef v x) (intValuationDef v 0)
[PROOFSTEP]
rw [max_comm, intValuationDef, if_pos (Eq.refl _)]
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ intValuationDef v x ≤ max 0 (intValuationDef v x)
[PROOFSTEP]
rw [max_eq_right (WithZero.zero_le (v.intValuationDef x))]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ intValuationDef v (x + y) ≤ max (intValuationDef v x) (intValuationDef v y)
[PROOFSTEP]
by_cases hxy : x + y = 0
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ intValuationDef v (x + y) ≤ max (intValuationDef v x) (intValuationDef v y)
[PROOFSTEP]
rw [intValuationDef, if_pos hxy]
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ 0 ≤ max (intValuationDef v x) (intValuationDef v y)
[PROOFSTEP]
exact zero_le'
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ intValuationDef v (x + y) ≤ max (intValuationDef v x) (intValuationDef v y)
[PROOFSTEP]
rw [v.intValuationDef_if_neg hxy, v.intValuationDef_if_neg hx, v.intValuationDef_if_neg hy, WithZero.le_max_iff,
  IntValuation.le_max_iff_min_le]
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) ≤
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
[PROOFSTEP]
set nmin :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { x })).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { y })).factors)
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
[PROOFSTEP]
have h_dvd_x : x ∈ v.asIdeal ^ nmin :=
  by
  rw [← Associates.le_singleton_iff x nmin _, Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]
  exact min_le_left _ _
  apply v.associates_irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ x ∈ v.asIdeal ^ nmin
[PROOFSTEP]
rw [← Associates.le_singleton_iff x nmin _, Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
exact min_le_left _ _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
apply v.associates_irreducible
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
[PROOFSTEP]
have h_dvd_y : y ∈ v.asIdeal ^ nmin :=
  by
  rw [← Associates.le_singleton_iff y nmin _, Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hy) _]
  exact min_le_right _ _
  apply v.associates_irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ y ∈ v.asIdeal ^ nmin
[PROOFSTEP]
rw [← Associates.le_singleton_iff y nmin _, Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hy) _]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
exact min_le_right _ _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
apply v.associates_irreducible
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
[PROOFSTEP]
have h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y}) :=
  by
  rw [Associates.le_singleton_iff]
  exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
[PROOFSTEP]
rw [Associates.le_singleton_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ x + y ∈ v.asIdeal ^ nmin
[PROOFSTEP]
exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
[PROOFSTEP]
rw [Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hxy) _] at h_dvd_xy 
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
exact h_dvd_xy
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ Irreducible (Associates.mk v.asIdeal)
[PROOFSTEP]
apply v.associates_irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ∃ π, intValuationDef v π = ↑(↑ofAdd (-1))
[PROOFSTEP]
have hv : _root_.Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ∃ π, intValuationDef v π = ↑(↑ofAdd (-1))
[PROOFSTEP]
have hlt : v.asIdeal ^ 2 < v.asIdeal := by
  rw [← Ideal.dvdNotUnit_iff_lt]
  exact ⟨v.ne_bot, v.asIdeal, (not_congr Ideal.isUnit_iff).mpr (Ideal.IsPrime.ne_top v.isPrime), sq v.asIdeal⟩
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
⊢ v.asIdeal ^ 2 < v.asIdeal
[PROOFSTEP]
rw [← Ideal.dvdNotUnit_iff_lt]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
⊢ DvdNotUnit v.asIdeal (v.asIdeal ^ 2)
[PROOFSTEP]
exact ⟨v.ne_bot, v.asIdeal, (not_congr Ideal.isUnit_iff).mpr (Ideal.IsPrime.ne_top v.isPrime), sq v.asIdeal⟩
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
⊢ ∃ π, intValuationDef v π = ↑(↑ofAdd (-1))
[PROOFSTEP]
obtain ⟨π, mem, nmem⟩ := SetLike.exists_of_lt hlt
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
⊢ ∃ π, intValuationDef v π = ↑(↑ofAdd (-1))
[PROOFSTEP]
have hπ : Associates.mk (Ideal.span { π }) ≠ 0 :=
  by
  rw [Associates.mk_ne_zero']
  intro h
  rw [h] at nmem 
  exact nmem (Submodule.zero_mem (v.asIdeal ^ 2))
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
⊢ Associates.mk (Ideal.span {π}) ≠ 0
[PROOFSTEP]
rw [Associates.mk_ne_zero']
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
⊢ π ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
h : π = 0
⊢ False
[PROOFSTEP]
rw [h] at nmem 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬0 ∈ v.asIdeal ^ 2
h : π = 0
⊢ False
[PROOFSTEP]
exact nmem (Submodule.zero_mem (v.asIdeal ^ 2))
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ∃ π, intValuationDef v π = ↑(↑ofAdd (-1))
[PROOFSTEP]
use π
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ intValuationDef v π = ↑(↑ofAdd (-1))
[PROOFSTEP]
rw [intValuationDef, if_neg (Associates.mk_ne_zero'.mp hπ), WithZero.coe_inj]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ↑ofAdd (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))))) =
    ↑ofAdd (-1)
[PROOFSTEP]
apply congr_arg
[GOAL]
case h.h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ -↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))) = -1
[PROOFSTEP]
rw [neg_inj, ← Int.ofNat_one, Int.coe_nat_inj']
[GOAL]
case h.h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : ¬π ∈ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
[PROOFSTEP]
rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd_iff] at mem nmem 
[GOAL]
case h.h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : Associates.mk v.asIdeal ≤ Associates.mk (Ideal.span {π})
nmem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
[PROOFSTEP]
rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem 
[GOAL]
case h.h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : 1 ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))
nmem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
[PROOFSTEP]
rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at nmem 
[GOAL]
case h.h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : 1 ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))
nmem : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) < 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
[PROOFSTEP]
exact Nat.eq_of_le_of_lt_succ mem nmem
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : { x // x ∈ nonZeroDivisors R }
⊢ ↑(valuation v) (IsLocalization.mk' K r s) = ↑(intValuation v) r / ↑(intValuation v) ↑s
[PROOFSTEP]
erw [valuation_def, (IsLocalization.toLocalizationMap (nonZeroDivisors R) K).lift_mk', div_eq_mul_inv,
  mul_eq_mul_left_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : { x // x ∈ nonZeroDivisors R }
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑(intValuation v).toMonoidWithZeroHom) (nonZeroDivisors R))
                (_ : ∀ (s : { x // x ∈ nonZeroDivisors R }), IsUnit (↑↑(intValuation v).toMonoidWithZeroHom ↑s)))
            s)⁻¹ =
      (↑(intValuation v) ↑s)⁻¹ ∨
    ↑↑(intValuation v).toMonoidWithZeroHom r = 0
[PROOFSTEP]
left
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : { x // x ∈ nonZeroDivisors R }
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑(intValuation v).toMonoidWithZeroHom) (nonZeroDivisors R))
              (_ : ∀ (s : { x // x ∈ nonZeroDivisors R }), IsUnit (↑↑(intValuation v).toMonoidWithZeroHom ↑s)))
          s)⁻¹ =
    (↑(intValuation v) ↑s)⁻¹
[PROOFSTEP]
rw [Units.val_inv_eq_inv_val, inv_inj]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : { x // x ∈ nonZeroDivisors R }
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑(intValuation v).toMonoidWithZeroHom) (nonZeroDivisors R))
            (_ : ∀ (s : { x // x ∈ nonZeroDivisors R }), IsUnit (↑↑(intValuation v).toMonoidWithZeroHom ↑s)))
        s) =
    ↑(intValuation v) ↑s
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ ↑(valuation v) (↑(algebraMap R K) r) = ↑(intValuation v) r
[PROOFSTEP]
rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ ↑(valuation v) (↑(algebraMap R K) r) ≤ 1
[PROOFSTEP]
rw [valuation_of_algebraMap]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ ↑(intValuation v) r ≤ 1
[PROOFSTEP]
exact v.int_valuation_le_one r
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ ↑(valuation v) (↑(algebraMap R K) r) < 1 ↔ v.asIdeal ∣ Ideal.span {r}
[PROOFSTEP]
rw [valuation_of_algebraMap]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ ↑(intValuation v) r < 1 ↔ v.asIdeal ∣ Ideal.span {r}
[PROOFSTEP]
exact v.int_valuation_lt_one_iff_dvd r
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ∃ π, ↑(valuation v) π = ↑(↑ofAdd (-1))
[PROOFSTEP]
obtain ⟨r, hr⟩ := v.int_valuation_exists_uniformizer
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : intValuationDef v r = ↑(↑ofAdd (-1))
⊢ ∃ π, ↑(valuation v) π = ↑(↑ofAdd (-1))
[PROOFSTEP]
use algebraMap R K r
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : intValuationDef v r = ↑(↑ofAdd (-1))
⊢ ↑(valuation v) (↑(algebraMap R K) r) = ↑(↑ofAdd (-1))
[PROOFSTEP]
rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : intValuationDef v r = ↑(↑ofAdd (-1))
⊢ ↑(intValuation v) r = ↑(↑ofAdd (-1))
[PROOFSTEP]
exact hr
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : { x // x ∈ adicCompletionIntegers K v }
⊢ r • ↑x ∈ adicCompletionIntegers K v
[PROOFSTEP]
have h : (algebraMap R (adicCompletion K v)) r = (algebraMap R K r : adicCompletion K v) := rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : { x // x ∈ adicCompletionIntegers K v }
h : ↑(algebraMap R (adicCompletion K v)) r = ↑((fun x => K) r) (↑(algebraMap R K) r)
⊢ r • ↑x ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [Algebra.smul_def]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : { x // x ∈ adicCompletionIntegers K v }
h : ↑(algebraMap R (adicCompletion K v)) r = ↑((fun x => K) r) (↑(algebraMap R K) r)
⊢ ↑(algebraMap R (adicCompletion K v)) r * ↑x ∈ adicCompletionIntegers K v
[PROOFSTEP]
refine'
  ValuationSubring.mul_mem _ _ _ _
    x.2
      --Porting note: added instance
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : { x // x ∈ adicCompletionIntegers K v }
h : ↑(algebraMap R (adicCompletion K v)) r = ↑((fun x => K) r) (↑(algebraMap R K) r)
⊢ ↑(algebraMap R (adicCompletion K v)) r ∈ adicCompletionIntegers K v
[PROOFSTEP]
letI : Valued K ℤₘ₀ := adicValued v
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : { x // x ∈ adicCompletionIntegers K v }
h : ↑(algebraMap R (adicCompletion K v)) r = ↑((fun x => K) r) (↑(algebraMap R K) r)
this : Valued K ℤₘ₀ := adicValued v
⊢ ↑(algebraMap R (adicCompletion K v)) r ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, h, Valued.valuedCompletion_apply]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : { x // x ∈ adicCompletionIntegers K v }
h : ↑(algebraMap R (adicCompletion K v)) r = ↑((fun x => K) r) (↑(algebraMap R K) r)
this : Valued K ℤₘ₀ := adicValued v
⊢ ↑Valued.v (↑(algebraMap R K) r) ≤ 1
[PROOFSTEP]
exact v.valuation_le_one _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v
[PROOFSTEP]
letI : Valued K ℤₘ₀ := adicValued v
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
this : Valued K ℤₘ₀ := adicValued v
⊢ ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, Valued.valuedCompletion_apply]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
this : Valued K ℤₘ₀ := adicValued v
⊢ ↑Valued.v (↑(algebraMap R K) r) ≤ 1
[PROOFSTEP]
exact v.valuation_le_one _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (fun r =>
        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
          property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
      1 =
    1
[PROOFSTEP]
simp only [map_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ { val := ↑K 1, property := (_ : (fun x => x ∈ adicCompletionIntegers K v) (↑K 1)) } = 1
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
⊢ OneHom.toFun
      {
        toFun := fun r =>
          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
        map_one' :=
          (_ :
            (fun r =>
                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                    property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                1 =
              1) }
      (x * y) =
    OneHom.toFun
        {
          toFun := fun r =>
            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
          map_one' :=
            (_ :
              (fun r =>
                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                      property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                  1 =
                1) }
        x *
      OneHom.toFun
        {
          toFun := fun r =>
            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
          map_one' :=
            (_ :
              (fun r =>
                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                      property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                  1 =
                1) }
        y
[PROOFSTEP]
ext
  --Porting note: added instance
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
⊢ ↑(OneHom.toFun
        {
          toFun := fun r =>
            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
          map_one' :=
            (_ :
              (fun r =>
                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                      property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                  1 =
                1) }
        (x * y)) =
    ↑(OneHom.toFun
          {
            toFun := fun r =>
              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
            map_one' :=
              (_ :
                (fun r =>
                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                        property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                    1 =
                  1) }
          x *
        OneHom.toFun
          {
            toFun := fun r =>
              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
            map_one' :=
              (_ :
                (fun r =>
                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                        property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                    1 =
                  1) }
          y)
[PROOFSTEP]
letI : Valued K ℤₘ₀ := adicValued v
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
this : Valued K ℤₘ₀ := adicValued v
⊢ ↑(OneHom.toFun
        {
          toFun := fun r =>
            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
          map_one' :=
            (_ :
              (fun r =>
                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                      property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                  1 =
                1) }
        (x * y)) =
    ↑(OneHom.toFun
          {
            toFun := fun r =>
              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
            map_one' :=
              (_ :
                (fun r =>
                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                        property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                    1 =
                  1) }
          x *
        OneHom.toFun
          {
            toFun := fun r =>
              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
            map_one' :=
              (_ :
                (fun r =>
                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                        property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                    1 =
                  1) }
          y)
[PROOFSTEP]
simp_rw [RingHom.map_mul, Subring.coe_mul, UniformSpace.Completion.coe_mul]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun r =>
                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                  property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
              map_one' :=
                (_ :
                  (fun r =>
                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                          property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                      1 =
                    1) },
          map_mul' :=
            (_ :
              ∀ (x y : R),
                OneHom.toFun
                    {
                      toFun := fun r =>
                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                          property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                      map_one' :=
                        (_ :
                          (fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                              1 =
                            1) }
                    (x * y) =
                  OneHom.toFun
                      {
                        toFun := fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                        map_one' :=
                          (_ :
                            (fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                1 =
                              1) }
                      x *
                    OneHom.toFun
                      {
                        toFun := fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                        map_one' :=
                          (_ :
                            (fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                1 =
                              1) }
                      y) })
      0 =
    0
[PROOFSTEP]
simp only [map_zero]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ { val := ↑K 0, property := (_ : (fun x => x ∈ adicCompletionIntegers K v) (↑K 0)) } = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun r =>
                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                  property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
              map_one' :=
                (_ :
                  (fun r =>
                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                          property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                      1 =
                    1) },
          map_mul' :=
            (_ :
              ∀ (x y : R),
                OneHom.toFun
                    {
                      toFun := fun r =>
                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                          property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                      map_one' :=
                        (_ :
                          (fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                              1 =
                            1) }
                    (x * y) =
                  OneHom.toFun
                      {
                        toFun := fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                        map_one' :=
                          (_ :
                            (fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                1 =
                              1) }
                      x *
                    OneHom.toFun
                      {
                        toFun := fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                        map_one' :=
                          (_ :
                            (fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                1 =
                              1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun r =>
                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                    property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                map_one' :=
                  (_ :
                    (fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : R),
                  OneHom.toFun
                      {
                        toFun := fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                        map_one' :=
                          (_ :
                            (fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun r =>
                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                    property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                map_one' :=
                  (_ :
                    (fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : R),
                  OneHom.toFun
                      {
                        toFun := fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                        map_one' :=
                          (_ :
                            (fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        y) })
        y
[PROOFSTEP]
ext
  --Porting note: added instance
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
⊢ ↑(OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun r =>
                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                    property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                map_one' :=
                  (_ :
                    (fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : R),
                  OneHom.toFun
                      {
                        toFun := fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                        map_one' :=
                          (_ :
                            (fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        y) })
        (x + y)) =
    ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun r =>
                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                      property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                  map_one' :=
                    (_ :
                      (fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : R),
                    OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun r =>
                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                      property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                  map_one' :=
                    (_ :
                      (fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : R),
                    OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          y) })
          y)
[PROOFSTEP]
letI : Valued K ℤₘ₀ := adicValued v
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R
this : Valued K ℤₘ₀ := adicValued v
⊢ ↑(OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun r =>
                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                    property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                map_one' :=
                  (_ :
                    (fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : R),
                  OneHom.toFun
                      {
                        toFun := fun r =>
                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                            property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                        map_one' :=
                          (_ :
                            (fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        y) })
        (x + y)) =
    ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun r =>
                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                      property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                  map_one' :=
                    (_ :
                      (fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : R),
                    OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun r =>
                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                      property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                  map_one' :=
                    (_ :
                      (fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : R),
                    OneHom.toFun
                        {
                          toFun := fun r =>
                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                              property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                          map_one' :=
                            (_ :
                              (fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          y) })
          y)
[PROOFSTEP]
simp_rw [RingHom.map_add, Subring.coe_add, UniformSpace.Completion.coe_add]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : (fun x => { x // x ∈ adicCompletionIntegers K v }) r
⊢ ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  {
                    toFun := fun r =>
                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                        property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                    map_one' :=
                      (_ :
                        (fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                            1 =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : R),
                      OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) }
                            y) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : R),
                              OneHom.toFun
                                  {
                                    toFun := fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                    map_one' :=
                                      (_ :
                                        (fun r =>
                                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                property :=
                                                  (_ :
                                                    ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                      adicCompletionIntegers K v) })
                                            1 =
                                          1) }
                                  (x * y) =
                                OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    x *
                                  OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    y) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : R),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : R),
                                OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : R),
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        y) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : R),
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        y) })
                        y) }
        r *
      x =
    x *
      ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  {
                    toFun := fun r =>
                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                        property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                    map_one' :=
                      (_ :
                        (fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                            1 =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : R),
                      OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) }
                            y) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : R),
                              OneHom.toFun
                                  {
                                    toFun := fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                    map_one' :=
                                      (_ :
                                        (fun r =>
                                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                property :=
                                                  (_ :
                                                    ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                      adicCompletionIntegers K v) })
                                            1 =
                                          1) }
                                  (x * y) =
                                OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    x *
                                  OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    y) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : R),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : R),
                                OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : R),
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        y) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : R),
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        y) })
                        y) }
        r
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : (fun x => { x // x ∈ adicCompletionIntegers K v }) r
⊢ { val := ↑K (↑(algebraMap R K) r), property := (_ : ↑Valued.v (↑K (↑(algebraMap R K) r)) ≤ 1) } * x =
    x * { val := ↑K (↑(algebraMap R K) r), property := (_ : ↑Valued.v (↑K (↑(algebraMap R K) r)) ≤ 1) }
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : (fun x => { x // x ∈ adicCompletionIntegers K v }) r
⊢ r • x =
    ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  {
                    toFun := fun r =>
                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                        property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                    map_one' :=
                      (_ :
                        (fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                            1 =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : R),
                      OneHom.toFun
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) }
                            y) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          {
                            toFun := fun r =>
                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                property :=
                                  (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                            map_one' :=
                              (_ :
                                (fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                    1 =
                                  1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : R),
                              OneHom.toFun
                                  {
                                    toFun := fun r =>
                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                        property :=
                                          (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                    map_one' :=
                                      (_ :
                                        (fun r =>
                                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                property :=
                                                  (_ :
                                                    ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                      adicCompletionIntegers K v) })
                                            1 =
                                          1) }
                                  (x * y) =
                                OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    x *
                                  OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    y) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : R),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : R),
                                OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : R),
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        y) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : R),
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        y) })
                        y) }
        r *
      x
[PROOFSTEP]
ext
  --Porting note: added `dsimp`
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : (fun x => { x // x ∈ adicCompletionIntegers K v }) r
⊢ ↑(r • x) =
    ↑(↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    {
                      toFun := fun r =>
                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                          property := (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                      map_one' :=
                        (_ :
                          (fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                              1 =
                            1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : R),
                        OneHom.toFun
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) }
                            (x * y) =
                          OneHom.toFun
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) }
                              x *
                            OneHom.toFun
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) }
                              y) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun r =>
                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                  property :=
                                    (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                              map_one' :=
                                (_ :
                                  (fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                      1 =
                                    1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : R),
                                OneHom.toFun
                                    {
                                      toFun := fun r =>
                                        { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                          property :=
                                            (_ :
                                              ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                      map_one' :=
                                        (_ :
                                          (fun r =>
                                                { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                  property :=
                                                    (_ :
                                                      ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                        adicCompletionIntegers K v) })
                                              1 =
                                            1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      y) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : R),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun r =>
                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                    property :=
                                      (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                map_one' :=
                                  (_ :
                                    (fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) })
                                        1 =
                                      1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : R),
                                  OneHom.toFun
                                      {
                                        toFun := fun r =>
                                          { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                            property :=
                                              (_ :
                                                ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                        map_one' :=
                                          (_ :
                                            (fun r =>
                                                  { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                    property :=
                                                      (_ :
                                                        ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                          adicCompletionIntegers K v) })
                                                1 =
                                              1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        y) })
                        (x + y) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                  map_one' :=
                                    (_ :
                                      (fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) })
                                          1 =
                                        1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : R),
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun r =>
                                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                property :=
                                                  (_ :
                                                    ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                      adicCompletionIntegers K v) },
                                            map_one' :=
                                              (_ :
                                                (fun r =>
                                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                        property :=
                                                          (_ :
                                                            ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                              adicCompletionIntegers K v) })
                                                    1 =
                                                  1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun r =>
                                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                property :=
                                                  (_ :
                                                    ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                      adicCompletionIntegers K v) },
                                            map_one' :=
                                              (_ :
                                                (fun r =>
                                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                        property :=
                                                          (_ :
                                                            ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                              adicCompletionIntegers K v) })
                                                    1 =
                                                  1) }
                                          y) })
                          x +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun r =>
                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                      property :=
                                        (_ : ↑((fun x => K) r) (↑(algebraMap R K) r) ∈ adicCompletionIntegers K v) },
                                  map_one' :=
                                    (_ :
                                      (fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) })
                                          1 =
                                        1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : R),
                                    OneHom.toFun
                                        {
                                          toFun := fun r =>
                                            { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                              property :=
                                                (_ :
                                                  ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                    adicCompletionIntegers K v) },
                                          map_one' :=
                                            (_ :
                                              (fun r =>
                                                    { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                      property :=
                                                        (_ :
                                                          ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                            adicCompletionIntegers K v) })
                                                  1 =
                                                1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun r =>
                                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                property :=
                                                  (_ :
                                                    ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                      adicCompletionIntegers K v) },
                                            map_one' :=
                                              (_ :
                                                (fun r =>
                                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                        property :=
                                                          (_ :
                                                            ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                              adicCompletionIntegers K v) })
                                                    1 =
                                                  1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun r =>
                                              { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                property :=
                                                  (_ :
                                                    ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                      adicCompletionIntegers K v) },
                                            map_one' :=
                                              (_ :
                                                (fun r =>
                                                      { val := ↑((fun x => K) r) (↑(algebraMap R K) r),
                                                        property :=
                                                          (_ :
                                                            ↑((fun x => K) r) (↑(algebraMap R K) r) ∈
                                                              adicCompletionIntegers K v) })
                                                    1 =
                                                  1) }
                                          y) })
                          y) }
          r *
        x)
[PROOFSTEP]
dsimp
  --Porting note: added instance
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : (fun x => { x // x ∈ adicCompletionIntegers K v }) r
⊢ ↑(r • x) = ↑K (↑(algebraMap R K) r) * ↑x
[PROOFSTEP]
letI : Valued K ℤₘ₀ := adicValued v
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : (fun x => { x // x ∈ adicCompletionIntegers K v }) r
this : Valued K ℤₘ₀ := adicValued v
⊢ ↑(r • x) = ↑K (↑(algebraMap R K) r) * ↑x
[PROOFSTEP]
simp only [Subring.coe_mul, Algebra.smul_def]
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : (fun x => { x // x ∈ adicCompletionIntegers K v }) r
this : Valued K ℤₘ₀ := adicValued v
⊢ ↑(r • x) = ↑K (↑(algebraMap R K) r) * ↑x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
c : R
x : { x // x ∈ adicCompletionIntegers K v }
hcx : c • x = 0
⊢ c = 0 ∨ x = 0
[PROOFSTEP]
rw [Algebra.smul_def, mul_eq_zero] at hcx 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
c : R
x : { x // x ∈ adicCompletionIntegers K v }
hcx : ↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) c = 0 ∨ x = 0
⊢ c = 0 ∨ x = 0
[PROOFSTEP]
refine' hcx.imp_left fun hc => _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
c : R
x : { x // x ∈ adicCompletionIntegers K v }
hcx : ↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) c = 0 ∨ x = 0
hc : ↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) c = 0
⊢ c = 0
[PROOFSTEP]
letI : UniformSpace K := v.adicValued.toUniformSpace
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
c : R
x : { x // x ∈ adicCompletionIntegers K v }
hcx : ↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) c = 0 ∨ x = 0
hc : ↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) c = 0
this : UniformSpace K := Valued.toUniformSpace
⊢ c = 0
[PROOFSTEP]
rw [← map_zero (algebraMap R (v.adicCompletionIntegers K))] at hc 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
c : R
x : { x // x ∈ adicCompletionIntegers K v }
hcx : ↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) c = 0 ∨ x = 0
hc :
  ↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) c = ↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) 0
this : UniformSpace K := Valued.toUniformSpace
⊢ c = 0
[PROOFSTEP]
exact IsFractionRing.injective R K (UniformSpace.Completion.coe_injective K (Subtype.ext_iff.mp hc))
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
y : { x // x ∈ adicCompletionIntegers K v }
z : adicCompletion K v
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
simp only [Algebra.smul_def]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
y : { x // x ∈ adicCompletionIntegers K v }
z : adicCompletion K v
⊢ ↑(algebraMap { x // x ∈ adicCompletionIntegers K v } (adicCompletion K v))
        (↑(algebraMap R { x // x ∈ adicCompletionIntegers K v }) x * y) *
      z =
    ↑(algebraMap R (adicCompletion K v)) x *
      (↑(algebraMap { x // x ∈ adicCompletionIntegers K v } (adicCompletion K v)) y * z)
[PROOFSTEP]
apply mul_assoc
