Exists nice factorization

theorem exists_nice_factorization'  {ε : ℝ}  (hε_pos : 0 < ε)  (hε : ε < 1/2)  {d : ℕ}  (hd : d = ⌊10 * ε⁻¹^4⌋₊)  {n : ℕ}  {X : ℕ}  (h1n : 1 ≤ n)  (hnX : n ≤ X)  (α : ℝ)  (hsim : (radical n : ℕ) ~ (X : ℝ) ^ α) :  ∃ (x : (Fin d) → ℕ), ∃ c : ℕ,    n = c * ∏ j, x j ^ (j.val + 1 : ℕ) ∧    c ≤ (X : ℝ) ^ (ε^2) ∧    c ≤ ⌊(X : ℝ) ^ (ε/4)⌋₊ ∧    (∀ i j, i ≠ j → Nat.gcd (x i) (x j) = 1) ∧    (X : ℝ)^(α - ε) ≤ ∏ j, x j ∧ ∏ j, x j ≤ 2 * (X : ℝ)^(α + ε) ∧    0 < c ∧ (∀ i, 0 < x i) ∧ (∀ i, x i ≤ X) := by  have hε_sq : ε^2/2 < 1/2 := by    nlinarith only [hε, hε_pos]  have : 0 < X := by omega  simp only [similar, Set.mem_Icc] at hsim  obtain ⟨x, c, x_eq_c_mul_prod, c_le_pow, hx_cop, le_rad_n, rad_n_le, c_pos, hx_pos, hx_le_X⟩ :=    exists_nice_factorization (ε := ε^2/2) (by positivity) hε_sq (d := d) (by rw [hd]; ring_nf)      h1n hnX  refine ⟨x, c, x_eq_c_mul_prod, ?_, ?_, hx_cop, ?_, ?_, c_pos, hx_pos, hx_le_X⟩  · trans (X : ℝ)^(ε^2/2)    · exact c_le_pow    gcongr    · norm_cast    · linarith [sq_nonneg ε]  · rw [Nat.le_floor_iff]    · apply c_le_pow.trans      gcongr _ ^ ?_      · norm_cast      · nlinarith    positivity  · rw [sub_eq_add_neg, Real.rpow_add, Real.rpow_neg, mul_inv_le_iff₀]    · apply hsim.1.trans (rad_n_le.trans _)      rw [mul_comm]      gcongr      · norm_cast      · nlinarith only [hε, hε_pos]    · positivity    · positivity    · positivity  · rw [Real.rpow_add, ← mul_assoc, ← mul_inv_le_iff₀]    · apply le_trans (le_trans _ le_rad_n) hsim.2      rw [mul_comm, Real.rpow_neg (by positivity)]      gcongr      · norm_cast      · nlinarith only [hε, hε_pos]    · positivity    · norm_cast