TendstoUniformlyOn.mul_left_bounded

theorem _root_.TendstoUniformlyOn.mul_left_bounded {ι : Type*} {p : Filter ι} {K : Set ℂ}    {F : ι → ℂ → ℂ} {f : ℂ → ℂ} {h : ℂ → ℂ}    (hF : TendstoUniformlyOn F f p K) (hh : ∃ C, ∀ z ∈ K, ‖h z‖ ≤ C) :    TendstoUniformlyOn (fun n z => h z * F n z) (fun z => h z * f z) p K := by  intro u hu  rcases Metric.mem_uniformity_dist.1 hu with ⟨ε, hεpos, hεu⟩  rcases hh with ⟨C, hC⟩  set C' : ℝ := max C 1  have hC'pos : 0 < C' := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_max_right _ _)  have hC' : ∀ z ∈ K, ‖h z‖ ≤ C' := fun z hz => le_trans (hC z hz) (le_max_left _ _)  have hv : {p : ℂ × ℂ | dist p.1 p.2 < ε / C'} ∈ uniformity ℂ :=    Metric.mem_uniformity_dist.2 ⟨ε / C', div_pos hεpos hC'pos, fun _ _ hab => hab⟩  have hF' : ∀ᶠ n in p, ∀ z : ℂ, z ∈ K → dist (f z) (F n z) < ε / C' := hF _ hv  filter_upwards [hF'] with n hn z hzK  have hn' : ‖f z - F n z‖ < ε / C' := by simpa [dist_eq_norm] using hn z hzK  have hle : ‖h z‖ * ‖f z - F n z‖ ≤ C' * ‖f z - F n z‖ :=    mul_le_mul_of_nonneg_right (hC' z hzK) (norm_nonneg _)  have hlt : C' * ‖f z - F n z‖ < C' * (ε / C') := mul_lt_mul_of_pos_left hn' hC'pos  have hnorm :      ‖h z * f z - h z * F n z‖ = ‖h z‖ * ‖f z - F n z‖ := by    calc      ‖h z * f z - h z * F n z‖ = ‖h z * (f z - F n z)‖ := by simp [mul_sub]      _ = ‖h z‖ * ‖f z - F n z‖ := by simp  have hdist : dist (h z * f z) (h z * F n z) < ε := by    rw [dist_eq_norm, hnorm]    have hlt' : ‖h z‖ * ‖f z - F n z‖ < ε := by      calc        ‖h z‖ * ‖f z - F n z‖ ≤ C' * ‖f z - F n z‖ := hle        _ < C' * (ε / C') := hlt        _ = ε := by field_simp [hC'pos.ne']    exact hlt'  exact hεu hdist