Complex.Hadamard.card_ball_le_divisorMassClosedBall₀

lemma card_ball_le_divisorMassClosedBall₀    {f : ℂ → ℂ} (hf : Differentiable ℂ f) {R : ℝ} (hR : 0 < R) :    (Nat.card {p : divisorZeroIndex₀ f (Set.univ : Set ℂ) // ‖divisorZeroIndex₀_val p‖ ≤ R} : ℝ)      ≤ divisorMassClosedBall₀ f R := by  set U : Set ℂ := (Set.univ : Set ℂ)  set D : Function.locallyFinsuppWithin U ℤ := MeromorphicOn.divisor f U  haveI :      Fintype {p : divisorZeroIndex₀ f U // ‖divisorZeroIndex₀_val p‖ ≤ R} := by    have : Finite {p : divisorZeroIndex₀ f U // ‖divisorZeroIndex₀_val p‖ ≤ R} := by      have : Metric.closedBall (0 : ℂ) R ⊆ U := by simp [U]      simpa using (finite_divisorZeroIndex₀_subtype_norm_le (f := f) (U := U) (B := R) this)    exact Fintype.ofFinite _  have hDnonneg : 0 ≤ D := by    simpa [D, U] using (Differentiable.divisor_nonneg (f := f) hf)  let SR : Finset ℂ :=    (Function.locallyFinsuppWithin.finiteSupport (Function.locallyFinsuppWithin.toClosedBall R D)          (isCompact_closedBall (0 : ℂ) |R|)).toFinset  let S : Finset ℂ := SR.filter fun z : ℂ => z ≠ 0  let T : Type :=    Σ z : S, Fin (Int.toNat (D z.1))  let φ :      {p : divisorZeroIndex₀ f U // ‖divisorZeroIndex₀_val p‖ ≤ R} → T := fun p =>    let z0 : ℂ := divisorZeroIndex₀_val p.1    have hz0_memSR : z0 ∈ SR := by      have hz0_norm : ‖z0‖ ≤ |R| := by        have : ‖z0‖ ≤ R := p.2        simpa [abs_of_pos hR] using this      have hz0_support : z0 ∈ (Function.locallyFinsuppWithin.toClosedBall R D).support := by        have hz0_suppD : z0 ∈ D.support := by          simp [z0, D]        exact Function.locallyFinsuppWithin.mem_toClosedBall_support_of_mem_support_of_norm_le_abs          hz0_suppD hz0_norm      exact (Set.Finite.mem_toFinset        (Function.locallyFinsuppWithin.finiteSupport          (Function.locallyFinsuppWithin.toClosedBall R D)            (isCompact_closedBall (0 : ℂ) |R|))).2 hz0_support    have hz0_ne0 : z0 ≠ 0 := divisorZeroIndex₀_val_ne_zero p.1    have hz0_memS : z0 ∈ S := Finset.mem_filter.2 ⟨hz0_memSR, hz0_ne0⟩    ⟨⟨z0, hz0_memS⟩, by        simpa [z0, divisorZeroIndex₀_val, D] using p.1.1.2⟩  have hφ_inj : Function.Injective φ := by    intro p q hpq    have hσ := (Sigma.mk.inj_iff).1 hpq    have hzS : (φ p).1 = (φ q).1 := hσ.1    have hz : divisorZeroIndex₀_val p.1 = divisorZeroIndex₀_val q.1 := by      simpa [φ] using congrArg Subtype.val hzS    apply Subtype.ext    apply Subtype.ext    apply Sigma.ext    · exact hz    · simpa [φ] using hσ.2  have hcard_le :      Fintype.card {p : divisorZeroIndex₀ f U // ‖divisorZeroIndex₀_val p‖ ≤ R} ≤ Fintype.card T :=    Fintype.card_le_of_injective φ hφ_inj  have hT_card :      (Fintype.card T : ℝ) =        (S.sum fun z : ℂ => (Int.toNat (D z) : ℝ)) := by    have hNat :        Fintype.card T = ∑ z : S, Int.toNat (D z.1) := by      have h1 :          Fintype.card T = ∑ z : S, Fintype.card (Fin (Int.toNat (D z.1))) := by        change Fintype.card (Sigma (fun z : S => Fin (Int.toNat (D z.1))))            = ∑ z : S, Fintype.card (Fin (Int.toNat (D z.1)))        exact (Fintype.card_sigma (ι := S) (α := fun z : S => Fin (Int.toNat (D z.1))))      simpa using h1    have hR :        (Fintype.card T : ℝ) = ∑ z : S, (Int.toNat (D z.1) : ℝ) := by      exact_mod_cast hNat    have hR' :        (Fintype.card T : ℝ) = S.attach.sum (fun z : S => (Int.toNat (D z.1) : ℝ)) := by      simpa [Finset.univ_eq_attach] using hR    calc      (Fintype.card T : ℝ) = S.attach.sum (fun z : S => (Int.toNat (D z.1) : ℝ)) := hR'      _ = S.sum (fun z : ℂ => (Int.toNat (D z) : ℝ)) := by            simpa using (Finset.sum_attach (s := S) (f := fun z : ℂ => (Int.toNat (D z) : ℝ)))  have htoNat_le : ∀ z ∈ S, (Int.toNat (D z) : ℝ) ≤ (D z : ℝ) := by    intro z hz    have hDz_nonneg : 0 ≤ D z := by simpa [D] using hDnonneg z    have hEqZ : ((Int.toNat (D z) : ℕ) : ℤ) = D z := by      simpa using (Int.toNat_of_nonneg hDz_nonneg)    have hEqR : (Int.toNat (D z) : ℝ) = (D z : ℝ) := by      exact_mod_cast hEqZ    exact le_of_eq hEqR  calc    (Nat.card {p : divisorZeroIndex₀ f U // ‖divisorZeroIndex₀_val p‖ ≤ R} : ℝ)        = (Fintype.card {p : divisorZeroIndex₀ f U // ‖divisorZeroIndex₀_val p‖ ≤ R} : ℝ) := by          simp [Nat.card_eq_fintype_card]    _ ≤ (Fintype.card T : ℝ) := by exact_mod_cast hcard_le    _ = S.sum (fun z : ℂ => (Int.toNat (D z) : ℝ)) := hT_card    _ ≤ S.sum (fun z : ℂ => (D z : ℝ)) := by      refine Finset.sum_le_sum ?_      intro z hz      exact htoNat_le z hz    _ = divisorMassClosedBall₀ f R := by      rfl