awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Ne.{u_1 + 1} (α := Associates (Ideal R))
    (Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
    0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
h_dvd :
  LE.le (α := Associates (Ideal R))
    (Associates.mk (v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
    (Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
h_not_dvd :
  ¬LE.le (α := Associates (Ideal R))
      (Associates.mk
        (v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1)))
      (Associates.mk
        (∏ᶠ (v : HeightOneSpectrum R),
          v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ≤
    Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))

Tactic:
rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le h_ne_zero hv] at h_dvd h_not_dvd

Premises used: Associates.prime_pow_dvd_iff_le, Associates.mk_pow
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Ne.{u_1 + 1} (α := Associates (Ideal R))
    (Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
    0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
h_dvd :
  LE.le (α := Associates (Ideal R))
    (Associates.mk (v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
    (Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
h_not_dvd :
  ¬LE.le (α := Associates (Ideal R))
      (Associates.mk
        (v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1)))
      (Associates.mk
        (∏ᶠ (v : HeightOneSpectrum R),
          v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
h_dvd₁ :
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ≤
    Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
⊢ ¬Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1 ≤
      Associates.count (Associates.mk v.asIdeal)
        (Associates.factors
          (Associates.mk
            (∏ᶠ (v : HeightOneSpectrum R),
              v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))

Tactic:
rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le h_ne_zero hv] at h_dvd h_not_dvd

Premises used: Associates.prime_pow_dvd_iff_le, Associates.mk_pow
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Ne.{u_1 + 1} (α := Associates (Ideal R))
    (Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
    0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
h_dvd :
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ≤
    Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
h_not_dvd :
  ¬Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1 ≤
      Associates.count (Associates.mk v.asIdeal)
        (Associates.factors
          (Associates.mk
            (∏ᶠ (v : HeightOneSpectrum R),
              v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))) <
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1

Tactic:
rw [not_le] at h_not_dvd

Premises used: not_le
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Ne.{u_1 + 1} (α := Associates (Ideal R))
    (Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
    0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
h_dvd :
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ≤
    Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
h_not_dvd :
  Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))) <
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))

Tactic:
apply Nat.eq_of_le_of_lt_succ h_dvd h_not_dvd

Premises used: Nat.eq_of_le_of_lt_succ
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
rw : Eq (α := Associates (Ideal R)) (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)) (Associates.mk I)
⊢ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I = I

Tactic:
rw [← associated_iff_eq, ← Associates.mk_eq_mk_iff_associated]

Premises used: Associates.mk_eq_mk_iff_associated, associated_iff_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
ha : Ne.{u_1 + 1} (α := Associates (Ideal R)) (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)) 0
hb : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
h :
  ∀ (p : Associates (Ideal R)),
    Irreducible p →
      p.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
        p.count (Associates.factors (Associates.mk I))
⊢ Eq (α := Associates (Ideal R)) (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)) (Associates.mk I)

Tactic:
apply Associates.eq_of_eq_counts

Premises used: Associates.eq_of_eq_counts
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Ne.{u_1 + 1} (α := Associates (Ideal R)) (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)) 0

Tactic:
apply Associates.finprod_ne_zero I

Premises used: Associates.finprod_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Ne (α := Associates (Ideal R)) (Associates.mk I) 0

Tactic:
apply Associates.mk_ne_zero.mpr hI

Premises used: Iff.mpr, Associates.mk_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
hv : Irreducible v
h :
  ∀ (J : Ideal R) (hJv : Associates.mk J = v),
    v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
      v.count (Associates.factors (Associates.mk I))
⊢ v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
    v.count (Associates.factors (Associates.mk I))

Tactic:
obtain ⟨J, hJv⟩ := Associates.exists_rep v

Premises used: Associates.exists_rep
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
hv : Irreducible v
J : Ideal R
hJv : Associates.mk J = v
⊢ Irreducible J

Tactic:
rw [← hJv, Associates.irreducible_mk] at hv

Premises used: Associates.irreducible_mk
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
hv : Irreducible v
J : Ideal R
hJv : Associates.mk J = v
hv₁ : Irreducible J
⊢ Associates.mk J = v

Tactic:
rw [← hJv, Associates.irreducible_mk] at hv

Premises used: Associates.irreducible_mk
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
h :
  Associates.count (Associates.mk J)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
    Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
⊢ v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
    v.count (Associates.factors (Associates.mk I))

Tactic:
rw [← hJv]
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ Associates.count (Associates.mk J)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
    Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))

Tactic:
apply Ideal.finprod_count
    ⟨J, Ideal.isPrime_of_prime (irreducible_iff_prime.mp hv), Irreducible.ne_zero hv⟩ I hI

Premises used: IsDedekindDomain.HeightOneSpectrum.mk, Iff.mp, Ideal.finprod_count, Irreducible.ne_zero, Ideal.isPrime_of_prime, irreducible_iff_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
ha : Ne.{u_1 + 1} (α := Associates (Ideal R)) (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)) 0
hb : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
h :
  ∀ (p : Associates (Ideal R)),
    Irreducible p →
      p.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
        p.count (Associates.factors (Associates.mk I))
hb₁ : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
h₁ h₂ h₃ :
  ∀ (v : Associates (Ideal R)) (hv : Irreducible v),
    v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
      v.count (Associates.factors (Associates.mk I))
h₄ :
  ∀ (v : Associates (Ideal R)) (hv : Irreducible v) (J : Ideal R) (hJv : Associates.mk J = v),
    v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
      v.count (Associates.factors (Associates.mk I))
h₅ :
  ∀ (v : Associates (Ideal R)) (J : Ideal R) (hv : Irreducible J) (hJv : Associates.mk J = v),
    v.count (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
      v.count (Associates.factors (Associates.mk I))
h₆ :
  ∀ (v : Associates (Ideal R)) (J : Ideal R) (hv : Irreducible J) (hJv : Associates.mk J = v),
    Associates.count (Associates.mk J)
        (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I))) =
      Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
⊢ Eq (α := Associates (Ideal R)) (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)) (Associates.mk I)

Tactic:
classical
  apply Associates.eq_of_eq_counts
  · apply Associates.finprod_ne_zero I
  · apply Associates.mk_ne_zero.mpr hI
  intro v hv
  obtain ⟨J, hJv⟩ := Associates.exists_rep v
  rw [← hJv, Associates.irreducible_mk] at hv
  rw [← hJv]
  apply Ideal.finprod_count
    ⟨J, Ideal.isPrime_of_prime (irreducible_iff_prime.mp hv), Irreducible.ne_zero hv⟩ I hI

Premises used: Iff.mpr, Associates.irreducible_mk, Associates.eq_of_eq_counts, Associates.finprod_ne_zero, Associates.mk_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
nth_rw :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
⊢ ⨅ (i : HeightOneSpectrum R), i.maxPowDividing I = I

Tactic:
nth_rw 2 [← Ideal.finprod_heightOneSpectrum_factorization h0]

Premises used: Ideal.finprod_heightOneSpectrum_factorization
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
rw :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
rw₁ :
  (↑(Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯) :
        Set (HeightOneSpectrum R)).Pairwise
    (onFun (β := Ideal R) IsCoprime fun (i : HeightOneSpectrum R) ↦ i.maxPowDividing I)
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)

Tactic:
rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]

Premises used: dif_pos, Ideal.hasFiniteMulSupport, Ideal.prod_eq_iInf_of_pairwise_isCoprime, finprod_def
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x ↔
      Membership.mem (γ := Ideal R)
        (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
          i.maxPowDividing I)
        x
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)

Tactic:
ext x
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h :
  Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x →
    Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x
h₁ :
  Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x →
    Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x
⊢ Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x ↔
    Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x

Tactic:
constructor
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x →
    Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x

Tactic:
aesop
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h :
  (∀ (i : HeightOneSpectrum R) (i_1 : ¬i.maxPowDividing I = ⊤), x ∈ i.maxPowDividing I) →
    ∀ (i : HeightOneSpectrum R), x ∈ i.maxPowDividing I
⊢ Membership.mem (γ := Ideal R)
      (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I)
      x →
    Membership.mem (γ := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I) x

Tactic:
simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]

Premises used: Ideal.one_eq_top, Submodule.mem_iInf, Set.Finite.mem_toFinset, Function.mem_mulSupport, ne_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R) (i_1 : ¬i.maxPowDividing I = ⊤), x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
pos : i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
neg : ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
⊢ x ∈ i.maxPowDividing I

Tactic:
by_cases i.maxPowDividing I = ⊤

Premises used: IsDedekindDomain.HeightOneSpectrum.maxPowDividing
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R) (i_1 : ¬i.maxPowDividing I = ⊤), x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
h_1 : i.maxPowDividing I = ⊤
⊢ x ∈ i.maxPowDividing I

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R) (i_1 : ¬i.maxPowDividing I = ⊤), x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
h_1 : ¬i.maxPowDividing I = ⊤
⊢ x ∈ i.maxPowDividing I

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : HeightOneSpectrum R
hx :
  x ∈
    (↑(Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯) :
      Set (HeightOneSpectrum R))
y : HeightOneSpectrum R
hy :
  y ∈
    (↑(Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯) :
      Set (HeightOneSpectrum R))
hxy : x ≠ y
⊢ onFun (β := Ideal R) IsCoprime (fun (i : HeightOneSpectrum R) ↦ i.maxPowDividing I) x y

Tactic:
apply IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne _ _ hxy

Premises used: IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
rw :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (if h : HasFiniteMulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I then
      ∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) h,
        i.maxPowDividing I
    else 1)
rw₁ :
  Eq (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
rw₂ :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
rw₃ :
  (↑(Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯) :
        Set (HeightOneSpectrum R)).Pairwise
    (onFun (β := Ideal R) IsCoprime fun (i : HeightOneSpectrum R) ↦ i.maxPowDividing I)
rw₄ :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
rw₅ :
  (↑(Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯) :
        Set (HeightOneSpectrum R)).Pairwise
    (onFun (β := Ideal R) IsCoprime fun (i : HeightOneSpectrum R) ↦ i.maxPowDividing I)
rw₆ :
  Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (⨅ i ∈ Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
      i.maxPowDividing I)
rw₇ rw₈ :
  (↑(Finite.toFinset (s := mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯) :
        Set (HeightOneSpectrum R)).Pairwise
    (onFun (β := Ideal R) IsCoprime fun (i : HeightOneSpectrum R) ↦ i.maxPowDividing I)
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : HeightOneSpectrum R), i.maxPowDividing I)
    (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)

Tactic:
classical
  rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]
  · ext x
    constructor
    · aesop
    · simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
      intro h i
      by_cases i.maxPowDividing I = ⊤ <;> simp_all
  · intro x hx y hy hxy
    apply IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne _ _ hxy

Premises used: Ideal.one_eq_top, Submodule.mem_iInf, Set.Finite.mem_toFinset, Function.mem_mulSupport, dif_pos, ne_eq, Ideal.hasFiniteMulSupport, Ideal.prod_eq_iInf_of_pairwise_isCoprime, finprod_def
-- 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 : Ideal R
hI : I ≠ 0
rw : (↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) : FractionalIdeal R⁰ K)
| (↑I : FractionalIdeal R⁰ K)

Tactic:
rw [← Ideal.finprod_heightOneSpectrum_factorization hI]

Premises used: Ideal.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 : Ideal R
hI : I ≠ 0
conv_rhs :
  Eq.{u_2 + 1} (α := 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)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) : ℤ))
    (↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) : FractionalIdeal R⁰ K)
⊢ Eq.{u_2 + 1} (α := 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)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) : ℤ))
    (↑I : FractionalIdeal R⁰ K)

Tactic:
conv_rhs => rw [← Ideal.finprod_heightOneSpectrum_factorization hI]

Premises used: Ideal.finprod_heightOneSpectrum_factorization