Exists forall adic Valued sub lt

theorem exists_forall_adicValued_sub_lt {ι : Type*} (s : Finset ι)    (e : ι → (WithZero (Multiplicative ℤ))ˣ) (valuation : ι → HeightOneSpectrum A)    (injective : Function.Injective valuation)    (x : (i : ι) → (valuation i).adicCompletionIntegers K) :    ∃ a, ∀ i ∈ s, Valued.v ((algebraMap A K a) - (x i).val) < (e i).val := by  -- Approximate elements of `𝒪_v` with elements of `A` using the previous theorem.  choose f hf using fun (i : s) =>    exists_adicValued_sub_lt_of_adicCompletionInteger K (valuation i) (x i) (e i)  -- Convert the hypotheses from being about valuations to being about ideals, so  -- that we can apply (a suitable corollary of) the Chinese remainder theorem.  have hexists_e' : ∀ (i : ι), ∃ (e' : ℕ), (Multiplicative.ofAdd (-(e' : ℤ))) < (e i).val := by    intro i    apply exists_ofAdd_natCast_lt (e i).ne_zero  choose e' he' using hexists_e'  have hinj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j →      (fun i ↦ (valuation i).asIdeal) i ≠ (fun i ↦ (valuation i).asIdeal) j := by    intro _ _ _ _    exact mt <| fun hij ↦ injective (HeightOneSpectrum.ext hij)  -- Use Chinese remainder theorem to get a single approximation for `f i` for all `i ∈ s`.  obtain ⟨a, ha⟩ := IsDedekindDomain.exists_forall_sub_mem_ideal (s := s)    (fun i => (valuation i).asIdeal) e' (fun i hi => (valuation i).prime) hinj f  use a  intro i hi  specialize ha i hi  specialize hf ⟨i, hi⟩  rw [← intValuation_le_pow_iff_mem, ← valuation_of_algebraMap (K := K),    ← valuedAdicCompletion_eq_valuation, algebraMap.coe_sub] at ha  refine lt_of_le_of_lt ?_ (Valuation.map_add_lt _ (ha.trans_lt (he' i)) hf)  apply le_of_eq  congr  rw [add_sub, sub_eq_sub_iff_add_eq_add, add_right_cancel_iff,    add_comm_sub, add_sub, eq_sub_iff_add_eq]  rfl