-- 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
v : HeightOneSpectrum R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : 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))
    ⋯
J₁ : Ideal R :=
  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))
    ⋯
h_aJ :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑(J₁ * Ideal.span {a}) : FractionalIdeal R⁰ K)
    (↑(J * Ideal.span {a₁}) : FractionalIdeal R⁰ K)
h_a₁J₁ :
  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) a₁)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J₁ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
h_J_ne_zero : J ≠ 0
h_a₁' :
  Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a₁) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (0 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
h_a' :
  Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (0 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
rw : Ne (α := Associates (Ideal R)) (Associates.mk J) 0
rw₁ :
  Ne (α := Associates (Ideal R))
    (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))
            ⋯}))
    0
rw₂ :
  Ne (α := Associates (Ideal R))
    (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))
        ⋯))
    0
rw₃ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {a})) 0
⊢ count K v I =
    HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ)

Tactic:
rw [count, dif_neg hI, sub_eq_sub_iff_add_eq_add, ← natCast_add, ← natCast_add, natCast_inj,
    ← Associates.count_mul _ _ hv, ← Associates.count_mul _ _ hv, Associates.mk_mul_mk,
    Associates.mk_mul_mk, coeIdeal_injective h_aJ]

Premises used: Int.natCast_add, FractionalIdeal.coeIdeal_injective, sub_eq_sub_iff_add_eq_add, dif_neg, Associates.mk_mul_mk, Associates.count_mul, FractionalIdeal.count, Int.natCast_inj