[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : R_hat R K
⊢ ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) }
      (x + y) =
    ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) } x +
      ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) } y
[PROOFSTEP]
refine funext fun v => ?_
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : R_hat R K
v : HeightOneSpectrum R
⊢ ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) } (x + y)
      v =
    (ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) } x +
        ZeroHom.toFun { toFun := fun x v => ↑(x v), map_zero' := (_ : (fun x v => ↑(x v)) 0 = (fun x v => ↑(x v)) 0) }
          y)
      v
[PROOFSTEP]
simp only [coe_apply, Pi.add_apply, Subring.coe_add]
  -- Porting note: added
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : R_hat R K
v : HeightOneSpectrum R
⊢ ↑((x + y) v) = ((fun v => ↑(x v)) + fun v => ↑(y v)) v
[PROOFSTEP]
erw [Pi.add_apply, Pi.add_apply, Subring.coe_add]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
src✝ : R_hat R K →+ K_hat R K := addMonoidHom R K
x y : R_hat R K
⊢ OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } (x * y) =
    OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } x *
      OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } y
[PROOFSTEP]
refine funext fun p => ?_
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
src✝ : R_hat R K →+ K_hat R K := addMonoidHom R K
x y : R_hat R K
p : HeightOneSpectrum R
⊢ OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } (x * y)
      p =
    (OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } x *
        OneHom.toFun { toFun := fun x v => ↑(x v), map_one' := (_ : (fun x v => ↑(x v)) 1 = (fun x v => ↑(x v)) 1) } y)
      p
[PROOFSTEP]
simp only [Pi.mul_apply, Subring.coe_mul]
  -- Porting note: added
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
src✝ : R_hat R K →+ K_hat R K := addMonoidHom R K
x y : R_hat R K
p : HeightOneSpectrum R
⊢ ↑((x * y) p) = ((fun v => ↑(x v)) * fun v => ↑(y v)) p
[PROOFSTEP]
erw [Pi.mul_apply, Pi.mul_apply, Subring.coe_mul]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Algebra K ((v : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K v)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Algebra R ((v : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K v)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsScalarTower R K ((v : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K v)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Algebra R ((v : HeightOneSpectrum R) → { x // x ∈ adicCompletionIntegers K v })
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsScalarTower R ((v : HeightOneSpectrum R) → { x // x ∈ adicCompletionIntegers K v })
    ((v : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K v)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : IsFiniteAdele x
hy : IsFiniteAdele y
⊢ IsFiniteAdele (x + y)
[PROOFSTEP]
rw [IsFiniteAdele, Filter.eventually_cofinite] at hx hy ⊢
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
⊢ Set.Finite {x_1 | ¬(x + y) x_1 ∈ adicCompletionIntegers K x_1}
[PROOFSTEP]
have h_subset :
  {v : HeightOneSpectrum R | ¬(x + y) v ∈ v.adicCompletionIntegers K} ⊆
    {v : HeightOneSpectrum R | ¬x v ∈ v.adicCompletionIntegers K} ∪
      {v : HeightOneSpectrum R | ¬y v ∈ v.adicCompletionIntegers K} :=
  by
  intro v hv
  rw [mem_union, mem_setOf, mem_setOf]
  rw [mem_setOf] at hv 
  contrapose! hv
  rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, ← max_le_iff] at hv 
  rw [mem_adicCompletionIntegers, Pi.add_apply]
  exact le_trans (Valued.v.map_add_le_max' (x v) (y v)) hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
⊢ {v | ¬(x + y) v ∈ adicCompletionIntegers K v} ⊆
    {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
[PROOFSTEP]
intro v hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : v ∈ {v | ¬(x + y) v ∈ adicCompletionIntegers K v}
⊢ v ∈ {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
[PROOFSTEP]
rw [mem_union, mem_setOf, mem_setOf]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : v ∈ {v | ¬(x + y) v ∈ adicCompletionIntegers K v}
⊢ ¬x v ∈ adicCompletionIntegers K v ∨ ¬y v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_setOf] at hv 
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ¬(x + y) v ∈ adicCompletionIntegers K v
⊢ ¬x v ∈ adicCompletionIntegers K v ∨ ¬y v ∈ adicCompletionIntegers K v
[PROOFSTEP]
contrapose! hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : x v ∈ adicCompletionIntegers K v ∧ y v ∈ adicCompletionIntegers K v
⊢ (x + y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, ← max_le_iff] at hv 
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : max (↑Valued.v (x v)) (↑Valued.v (y v)) ≤ 1
⊢ (x + y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, Pi.add_apply]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : max (↑Valued.v (x v)) (↑Valued.v (y v)) ≤ 1
⊢ ↑Valued.v (x v + y v) ≤ 1
[PROOFSTEP]
exact le_trans (Valued.v.map_add_le_max' (x v) (y v)) hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
h_subset :
  {v | ¬(x + y) v ∈ adicCompletionIntegers K v} ⊆
    {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
⊢ Set.Finite {x_1 | ¬(x + y) x_1 ∈ adicCompletionIntegers K x_1}
[PROOFSTEP]
exact (hx.union hy).subset h_subset
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsFiniteAdele 0
[PROOFSTEP]
rw [IsFiniteAdele, Filter.eventually_cofinite]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Set.Finite {x | ¬OfNat.ofNat 0 x ∈ adicCompletionIntegers K x}
[PROOFSTEP]
have h_empty : {v : HeightOneSpectrum R | ¬(0 : v.adicCompletion K) ∈ v.adicCompletionIntegers K} = ∅ :=
  by
  ext v; rw [mem_empty_iff_false, iff_false_iff]; intro hv
  rw [mem_setOf] at hv ; apply hv; rw [mem_adicCompletionIntegers]
  have h_zero : (Valued.v (0 : v.adicCompletion K) : WithZero (Multiplicative ℤ)) = 0 := Valued.v.map_zero'
  rw [h_zero];
  exact
    zero_le_one'
      _
        -- Porting note: was `exact`, but `OfNat` got in the way.
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ {v | ¬0 ∈ adicCompletionIntegers K v} = ∅
[PROOFSTEP]
ext v
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
⊢ v ∈ {v | ¬0 ∈ adicCompletionIntegers K v} ↔ v ∈ ∅
[PROOFSTEP]
rw [mem_empty_iff_false, iff_false_iff]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
⊢ ¬v ∈ {v | ¬0 ∈ adicCompletionIntegers K v}
[PROOFSTEP]
intro hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : v ∈ {v | ¬0 ∈ adicCompletionIntegers K v}
⊢ False
[PROOFSTEP]
rw [mem_setOf] at hv 
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
⊢ False
[PROOFSTEP]
apply hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
⊢ 0 ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
⊢ ↑Valued.v 0 ≤ 1
[PROOFSTEP]
have h_zero : (Valued.v (0 : v.adicCompletion K) : WithZero (Multiplicative ℤ)) = 0 := Valued.v.map_zero'
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
h_zero : ↑Valued.v 0 = 0
⊢ ↑Valued.v 0 ≤ 1
[PROOFSTEP]
rw [h_zero]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬0 ∈ adicCompletionIntegers K v
h_zero : ↑Valued.v 0 = 0
⊢ 0 ≤ 1
[PROOFSTEP]
exact
  zero_le_one'
    _
      -- Porting note: was `exact`, but `OfNat` got in the way.
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
h_empty : {v | ¬0 ∈ adicCompletionIntegers K v} = ∅
⊢ Set.Finite {x | ¬OfNat.ofNat 0 x ∈ adicCompletionIntegers K x}
[PROOFSTEP]
convert finite_empty
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K_hat R K
hx : IsFiniteAdele x
⊢ IsFiniteAdele (-x)
[PROOFSTEP]
rw [IsFiniteAdele] at hx ⊢
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
have h : ∀ v : HeightOneSpectrum R, -x v ∈ v.adicCompletionIntegers K ↔ x v ∈ v.adicCompletionIntegers K :=
  by
  intro v
  rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, Valuation.map_neg]
    -- Porting note: was `simpa only [Pi.neg_apply, h] using hx` but `Pi.neg_apply` no longer works
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
⊢ ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
[PROOFSTEP]
intro v
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
v : HeightOneSpectrum R
⊢ -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, Valuation.map_neg]
  -- Porting note: was `simpa only [Pi.neg_apply, h] using hx` but `Pi.neg_apply` no longer works
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
convert hx using 2 with v
[GOAL]
case h.e'_2.h.a
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
v : HeightOneSpectrum R
⊢ (-x) v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
[PROOFSTEP]
convert h v
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : IsFiniteAdele x
hy : IsFiniteAdele y
⊢ IsFiniteAdele (x * y)
[PROOFSTEP]
rw [IsFiniteAdele, Filter.eventually_cofinite] at hx hy ⊢
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
⊢ Set.Finite {x_1 | ¬(x * y) x_1 ∈ adicCompletionIntegers K x_1}
[PROOFSTEP]
have h_subset :
  {v : HeightOneSpectrum R | ¬(x * y) v ∈ v.adicCompletionIntegers K} ⊆
    {v : HeightOneSpectrum R | ¬x v ∈ v.adicCompletionIntegers K} ∪
      {v : HeightOneSpectrum R | ¬y v ∈ v.adicCompletionIntegers K} :=
  by
  intro v hv
  rw [mem_union, mem_setOf, mem_setOf]
  rw [mem_setOf] at hv 
  contrapose! hv
  rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers] at hv 
  have h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v) := Valued.v.map_mul' (x v) (y v)
  rw [mem_adicCompletionIntegers, Pi.mul_apply, h_mul]
  exact @mul_le_one' (WithZero (Multiplicative ℤ)) _ _ (OrderedCommMonoid.to_covariantClass_left _) _ _ hv.left hv.right
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
⊢ {v | ¬(x * y) v ∈ adicCompletionIntegers K v} ⊆
    {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
[PROOFSTEP]
intro v hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : v ∈ {v | ¬(x * y) v ∈ adicCompletionIntegers K v}
⊢ v ∈ {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
[PROOFSTEP]
rw [mem_union, mem_setOf, mem_setOf]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : v ∈ {v | ¬(x * y) v ∈ adicCompletionIntegers K v}
⊢ ¬x v ∈ adicCompletionIntegers K v ∨ ¬y v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_setOf] at hv 
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ¬(x * y) v ∈ adicCompletionIntegers K v
⊢ ¬x v ∈ adicCompletionIntegers K v ∨ ¬y v ∈ adicCompletionIntegers K v
[PROOFSTEP]
contrapose! hv
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : x v ∈ adicCompletionIntegers K v ∧ y v ∈ adicCompletionIntegers K v
⊢ (x * y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers] at hv 
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ↑Valued.v (x v) ≤ 1 ∧ ↑Valued.v (y v) ≤ 1
⊢ (x * y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
have h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v) := Valued.v.map_mul' (x v) (y v)
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ↑Valued.v (x v) ≤ 1 ∧ ↑Valued.v (y v) ≤ 1
h_mul : ↑Valued.v (x v * y v) = ↑Valued.v (x v) * ↑Valued.v (y v)
⊢ (x * y) v ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers, Pi.mul_apply, h_mul]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
v : HeightOneSpectrum R
hv : ↑Valued.v (x v) ≤ 1 ∧ ↑Valued.v (y v) ≤ 1
h_mul : ↑Valued.v (x v * y v) = ↑Valued.v (x v) * ↑Valued.v (y v)
⊢ ↑Valued.v (x v) * ↑Valued.v (y v) ≤ 1
[PROOFSTEP]
exact @mul_le_one' (WithZero (Multiplicative ℤ)) _ _ (OrderedCommMonoid.to_covariantClass_left _) _ _ hv.left hv.right
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K_hat R K
hx : Set.Finite {x_1 | ¬x x_1 ∈ adicCompletionIntegers K x_1}
hy : Set.Finite {x | ¬y x ∈ adicCompletionIntegers K x}
h_subset :
  {v | ¬(x * y) v ∈ adicCompletionIntegers K v} ⊆
    {v | ¬x v ∈ adicCompletionIntegers K v} ∪ {v | ¬y v ∈ adicCompletionIntegers K v}
⊢ Set.Finite {x_1 | ¬(x * y) x_1 ∈ adicCompletionIntegers K x_1}
[PROOFSTEP]
exact (hx.union hy).subset h_subset
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsFiniteAdele 1
[PROOFSTEP]
rw [IsFiniteAdele, Filter.eventually_cofinite]
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Set.Finite {x | ¬OfNat.ofNat 1 x ∈ adicCompletionIntegers K x}
[PROOFSTEP]
have h_empty : {v : HeightOneSpectrum R | ¬(1 : v.adicCompletion K) ∈ v.adicCompletionIntegers K} = ∅ :=
  by
  ext v; rw [mem_empty_iff_false, iff_false_iff]; intro hv
  rw [mem_setOf] at hv ; apply hv; rw [mem_adicCompletionIntegers]
  exact le_of_eq Valued.v.map_one'
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ {v | ¬1 ∈ adicCompletionIntegers K v} = ∅
[PROOFSTEP]
ext v
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
⊢ v ∈ {v | ¬1 ∈ adicCompletionIntegers K v} ↔ v ∈ ∅
[PROOFSTEP]
rw [mem_empty_iff_false, iff_false_iff]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
⊢ ¬v ∈ {v | ¬1 ∈ adicCompletionIntegers K v}
[PROOFSTEP]
intro hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : v ∈ {v | ¬1 ∈ adicCompletionIntegers K v}
⊢ False
[PROOFSTEP]
rw [mem_setOf] at hv 
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬1 ∈ adicCompletionIntegers K v
⊢ False
[PROOFSTEP]
apply hv
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬1 ∈ adicCompletionIntegers K v
⊢ 1 ∈ adicCompletionIntegers K v
[PROOFSTEP]
rw [mem_adicCompletionIntegers]
[GOAL]
case h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ v : HeightOneSpectrum R
hv : ¬1 ∈ adicCompletionIntegers K v
⊢ ↑Valued.v 1 ≤ 1
[PROOFSTEP]
exact le_of_eq Valued.v.map_one'
[GOAL]
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
h_empty : {v | ¬1 ∈ adicCompletionIntegers K v} = ∅
⊢ Set.Finite {x | ¬OfNat.ofNat 1 x ∈ adicCompletionIntegers K x}
[PROOFSTEP]
convert finite_empty
