-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finite_factors' {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R}
    {J : Ideal R} (haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) :
    ∀ᶠ v : HeightOneSpectrum R in Filter.cofinite,
      ((Associates.mk v.asIdeal).count (Associates.mk J).factors : ℤ) -
        (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_nmem : ¬v ∈ {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}
⊢ False

Tactic:
rw [mem_union, mem_setOf_eq, mem_setOf_eq] at h_nmem

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_nmem : ¬(v.asIdeal ∣ J ∨ v.asIdeal ∣ Ideal.span {a})
⊢ False

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
      0

Tactic:
have ha_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI haJ

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
      0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv : ¬0 = 0
hv_irred : Irreducible v.asIdeal
h_nmem :
  (Associates.mk v.asIdeal).count (Associates.mk J).factors = 0 ∧
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors = 0
⊢ False

Tactic:
exact hv (Eq.refl 0)

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
h_subset :
  {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0} ⊆
    {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
      0

Tactic:
exact Finite.subset (Finite.union (Ideal.finite_factors (ideal_factor_ne_zero hI haJ))
  (Ideal.finite_factors (constant_factor_ne_zero hI haJ))) h_subset

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_nmem : ¬(v.asIdeal ∣ J ∨ v.asIdeal ∣ Ideal.span {a})
⊢ False

Tactic:
push_neg at h_nmem

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_nmem : ¬v.asIdeal ∣ J ∧ ¬v.asIdeal ∣ Ideal.span {a}
⊢ False

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
⊢ v ∈ {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}

Tactic:
have hv_irred : Irreducible v.asIdeal := v.irreducible

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
⊢ v ∈ {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}