Closure Algebra Map Integers eq integers

theorem closureAlgebraMapIntegers_eq_integers :    closure (algebraMap A (v.adicCompletion K)).range =    SetLike.coe (v.adicCompletionIntegers K) := by  apply subset_antisymm  -- We know `closure A ⊆ 𝒪_v` because `𝒪_v` is closed and `A ⊆ 𝒪_v`  · apply closure_minimal _ (Valued.isClosed_valuationSubring _)    rintro b ⟨a, rfl⟩    exact coe_mem_adicCompletionIntegers v a  -- Show `𝒪_v ⊆ closure A` from `𝒪_v ⊆ closure O_[K]` and `closure O_[K] ⊆ closure A`  · let f := fun (k : WithVal (v.valuation K)) => (k : v.adicCompletion K)    suffices h : closure (f '' (f ⁻¹' (adicCompletionIntegers K v))) ⊆        closure (algebraMap A (adicCompletion K v)).range by      apply Set.Subset.trans _ h      -- `f = ofCompletion ∘ (↑·)` has dense range: `ofCompletion` is a surjective homeomorphism      -- and the completion coercion is dense.      exact DenseRange.subset_closure_image_preimage_of_isOpen        ((adicCompletion.ofCompletion_surjective K v).denseRange.comp          UniformSpace.Completion.denseRange_coe (adicCompletion.continuous_ofCompletion K v))        (Valued.isOpen_valuationSubring _)    -- Unfold the topological definitions until we get the result from the previous lemma    apply closure_minimal _ isClosed_closure    rintro k ⟨x, hx, rfl⟩    unfold f at hx    rw [Set.mem_preimage, SetLike.mem_coe, mem_adicCompletionIntegers,        adicCompletion.valued_ofCompletion, Valued.valuedCompletion_apply] at hx    rw [mem_closure_iff_nhds_zero]    intro U hU    rw [Valued.mem_nhds] at hU    obtain ⟨γ, hγ⟩ := hU    let γ' := Units.mapEquiv (valueGroup₀_equiv_withZeroMulInt _).toMulEquiv γ    obtain ⟨a, ha⟩ := exists_adicValued_sub_lt_of_adicValued_le_one K v γ' hx    use algebraMap A K a    constructor    · use a      rfl    · apply hγ      simp only [sub_zero, WithVal.equiv_symm_apply, Set.mem_setOf_eq]      rwa [← (valueGroup₀_equiv_withZeroMulInt_strictMono _).lt_iff_lt,        valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective        (valuedAdicCompletion_surjective K v)]