Complex.Hadamard.divisorZeroIndex₀_fiberFinset_card_eq_toNat_divisor

lemma divisorZeroIndex₀_fiberFinset_card_eq_toNat_divisor (f : ℂ → ℂ) {z₀ : ℂ} (hz₀ : z₀ ≠ 0) :    (divisorZeroIndex₀_fiberFinset (f := f) z₀).card =      Int.toNat (MeromorphicOn.divisor f (Set.univ : Set ℂ) z₀) := by  let S : Set (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := {p | divisorZeroIndex₀_val p = z₀}  have hS : S.Finite := divisorZeroIndex₀_fiber_finite (f := f) z₀  set n : ℕ := Int.toNat (MeromorphicOn.divisor f (Set.univ : Set ℂ) z₀)  have hcard : Nat.card S = n := by    classical    haveI : Fintype S := hS.fintype    -- `S` is the fiber over `z₀`, hence equivalent to `Fin (Int.toNat (divisor z₀))`.    let e : S ≃ Fin n :=      { toFun := by          intro x          rcases x with ⟨p, hp⟩          rcases p with ⟨⟨z, q⟩, hz⟩          have hzEq : z = z₀ := by simpa [divisorZeroIndex₀_val] using! hp          subst hzEq          simpa [n] using q        invFun := by          intro q          refine ⟨⟨⟨z₀, ?_⟩, hz₀⟩, ?_⟩          · simpa [n] using q          · simp [S, divisorZeroIndex₀_val]        left_inv := by          rintro ⟨p, hp⟩          rcases p with ⟨⟨z, q⟩, hz⟩          have hzEq : z = z₀ := by simpa [divisorZeroIndex₀_val] using! hp          subst hzEq          (ext; rfl)        right_inv := by          intro q          rfl }    have h := Nat.card_congr (α := S) (β := Fin n) e    simpa using (h.trans (by simp))  have hSncard : S.ncard = n := by    simpa [Nat.card_coe_set_eq] using hcard  have hto : hS.toFinset = divisorZeroIndex₀_fiberFinset (f := f) z₀ := by    rfl  have htoFinset : S.ncard = (divisorZeroIndex₀_fiberFinset (f := f) z₀).card := by    have h' : S.ncard = hS.toFinset.card := Set.ncard_eq_toFinset_card S hS    simpa [hto] using h'  exact htoFinset.symm.trans hSncard