-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem zero : (0 : K_hat R K).IsFiniteAdele

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
h_zero : Valued.v 0 = 0
⊢ Valued.v 0 ≤ 1

Tactic:
rw [h_zero]

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
h_zero : Valued.v 0 = 0
⊢ 0 ≤ 1

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
⊢ 0 ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers]

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
⊢ Valued.v 0 ≤ 1

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
⊢ Valued.v 0 ≤ 1

Tactic:
have h_zero : (Valued.v (0 : v.adicCompletion K) : WithZero (Multiplicative ℤ)) = 0 :=
  Valued.v.map_zero'

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
h_zero : Valued.v 0 = 0
⊢ Valued.v 0 ≤ 1

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ v ∉ {v | 0 ∉ adicCompletionIntegers K v}

Tactic:
intro hv

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : v ∈ {v | 0 ∉ adicCompletionIntegers K v}
⊢ False

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h_empty : {v | 0 ∉ adicCompletionIntegers K v} = ∅
⊢ {x | 0 x ∉ adicCompletionIntegers K x}.Finite

Tactic:
convert finite_empty

Result:
no goals

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ v ∈ {v | 0 ∉ adicCompletionIntegers K v} ↔ v ∈ ∅

Tactic:
rw [mem_empty_iff_false, iff_false]

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ v ∉ {v | 0 ∉ adicCompletionIntegers K v}

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ {x | 0 x ∉ adicCompletionIntegers K x}.Finite

Tactic:
have h_empty :
  {v : HeightOneSpectrum R | ¬(0 : v.adicCompletion K) ∈ v.adicCompletionIntegers K} = ∅ := by
  ext v; rw [mem_empty_iff_false, iff_false]; 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' _

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
h_empty : {v | 0 ∉ adicCompletionIntegers K v} = ∅
⊢ {x | 0 x ∉ adicCompletionIntegers K x}.Finite

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
⊢ False

Tactic:
apply hv

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
⊢ 0 ∈ adicCompletionIntegers K v

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
h_zero : Valued.v 0 = 0
⊢ 0 ≤ 1

Tactic:
exact zero_le_one' _

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsFiniteAdele 0

Tactic:
rw [IsFiniteAdele, Filter.eventually_cofinite]

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ {x | 0 x ∉ adicCompletionIntegers K x}.Finite

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : v ∈ {v | 0 ∉ adicCompletionIntegers K v}
⊢ False

Tactic:
rw [mem_setOf] at hv

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
hv : 0 ∉ adicCompletionIntegers K v
⊢ False

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ {v | 0 ∉ adicCompletionIntegers K v} = ∅

Tactic:
ext v

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ v ∈ {v | 0 ∉ adicCompletionIntegers K v} ↔ v ∈ ∅