-- 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
x : HeightOneSpectrum R
h h₁ :
  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))
                      ⋯})))) :
        ℤ) =
    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))
                      ⋯})))) :
        ℤ)
⊢ 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))
                      ⋯})))) :
        ℤ)

Tactic:
rw [count_ne_zero K _ hI]

Premises used: FractionalIdeal.count_ne_zero