-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
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
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (count K v I) =
    I
have h : 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)
            (Classical.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))
              sorry))⁻¹ :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    ((↑(Classical.choose (p := fun (x : Ideal R) ↦
            Classical.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))
                  sorry ≠
                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)
                          (Classical.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))
                            sorry))⁻¹ :
                    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))
            sorry) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
Tactic: have h := (Classical.choose_spec (Classical.choose_spec (exists_eq_spanSingleton_mul I))).2