Exists adic Valued sub lt of adic Completion Integer

theorem exists_adicValued_sub_lt_of_adicCompletionInteger    (x : v.adicCompletionIntegers K) (γ : ℤᵐ⁰ˣ) :    ∃a, Valued.v ((algebraMap A K a) - (x : v.adicCompletion K)) < γ.val := by  have h := closureAlgebraMapIntegers_eq_integers K v  rw [Set.ext_iff] at h  specialize h x  simp_rw [RingHom.coe_range, Subtype.coe_prop, iff_true, mem_closure_iff_nhds] at h  specialize h { y | Valued.v (y  - (x : v.adicCompletion K)) < γ.val }  have hn : {y | Valued.v (y - (x : v.adicCompletion K)) < γ.val} ∈ nhds x.val := by    rw [Valued.mem_nhds]    use (Units.mapEquiv (valueGroup₀_equiv_withZeroMulInt vK)).symm γ    have hsurj := (valuedAdicCompletion_surjective K v)    obtain ⟨z, hz⟩ := hsurj γ    simp [← hz, ← valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective hsurj,      (valueGroup₀_equiv_withZeroMulInt_strictMono (.ofClass vK)).lt_iff_lt,      -valueGroup₀_equiv_withZeroMulInt_apply]  obtain ⟨z, ⟨hz, a, ha⟩⟩ := h hn  use a  rw [algebraMap_adicCompletion, Function.comp_apply] at ha  rwa [ha]