norm_fOfZero_le_norm_BlaschkeOfZero

@[blueprint "norm_fOfZero_le_norm_BlaschkeOfZero"  (title := "norm-fOfZero-le-norm-BlaschkeOfZero")  (statement := /--    Let $0 < r < R<1$, and $f:\mathbb{C}\to\mathbb{C}$ be analytic on $\overline{\mathbb{D}_1}$ with    $f(0)\neq 0$. Then    $$|f(0)|\leq|B_f(0)|.$$  -/)  (proof := /--    Applying lemma \ref{BlaschkeOfZero} we know that    $$|B_f(0)|=|f(0)|\prod_{\rho\in\mathcal{K}_f(r)}      \left(\frac{R}{|\rho|}\right)^{m_f(\rho)}.$$    Note that for all $\rho\in\mathcal{K}_f(r)$ that $1<R/|\rho|$ since $r<R$.    Thus, the result follows.  -/)  (latexEnv := "lemma")]lemma norm_fOfZero_le_norm_BlaschkeOfZero {r R : ℝ} {f : ℂ → ℂ}    (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1)    (finiteZeros : (SetOfZeros 1 f).Finite)    (hf_neq_zero_at_zero : f 0 ≠ 0) :    ‖f 0‖ ≤ ‖BlaschkeB r R f 0‖ := by  have r_lt_one : r < 1 := lt_trans r_lt_R R_lt_one  rw [BlaschkeOfZero r_pos r_lt_one r_lt_R finiteZeros hf_neq_zero_at_zero, ← mul_one ‖f 0‖]  refine mul_le_mul (by rw[mul_one]) ?_ (zero_le_one) (mul_nonneg (norm_nonneg (f 0)) zero_le_one)  rw [← Finset.prod_const_one (s := (finiteSetOfZeros_mono r_lt_one finiteZeros).toFinset)]  apply Finset.prod_le_prod  · intro ρ hρ    exact zero_le_one  · intro ρ hρ    simp only [SetOfZeros, Finite.mem_toFinset, mem_setOf_eq] at hρ    apply one_le_pow₀    rw[one_le_div]    · linarith    · rw [norm_pos_iff]      by_contra h      rw [h] at hρ      exact hf_neq_zero_at_zero hρ.2