-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : ¬I = 0
h :
  ∀ (x : HeightOneSpectrum R),
    count K x I =
      HSub.hSub (α := ℤ)
        (↑(Associates.count (Associates.mk x.asIdeal)
              (Associates.factors
                (Associates.mk
                  (choose (p := fun (x : Ideal R) ↦
                    choose (p := fun (x : R) ↦
                          ∃ (aI : Ideal R),
                            x ≠ 0 ∧
                              I =
                                HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β :=
                                  FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                                  (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) x)⁻¹ :
                                    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                                  ((↑aI : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) :
                                    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
                          ⋯ ≠
                        0 ∧
                      I =
                        HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β :=
                          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                          (spanSingleton R⁰
                              ((algebraMap R K : (a : R) → K)
                                  (choose (p := fun (x : R) ↦
                                    ∃ (aI : Ideal R),
                                      x ≠ 0 ∧
                                        I =
                                          HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β :=
                                            FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                                            (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) x)⁻¹ :
                                              FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                                            ((↑aI : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) :
                                              FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
                                    ⋯))⁻¹ :
                            FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                          ((↑x : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
                    ⋯)))) :
          ℤ)
        (↑(Associates.count (Associates.mk x.asIdeal)
              (Associates.factors
                (Associates.mk
                  (Ideal.span
                    {choose (p := fun (x : R) ↦
                        ∃ (aI : Ideal R),
                          x ≠ 0 ∧
                            I =
                              HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β :=
                                FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                                (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) x)⁻¹ :
                                  FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                                ((↑aI : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) :
                                  FractionalIdeal.{u_1, u_2} (R := R) R⁰ K))
                        ⋯})))) :
          ℤ)
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Tactic:
convert! finite_factors' hI (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2

Premises used: Classical.choose_spec, And.right, FractionalIdeal.exists_eq_spanSingleton_mul, FractionalIdeal.finite_factors'