theorem lemma_16_30 {k : Type u} [Field k] [IsAlgClosed k] {F : Type u} [Field F] (ι : k →+* F) (_hι : Function.Injective ⇑ι) (R : ValuationSubring F) (hkR : ∀ (x : k), ι x ∈ R) : ∃ R' ≤ R, (∀ (x : k), ι x ∈ R') ∧ ∃ (Φ : ↥R' →+* k), RingHom.ker Φ = IsLocalRing.maximalIdeal ↥R' ∧ Function.Surjective ⇑Φ