Exists pow smul mem integer

theorem exists_pow_smul_mem_integer {ϖ : 𝒪[K]} (hϖ : Irreducible ϖ) (x : L) :    ∃ t : ℕ, (ϖ : K) ^ t • x ∈ 𝒪[L] := by  rcases eq_or_ne x 0 with rfl | hx  · exact ⟨0, by simp⟩  let : UniformSpace L := IsTopologicalAddGroup.rightUniformSpace L  have : IsUniformAddGroup L := isUniformAddGroup_of_addCommGroup (G := L)  let : (Valued.v (R := L)).RankOne := rankOneOfIoo L default  let : NontriviallyNormedField L := Valued.toNontriviallyNormedField (L := L) _  have hϖ1 : ‖algebraMap K L ϖ‖ < 1 := Valued.toNormedField.norm_lt_one_iff.mpr    (valuation_map_irreducible_lt_one hϖ)  obtain ⟨t, ht⟩ := _root_.exists_pow_lt_of_lt_one (inv_pos.mpr (norm_pos_iff.mpr hx)) hϖ1  have h1 : ‖(ϖ : K) ^ t • x‖ ≤ 1 := by    rw [Algebra.smul_def, map_pow, norm_mul, norm_pow]    calc ‖algebraMap K L ϖ‖ ^ t * ‖x‖        ≤ ‖x‖⁻¹ * ‖x‖ := by gcongr      _ = 1 := inv_mul_cancel₀ (norm_ne_zero_iff.mpr hx)  exact ⟨t, Valued.toNormedField.norm_le_one_iff.mp h1⟩