-- 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:
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
⊢ p = b v (a v) * ∏ᶠ (w : HeightOneSpectrum R) (_ : w ∈ S \ {v}), b w (a w)

Tactic:
rw [← finprod_mem_singleton (a := v) (f := fun v ↦ b v (a v)),
  finprod_mem_mul_diff (singleton_subset_iff.2 ‹v ∈ S›) a.2]

Result:
no goals

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
⊢ (a * ↑p) v ∈ adicCompletionIntegers K v

Tactic:
have pprod : p = b v (a v) * ∏ᶠ w ∈ S \ {v}, b w (a w) := by
  rw [← finprod_mem_singleton (a := v) (f := fun v ↦ b v (a v)),
    finprod_mem_mul_diff (singleton_subset_iff.2 ‹v ∈ S›) a.2]

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 * ↑p) v ∈ adicCompletionIntegers K v

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:
exact mul_mem (h v (a v)) <| coe_mem_adicCompletionIntegers _ _

Result:
no goals

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 * ↑p) v ∈ adicCompletionIntegers K v

Tactic:
rw [pprod]

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

Tactic:
intro v

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