Closure Algebra Map Integers eq prod Integers

theorem closureAlgebraMapIntegers_eq_prodIntegers {ι : Type*}    (v : ι → HeightOneSpectrum A)    (injective : Function.Injective v) :    closure (SetLike.coe (algebraMap A ((i : ι) → (v i).adicCompletion K)).range) =    (Set.pi Set.univ (fun (i : ι) ↦ ((v i).adicCompletionIntegers K).carrier)) := by  apply Set.Subset.antisymm  · apply closure_minimal    · rintro c ⟨a, ha⟩ i -      rw [← ha]      simp only [Pi.algebraMap_apply]      exact coe_mem_adicCompletionIntegers (v i) a    · apply isClosed_set_pi      rintro w -      apply Valued.isClosed_valuationSubring  · intro f hf    rw [mem_closure_iff_nhds_zero]    intro U hU    rw [Pi.zero_def, nhds_pi, Filter.mem_pi'] at hU    obtain ⟨I, t, htn, hts⟩ := hU    choose g' hg' using fun w => (Valued.is_topological_valuation (t w)).mp (htn w)    let g := fun w ↦ Units.mapEquiv (valueGroup₀_equiv_withZeroMulInt _).toMulEquiv (g' w)    obtain ⟨a, ha⟩ :=      exists_forall_adicValued_sub_lt K I g v injective (fun w => ⟨f w, hf w ⟨⟩⟩)    use algebraMap A _ a    constructor    · rw [RingHom.coe_range]      exact Set.mem_range_self a    · refine hts fun w hw ↦ hg' w ?_      rw [Set.mem_setOf_eq, ← (valueGroup₀_equiv_withZeroMulInt_strictMono _).lt_iff_lt,        valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective          (valuedAdicCompletion_surjective K (v w))]      exact ha w hw