-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem algebraMap' (k : K) : (algebraMap K (K_hat R K) k).IsFiniteAdele

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

Tactic:
have hd' : d ≠ 0 := nonZeroDivisors.ne_zero hd

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 | 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
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}.Finite

Tactic:
apply Finite.subset this

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

Tactic:
change {v : HeightOneSpectrum R | 1 < v.valuation K k}.Finite

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
⊢ {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 * (algebraMap R K) ↑(n, ⟨d, hd⟩).2) = (valuation K v) ((algebraMap R K) (n, ⟨d, hd⟩).1)
⊢ v ∈ {v | (valuation K v) ↑d < 1}

Tactic:
simp only [Valuation.map_mul, valuation_of_algebraMap] at hk

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 ∈ {v | (valuation K v) ↑d < 1}

Proof state:
case intro.mk.mk.hI
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
⊢ Ideal.span {d} ≠ 0

Tactic:
simpa only [Submodule.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot]

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
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.intValuationDef n

Tactic:
change 1 < v.intValuation n

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 n

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 : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
⊢ v ∈ {v | (valuation K v) ↑d < 1}

Tactic:
apply_fun v.valuation K at hk

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 * (algebraMap R K) ↑(n, ⟨d, hd⟩).2) = (valuation K v) ((algebraMap R K) (n, ⟨d, hd⟩).1)
⊢ v ∈ {v | (valuation K v) ↑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
⊢ 1 < v.intValuation d * (valuation K v) k

Tactic:
exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <|
  mul_le_mul_of_nonneg_right this (by 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
⊢ {x | (algebraMap K (K_hat R K)) k x ∉ adicCompletionIntegers K x}.Finite

Tactic:
simp_rw [mem_adicCompletionIntegers, ProdAdicCompletions.algebraMap_apply',
  adicCompletion, Valued.valuedCompletion_apply, not_le]

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 | 1 < Valued.v k}.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.asIdeal ∣ Ideal.span {d}}.Finite

Tactic:
apply Ideal.finite_factors

Result:
case intro.mk.mk.hI
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
⊢ Ideal.span {d} ≠ 0

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.intValuation d < 1

Tactic:
have := intValuation_le_one v n

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 : v.intValuationDef n ≤ 1
⊢ v.intValuation d < 1