Dense Range of prod Algebra Map

theorem denseRange_of_prodAlgebraMap {ι : Type*} [Finite ι]    {valuation : ι → HeightOneSpectrum A} (injective : Function.Injective valuation) :    DenseRange (algebraMap K ((i : ι) → (valuation i).adicCompletion K)) := by  rw [denseRange_iff_closure_range, Set.eq_univ_iff_forall]  let S := Set.range (algebraMap K ((i : ι) → (valuation i).adicCompletion K))  -- We've already shown that the closure of `A` is `∏_{v ∈ s} 𝒪_v`, so  -- the closure of `K` at least contains this set.  have hint : Set.pi Set.univ (fun (i : ι) ↦ ((valuation i).adicCompletionIntegers K).carrier)      ⊆ closure S := by    rw [← closureAlgebraMapIntegers_eq_prodIntegers _ _ injective]    apply closure_mono    exact fun _ ⟨a, ha⟩ ↦ ⟨algebraMap A K a, ha⟩  -- Next, the closure of `K` is closed under multiplication by `K` because  -- scalar multiplication by a constant is continuous.  have hmul : ∀x, x ∈ closure S → ∀k : K, k • x ∈ closure S := by    intro x h k    let f := fun (z : (i : ι) → (valuation i).adicCompletion K) ↦ k • z    have hf : ContinuousAt f x := Continuous.continuousAt (continuous_const_smul k)    apply closure_mono _ <| mem_closure_image hf h    rintro x ⟨_, ⟨z, rfl⟩, rfl⟩    use k • algebraMap K _ z    ext i    simp [Algebra.smul_def, f]  -- Finally, `∏_{v ∈ s} K_v = K • ∏_{v ∈ s} 𝒪_v`  intro x  obtain ⟨k, y, hy, hx⟩ := adicCompletion.eq_mul_pi_adicCompletionIntegers K valuation x  exact hx ▸ hmul y (hint hy) k