-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem algebraMap' (k : K) : (algebraMap K (K_hat R K) 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
k : K
⊢ ((algebraMap K (K_hat R K)) k).IsFiniteAdele

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
k : K
⊢ {x | (algebraMap K (K_hat R K)) k x ∉ adicCompletionIntegers K x}.Finite

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
k : K
⊢ {v | 1 < (valuation K v) k}.Finite

Tactic:
obtain ⟨⟨n, ⟨d, hd⟩⟩, hk⟩ := IsLocalization.surj (nonZeroDivisors R) k

Result:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
⊢ {v | 1 < (valuation K v) k}.Finite

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 1 < v.intValuation n

Tactic:
rw [← hk, mul_comm]

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 1 < v.intValuation d * (valuation K v) k

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
hk : (valuation K v) k * v.intValuation d = v.intValuation n
⊢ v ∈ {v | (valuation K v) ↑d < 1}

Tactic:
rw [mem_setOf_eq, valuation_of_algebraMap]

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
hk : (valuation K v) k * v.intValuation d = v.intValuation n
⊢ v.intValuation d < 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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 0 ≤ (valuation K v) k

Tactic:
simp

Result:
no goals

Proof state:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | 1 < (valuation K v) k}.Finite

Tactic:
suffices {v : HeightOneSpectrum R | v.valuation K d < 1}.Finite by
  apply Finite.subset this
  intro v hv
  apply_fun v.valuation K at hk
  simp only [Valuation.map_mul, valuation_of_algebraMap] at hk
  rw [mem_setOf_eq, valuation_of_algebraMap]
  have := intValuation_le_one v n
  contrapose! this
  change 1 < v.intValuation n
  rw [← hk, mul_comm]
  exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <|
    mul_le_mul_of_nonneg_right this (by simp)

Result:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | (valuation K v) ↑d < 1}.Finite

Proof state:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | (valuation K v) ↑d < 1}.Finite

Tactic:
simp_rw [valuation_of_algebraMap]

Result:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | v.intValuation d < 1}.Finite

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 0 < 1

Tactic:
simp

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
this : {v | (valuation K v) ↑d < 1}.Finite
⊢ {v | 1 < (valuation K v) k} ⊆ {v | (valuation K v) ↑d < 1}

Tactic:
intro v hv

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
this : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
⊢ v ∈ {v | (valuation K v) ↑d < 1}

Proof state:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | v.intValuation d < 1}.Finite

Tactic:
change {v : HeightOneSpectrum R | v.intValuationDef d < 1}.Finite

Result:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | v.intValuationDef d < 1}.Finite

Proof state:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | v.intValuationDef d < 1}.Finite

Tactic:
simp_rw [intValuation_lt_one_iff_dvd]

Result:
case intro.mk.mk
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | v.asIdeal ∣ Ideal.span {d}}.Finite