-- 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 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:
by_cases hv : a v ∈ adicCompletionIntegers K v

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

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, hp⟩) 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
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

Tactic:
let p := ∏ᶠ v ∈ S, b v (a 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 : (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)
⊢ ∃ b c, a * ↑↑b = ↑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
⊢ (a * ↑↑⟨p, hp⟩) v ∈ adicCompletionIntegers K v

Tactic:
dsimp only

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
⊢ (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:
push_cast

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