Exists nice factorization

theorem exists_nice_factorization  {ε : ℝ}  (hε_pos : 0 < ε)  (hε : ε < 1/2)  {d : ℕ}  (hd : d = ⌊5/2 * ε⁻¹^2⌋₊)  {n : ℕ}  {X : ℕ}  (h1n : 1 ≤ n)  (hnX : n ≤ X) :  ∃ (x : (Fin d) → ℕ), ∃ c : ℕ,    n = c * ∏ j, x j ^ (j.val + 1 : ℕ) ∧    c ≤ (X : ℝ) ^ ε ∧    (∀ i j, i ≠ j → Nat.gcd (x i) (x j) = 1) ∧    (X:ℝ)^(- ε) * ∏ j, x j ≤ (radical n : ℕ) ∧ (radical n : ℕ) ≤ (X:ℝ)^(ε) * ∏ j, x j ∧    0 < c ∧ (∀ i, 0 < x i) ∧ (∀ i, x i ≤ X) := by  let data : NiceFactorization.ProofData := ⟨    ε, hε_pos, hε, d, hd, n, X, h1n, hnX  ⟩  obtain ⟨x, c, hn, hc, hcop, h_le_rad, h_rad_le⟩ := NiceFactorization.exists_nice_factorization  have : NeZero ProofData.d := by infer_instance  simp_rw [data] at *  have hc_pos : 0 < c := by    have : 0 < n := by omega    apply Nat.pos_of_mul_pos_right (hn ▸ this)  have x_le_X (i : Fin d) : x i ≤ X := by    apply le_trans _ hnX    apply Nat.le_of_dvd    · omega    rw [hn]    apply Dvd.dvd.mul_left    trans x i ^ (i.val + 1)    · apply dvd_pow (dvd_rfl)      omega    apply Finset.dvd_prod_of_mem    exact Finset.mem_univ i  have hx_pos (i : Fin d) : 0 < x i := by    apply Nat.pos_of_ne_zero    intro h    rw [Finset.prod_eq_zero (Finset.mem_univ i)] at hn    · omega    · simp [h]  exact ⟨x, c, hn, hc, hcop, h_le_rad, h_rad_le, hc_pos, hx_pos, x_le_X⟩