-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem add {x y : K_hat R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) :
    (x + y).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
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | (x + y) v ∉ adicCompletionIntegers K v}
⊢ x v ∉ adicCompletionIntegers K v ∨ y v ∉ adicCompletionIntegers K v

Tactic:
rw [mem_setOf] at 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
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : (x + y) v ∉ adicCompletionIntegers K v
⊢ x v ∉ adicCompletionIntegers K v ∨ y v ∉ 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 y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : Valued.v (x v) ⊔ Valued.v (y v) ≤ 1
⊢ Valued.v (x v + y v) ≤ 1

Tactic:
exact le_trans (Valued.v.map_add_le_max' (x v) (y v)) hv

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
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
⊢ {v | (x + y) v ∉ adicCompletionIntegers K v} ⊆
    {v | x v ∉ adicCompletionIntegers K v} ∪ {v | y v ∉ adicCompletionIntegers K v}

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
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
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}

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 y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : x v ∈ adicCompletionIntegers K v ∧ y v ∈ adicCompletionIntegers K v
⊢ (x + y) v ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, ← max_le_iff] at 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
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : Valued.v (x v) ⊔ Valued.v (y v) ≤ 1
⊢ (x + y) v ∈ 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 y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
h_subset :
  {v | (x + y) v ∉ adicCompletionIntegers K v} ⊆
    {v | x v ∉ adicCompletionIntegers K v} ∪ {v | y v ∉ adicCompletionIntegers K v}
⊢ {x_1 | (x + y) x_1 ∉ adicCompletionIntegers K x_1}.Finite

Tactic:
exact (hx.union hy).subset h_subset

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
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
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}

Tactic:
rw [mem_union, mem_setOf, mem_setOf]

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 y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | (x + y) v ∉ adicCompletionIntegers K v}
⊢ x v ∉ adicCompletionIntegers K v ∨ y v ∉ 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 y : K_hat R K
hx : x.IsFiniteAdele
hy : y.IsFiniteAdele
⊢ (x + y).IsFiniteAdele

Tactic:
rw [IsFiniteAdele, Filter.eventually_cofinite] at hx hy ⊢

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 y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
⊢ {x_1 | (x + y) x_1 ∉ adicCompletionIntegers K x_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
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : (x + y) v ∉ adicCompletionIntegers K v
⊢ x v ∉ adicCompletionIntegers K v ∨ y v ∉ adicCompletionIntegers K v

Tactic:
contrapose! 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
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : x v ∈ adicCompletionIntegers K v ∧ y v ∈ adicCompletionIntegers K v
⊢ (x + y) v ∈ 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 y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
⊢ {x_1 | (x + y) x_1 ∉ adicCompletionIntegers K x_1}.Finite

Tactic:
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

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 y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
h_subset :
  {v | (x + y) v ∉ adicCompletionIntegers K v} ⊆
    {v | x v ∉ adicCompletionIntegers K v} ∪ {v | y v ∉ adicCompletionIntegers K v}
⊢ {x_1 | (x + y) x_1 ∉ adicCompletionIntegers K x_1}.Finite