-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem mul {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}
⊢ 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_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
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}
⊢ 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 : x v ∈ adicCompletionIntegers K v ∧ y v ∈ adicCompletionIntegers K v
⊢ (x * y) v ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers] 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) ≤ 1 ∧ 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
v : HeightOneSpectrum R
hv : Valued.v (x v) ≤ 1 ∧ Valued.v (y v) ≤ 1
⊢ (x * y) v ∈ adicCompletionIntegers K v

Tactic:
have h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v) :=
  Valued.v.map_mul' (x v) (y v)

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) ≤ 1 ∧ Valued.v (y v) ≤ 1
h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y 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] at hv
  have h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v) :=
    Valued.v.map_mul' (x v) (y v)
  rw [mem_adicCompletionIntegers, Pi.mul_apply, h_mul]
  exact mul_le_one' hv.left hv.right

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

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) ≤ 1 ∧ Valued.v (y v) ≤ 1
h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v)
⊢ (x * y) v ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers, Pi.mul_apply, h_mul]

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) ≤ 1 ∧ Valued.v (y v) ≤ 1
h_mul : Valued.v (x v * y v) = Valued.v (x v) * Valued.v (y v)
⊢ Valued.v (x v) * Valued.v (y v) ≤ 1