Ring Haar Char D𝔸 real surjective

lemma ringHaarChar_D𝔸_real_surjective (r : ℝ) (h : r > 0) :    ∃ (ρ : ℝˣ), ringHaarChar      ((D𝔸ProdRightUnits K D).symm (((Units.map (algebraMap ℝ (Dinf K D))) ρ),1)) = r := by  have a : IsUnit (r ^ (1 / Module.finrank ℝ (Dinf K D) : ℝ)) := by    simp only [one_div, isUnit_iff_ne_zero, ne_eq]    refine (Real.rpow_ne_zero (by positivity) ?_).mpr (by positivity)    simp [Nat.ne_zero_iff_zero_lt, Module.finrank_pos]  have := ringHaarChar_ModuleFinite_unit (K := ℝ) (R := Dinf K D) (a.unit)  use a.unit  rw [ringHaarChar_D𝔸, ringHaarChar_prod, map_one, mul_one]  simp_all only [gt_iff_lt, RingHom.toMonoidHom_eq_coe, NNReal.coe_pow]  have t : (ringHaarChar a.unit) = r ^ ((1 / Module.finrank ℝ (Dinf K D) : ℝ)) := by    simp_rw [MeasureTheory.ringHaarChar_real, IsUnit.unit_spec, coe_nnnorm, Real.norm_eq_abs,      one_div, abs_eq_self]    positivity  simp_rw [t, one_div]  exact Real.rpow_inv_natCast_pow (by positivity) (Nat.ne_zero_iff_zero_lt.mpr Module.finrank_pos)