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

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 | 1 ∉ adicCompletionIntegers K v} = ∅
⊢ {x | 1 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
hv : 1 ∉ 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 : 1 ∉ adicCompletionIntegers K v
⊢ 1 ∈ 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
⊢ {v | 1 ∉ 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 | 1 ∉ adicCompletionIntegers K v} ↔ 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
⊢ v ∉ {v | 1 ∉ 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 | 1 ∉ adicCompletionIntegers K v}
⊢ False

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 : 1 ∉ adicCompletionIntegers K v
⊢ Valued.v 1 ≤ 1

Tactic:
exact le_of_eq Valued.v.map_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 1

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 | 1 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 : 1 ∉ adicCompletionIntegers K v
⊢ 1 ∈ 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 : 1 ∉ adicCompletionIntegers K v
⊢ Valued.v 1 ≤ 1

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 | 1 x ∉ adicCompletionIntegers K x}.Finite

Tactic:
have h_empty :
  {v : HeightOneSpectrum R | ¬(1 : 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]
  exact le_of_eq Valued.v.map_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 | 1 ∉ adicCompletionIntegers K v} = ∅
⊢ {x | 1 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 | 1 ∉ 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 : 1 ∉ adicCompletionIntegers K v
⊢ False

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 | 1 ∉ 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 | 1 ∉ adicCompletionIntegers K v}