-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
lemma mul_nonZeroDivisor_mem_finiteIntegralAdeles (a : FiniteAdeleRing R K) :
    ∃ (b : R⁰) (c : R_hat R K), a * ((b : R) : FiniteAdeleRing R K) = c

Proof state:
case neg
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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
b : (v : HeightOneSpectrum R) → adicCompletion K v → R
hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰
h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v
p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v (a v)
hp : p ∈ R⁰
v : HeightOneSpectrum R
hv : a v ∉ adicCompletionIntegers K v
pprod : p = b v (a v) * ∏ᶠ (w : HeightOneSpectrum R) (_ : w ∈ S \ {v}), b w (a w)
⊢ (a * (↑(b v (a v)) * ↑(∏ᶠ (w : HeightOneSpectrum R) (_ : w ∈ S \ {v}), b w (a w)))) v ∈ adicCompletionIntegers K v

Tactic:
rw [← mul_assoc]

Result:
case neg
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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
b : (v : HeightOneSpectrum R) → adicCompletion K v → R
hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰
h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v
p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v (a v)
hp : p ∈ R⁰
v : HeightOneSpectrum R
hv : a v ∉ adicCompletionIntegers K v
pprod : p = b v (a v) * ∏ᶠ (w : HeightOneSpectrum R) (_ : w ∈ S \ {v}), b w (a w)
⊢ (a * ↑(b v (a v)) * ↑(∏ᶠ (w : HeightOneSpectrum R) (_ : w ∈ S \ {v}), b w (a w))) 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
a : FiniteAdeleRing R K
⊢ ∃ b c, a * ↑↑b = ↑c

Tactic:
let S := {v | a v ∉ adicCompletionIntegers K 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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
⊢ ∃ b c, a * ↑↑b = ↑c

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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
b : (v : HeightOneSpectrum R) → adicCompletion K v → R
hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰
h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v
p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v (a v)
hp : p ∈ R⁰
⊢ ∃ b c, a * ↑↑b = ↑c

Tactic:
use ⟨p, hp⟩

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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
b : (v : HeightOneSpectrum R) → adicCompletion K v → R
hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰
h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v
p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v (a v)
hp : p ∈ R⁰
⊢ ∃ c, a * ↑↑⟨p, hp⟩ = ↑c

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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
⊢ ∃ b c, a * ↑↑b = ↑c

Tactic:
choose b hb h using adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (R := R) (K := K)

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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
b : (v : HeightOneSpectrum R) → adicCompletion K v → R
hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰
h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v
⊢ ∃ b c, a * ↑↑b = ↑c

Proof state:
case pos
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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
b : (v : HeightOneSpectrum R) → adicCompletion K v → R
hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰
h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v
p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v (a v)
hp : p ∈ R⁰
v : HeightOneSpectrum R
hv : a v ∈ adicCompletionIntegers K v
⊢ (a * ↑↑⟨p, hp⟩) v ∈ adicCompletionIntegers K v

Tactic:
exact mul_mem hv <| coe_mem_adicCompletionIntegers _ _

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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
b : (v : HeightOneSpectrum R) → adicCompletion K v → R
hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰
h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v
p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v (a v)
hp : p ∈ R⁰
⊢ ∃ c, a * ↑↑⟨p, hp⟩ = ↑c

Tactic:
rw [exists_finiteIntegralAdele_iff]

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
a : FiniteAdeleRing R K
S : Set (HeightOneSpectrum R) := {v | a v ∉ adicCompletionIntegers K v}
b : (v : HeightOneSpectrum R) → adicCompletion K v → R
hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰
h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v
p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v (a v)
hp : p ∈ R⁰
⊢ ∀ (v : HeightOneSpectrum R), (a * ↑↑⟨p, hp⟩) v ∈ adicCompletionIntegers K v