awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
hI :
  spanSingleton R⁰ (mk' K n d) =
    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) (↑d : R))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(Ideal.span {n}) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {n})))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)))
    (spanSingleton R⁰ (mk' K n d))

Tactic:
finprod_heightOneSpectrum_factorization h0 hI

Premises used: FractionalIdeal.finprod_heightOneSpectrum_factorization
-- 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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) (0 : K)
h0 : Ne (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) 0
hI :
  spanSingleton R⁰ (mk' K n d) =
    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) (↑d : R))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(Ideal.span {n}) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {n})))) : ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)))
    (spanSingleton R⁰ (mk' K n d))

Tactic:
exact finprod_heightOneSpectrum_factorization h0 hI

Premises used: FractionalIdeal.finprod_heightOneSpectrum_factorization
-- 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
set :
  let d : ↥R⁰ :=
    choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k)
      ⋯;
  ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors
                  (Associates.mk
                    (Ideal.span {choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯})))) :
            ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)) =
    I
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors
                  (Associates.mk
                    (Ideal.span {choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯})))) :
            ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors
                  (Associates.mk
                    (Ideal.span
                      {(↑(choose (p := fun (x : ↥R⁰) ↦
                              mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k)
                              ⋯) :
                          R)})))) :
            ℤ)) =
    I

Tactic:
set d : ↥R⁰ := choose (choose_spec (exists_mk'_eq R⁰ k))

Premises used: nonZeroDivisors, Classical.choose_spec, Classical.choose, IsLocalization.exists_mk'_eq
-- 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
⊢ mk' K n d = k

Tactic:
have hnd : mk' K n d = k := choose_spec (choose_spec (exists_mk'_eq R⁰ k))
-- 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hnd : mk' K n d = k
by_contra : ∀ (h : n = 0), False
⊢ n ≠ 0

Tactic:
by_contra h
-- 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hnd : mk' K n d = k
h : n = 0
⊢ I = 0

Tactic:
rw [← hnd, h, IsFractionRing.mk'_eq_div, map_zero, zero_div, spanSingleton_zero] at hk

Premises used: IsFractionRing.mk'_eq_div, zero_div, map_zero, FractionalIdeal.spanSingleton_zero
-- 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hnd : mk' K n d = k
h : n = 0
hk₁ : I = 0
⊢ mk' K n d = k

Tactic:
rw [← hnd, h, IsFractionRing.mk'_eq_div, map_zero, zero_div, spanSingleton_zero] at hk

Premises used: IsFractionRing.mk'_eq_div, zero_div, map_zero, FractionalIdeal.spanSingleton_zero
-- 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hnd : mk' K n d = k
h : n = 0
hk₁ : I = 0
hnd₁ : mk' K n d = k
⊢ n = 0

Tactic:
rw [← hnd, h, IsFractionRing.mk'_eq_div, map_zero, zero_div, spanSingleton_zero] at hk

Premises used: IsFractionRing.mk'_eq_div, zero_div, map_zero, FractionalIdeal.spanSingleton_zero
-- 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
k : K
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hk : I = 0
hnd : mk' K n d = k
h : n = 0
⊢ False

Tactic:
hI hk
-- 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
k : K
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hk : I = 0
hnd : mk' K n d = k
h : n = 0
⊢ False

Tactic:
exact hI hk
-- 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hnd : mk' K n d = k
⊢ n ≠ 0

Tactic:
have hn0 : n ≠ 0 := by
    by_contra h
    rw [← hnd, h, IsFractionRing.mk'_eq_div, map_zero, zero_div, spanSingleton_zero] at hk
    exact hI hk
-- 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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯
d : ↥R⁰ :=
  choose (p := fun (x : ↥R⁰) ↦ mk' K (choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯) x = k) ⋯
hnd : mk' K n d = k
hn0 : n ≠ 0
rw : spanSingleton R⁰ (mk' K n d) = I
rw₁ : Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (mk' K n d)) (spanSingleton R⁰ k)
rw₂ rw₃ : Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ k) (spanSingleton R⁰ k)
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K)
        (HSub.hSub (α := ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors
                  (Associates.mk
                    (Ideal.span {choose (p := fun (x : R) ↦ ∃ (y : ↥(R⁰ : Submonoid R)), mk' K x y = k) ⋯})))) :
            ℤ)
          (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {(↑d : R)})))) :
            ℤ)) =
    I

Tactic:
rw [finprod_heightOneSpectrum_factorization_principal_fraction hn0 d, hk, hnd]

Premises used: FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction
-- 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
⊢ count K v 0 = 0

Tactic:
simp only [count, dif_pos]

Premises used: dif_pos, FractionalIdeal.count
-- 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
h_aJ :
  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)
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))
    ⋯
⊢ 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)

Tactic:
have h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁ :=
    (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2
-- 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
h_aJ :
  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)
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_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)
⊢ a₁ ≠ 0

Tactic:
have h_a₁_ne_zero : a₁ ≠ 0 := (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).1
-- 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
h_aJ :
  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)
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_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
⊢ J₁ ≠ 0

Tactic:
have h_J₁_ne_zero : J₁ ≠ 0 := ideal_factor_ne_zero hI h_a₁J₁
-- 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
h_aJ :
  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)
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_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
⊢ Ne (α := Ideal R) (Ideal.span {a}) 0

Tactic:
have h_a_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI h_aJ