Erdos392.exists_phi_div_self_lt

lemma exists_phi_div_self_lt {ε : ℝ} (hε : 0 < ε) :    ∃ a : ℕ, a ≠ 0 ∧ (a.totient : ℝ) / a < ε := by  obtain ⟨n, hn⟩ : ∃ n : ℕ, ∏ p ∈ filter Prime (range n), (1 - 1 / (p : ℝ)) < ε :=    (prod_one_sub_one_div_prime_tendsto_zero.eventually (gt_mem_nhds hε)).exists  use ∏ p ∈ filter Prime (range n), p  rw [totient_eq_div_primeFactors_mul, primeFactors_prod]  · rw [Nat.div_self] <;> norm_num    · rw [← Finset.prod_div_distrib]      refine ⟨prod_ne_zero_iff.mpr fun p hp ↦ (mem_filter.mp hp).2.ne_zero, ?_⟩      convert hn using 1      exact prod_congr rfl fun x hx ↦ by        rw [cast_sub <| succ_le_of_lt (mem_filter.mp hx).2.pos]        simp [sub_div, (mem_filter.mp hx).2.ne_zero]    · exact fun _ _ hi' ↦ hi'.pos  · aesop