awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I ≠ ⊥
⊢ (↑((idealFactorsEquivOfQuotEquiv f : (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L ⋯)) :
      Ideal A) ∈
    normalizedFactors J
have refine : ∀ (l l' : { l : Ideal R // l ∣ I }),
  Dvd.dvd.{u_2} (α := Ideal A)
      (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
              (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
            l) :
        Ideal A)
      (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
              (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
            l') :
        Ideal A) ↔
    (↑l : Ideal R) ∣ (↑l' : Ideal R)
Tactic: refine mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors hI hJ hL
    (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ emultiplicity
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x)
              (↑(Subtype.mk (p := fun (x : Ideal R) ↦
                    Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x) L hL) :
                Ideal R)
              ⋯)) :
        Ideal A)
      J =
    emultiplicity L I
have refine : ∀ (l l' : { l : Ideal R // l ∣ I }),
  Dvd.dvd.{u_2} (α := Ideal A)
      (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
              (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
            l) :
        Ideal A)
      (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
              (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
            l') :
        Ideal A) ↔
    (↑l : Ideal R) ∣ (↑l' : Ideal R)
Tactic: refine emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors hI hJ hL
    (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n
have zero : ∀ (h : a * b ∈ HPow.hPow (β := ℕ) I 0), a ∈ I ∨ b ∈ HPow.hPow (β := ℕ) I 0
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ n
zero : ∀ (h : a * b ∈ HPow.hPow (β := ℕ) I 0), a ∈ I ∨ b ∈ HPow.hPow (β := ℕ) I 0
⊢ a ∈ I ∨ b ∈ I ^ n
have succ : ∀ (n : ℕ) (h : a * b ∈ I ^ (n + 1)), a ∈ I ∨ b ∈ I ^ (n + 1)
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ (n + 1)
⊢ a ∈ I ∨ b ∈ I ^ (n + 1)
have pos : ∀ (hI0 : I = ⊥), a ∈ I ∨ b ∈ I ^ (n + 1)
Tactic: by_cases hI0 : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ (n + 1)
pos : ∀ (hI0 : I = ⊥), a ∈ I ∨ b ∈ I ^ (n + 1)
⊢ a ∈ I ∨ b ∈ I ^ (n + 1)
have neg : ∀ (hI0 : ¬I = ⊥), a ∈ I ∨ b ∈ I ^ (n + 1)
Tactic: by_cases hI0 : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ (n + 1)
hI0 : ¬I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n + 1)
have this : I.IsMaximal
Tactic: have : I.IsMaximal := hI.isMaximal hI0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I
have h₁ : b * a ∈ I ^ n
Tactic: rw [mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I
have rw : b ∈ I ∨ a ∈ I ^ n
Tactic: rw [or_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hI : I ≠ 0
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
⊢ Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) = Multiset.count J (normalizedFactors I)
have hI₁ : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
Tactic: replace hI : Associates.mk I ≠ 0 := Associates.mk_ne_zero.mpr hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
⊢ Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) = Multiset.count J (normalizedFactors I)
have hJ' : Irreducible (M := Associates (Ideal R)) (Associates.mk J)
Tactic: have hJ' : Irreducible (Associates.mk J) := by
    simpa only [Associates.irreducible_mk] using (prime_of_isPrime hJ₀ hJ).irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
hJ' : Irreducible (M := Associates (Ideal R)) (Associates.mk J)
⊢ Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) = Multiset.count J (normalizedFactors I)
have apply : I ≤ J ^ Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
Tactic: apply (count_normalizedFactors_eq (p := J) (x := I) _ _).symm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
hJ' : Irreducible (M := Associates (Ideal R)) (Associates.mk J)
apply : I ≤ J ^ Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
⊢ Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) = Multiset.count J (normalizedFactors I)
have apply₁ : ¬I ≤ J ^ (Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) + 1)
Tactic: apply (count_normalizedFactors_eq (p := J) (x := I) _ _).symm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
hJ' : Irreducible (M := Associates (Ideal R)) (Associates.mk J)
⊢ I ≤ J ^ Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
have rw : HPow.hPow (α := Associates (Ideal R)) (Associates.mk J)
    (Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))) ∣
  Associates.mk I
Tactic: rw [← dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
hJ' : Irreducible (M := Associates (Ideal R)) (Associates.mk J)
⊢ HPow.hPow (α := Associates (Ideal R)) (Associates.mk J)
      (Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))) ≤
    Associates.mk I
have rw : Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) ≤
  Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
Tactic: rw [Associates.prime_pow_dvd_iff_le hI hJ']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
hJ' : Irreducible (M := Associates (Ideal R)) (Associates.mk J)
⊢ ¬I ≤ J ^ (Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) + 1)
have rw : ¬HPow.hPow (α := Associates (Ideal R)) (Associates.mk J)
      (Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) + 1) ∣
    Associates.mk I
Tactic: rw [← dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Ne (α := Associates (Ideal R)) (Associates.mk I) 0
hJ' : Irreducible (M := Associates (Ideal R)) (Associates.mk J)
⊢ ¬HPow.hPow (α := Associates (Ideal R)) (Associates.mk J)
        (Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) + 1) ≤
      Associates.mk I
have rw : ¬Associates.count (Associates.mk J) (Associates.factors (Associates.mk I)) + 1 ≤
    Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
Tactic: rw [Associates.prime_pow_dvd_iff_le hI hJ']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a₀}))) = n
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := Prime.ne_zero hx
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a₀}))) = n
have hp : Irreducible (M := Ideal R) (span {x})
Tactic: rw [count_associates_factors_eq, UniqueFactorizationMonoid.count_normalizedFactors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
hp : Irreducible (M := Ideal R) (span {x})
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a₀}))) = n
have hnorm : Eq (α := Ideal R) ((normalize : (a : Ideal R) → Ideal R) (span {x}) : Ideal R) (span {x} : Ideal R)
Tactic: rw [count_associates_factors_eq, UniqueFactorizationMonoid.count_normalizedFactors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
hp : Irreducible (M := Ideal R) (span {x})
hnorm : Eq (α := Ideal R) ((normalize : (a : Ideal R) → Ideal R) (span {x}) : Ideal R) (span {x} : Ideal R)
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a₀}))) = n
have hle : HPow.hPow (α := Ideal R) (span {x}) n ∣ span {a₀}
Tactic: rw [count_associates_factors_eq, UniqueFactorizationMonoid.count_normalizedFactors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
hp : Irreducible (M := Ideal R) (span {x})
hnorm : Eq (α := Ideal R) ((normalize : (a : Ideal R) → Ideal R) (span {x}) : Ideal R) (span {x} : Ideal R)
hle : HPow.hPow (α := Ideal R) (span {x}) n ∣ span {a₀}
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a₀}))) = n
have hlt : ¬HPow.hPow (α := Ideal R) (span {x}) (n + 1) ∣ span {a₀}
Tactic: rw [count_associates_factors_eq, UniqueFactorizationMonoid.count_normalizedFactors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
hp : Irreducible (M := Ideal R) (span {x})
hnorm : Eq (α := Ideal R) ((normalize : (a : Ideal R) → Ideal R) (span {x}) : Ideal R) (span {x} : Ideal R)
hle : HPow.hPow (α := Ideal R) (span {x}) n ∣ span {a₀}
hlt : ¬HPow.hPow (α := Ideal R) (span {x}) (n + 1) ∣ span {a₀}
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a₀}))) = n
have hI : Ne (α := Ideal R) (span {a₀}) 0
Tactic: rw [count_associates_factors_eq, UniqueFactorizationMonoid.count_normalizedFactors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
hp : Irreducible (M := Ideal R) (span {x})
hnorm : Eq (α := Ideal R) ((normalize : (a : Ideal R) → Ideal R) (span {x}) : Ideal R) (span {x} : Ideal R)
hle : HPow.hPow (α := Ideal R) (span {x}) n ∣ span {a₀}
hlt : ¬HPow.hPow (α := Ideal R) (span {x}) (n + 1) ∣ span {a₀}
hI : Ne (α := Ideal R) (span {a₀}) 0
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a₀}))) = n
have hJ : IsPrime (α := R) (span {x})
Tactic: rw [count_associates_factors_eq, UniqueFactorizationMonoid.count_normalizedFactors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
hp : Irreducible (M := Ideal R) (span {x})
hnorm : Eq (α := Ideal R) ((normalize : (a : Ideal R) → Ideal R) (span {x}) : Ideal R) (span {x} : Ideal R)
hle : HPow.hPow (α := Ideal R) (span {x}) n ∣ span {a₀}
hlt : ¬HPow.hPow (α := Ideal R) (span {x}) (n + 1) ∣ span {a₀}
hI : Ne (α := Ideal R) (span {a₀}) 0
hJ : IsPrime (α := R) (span {x})
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a₀}))) = n
have hJ₀ : Ne (α := Ideal R) (span {x}) ⊥
Tactic: rw [count_associates_factors_eq, UniqueFactorizationMonoid.count_normalizedFactors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ HPow.hPow (α := Ideal R) (span {x}) n ∣ span {a₀}
have hle : Membership.mem (γ := Ideal R) (span {x ^ n}) (x ^ n * a)
Tactic: simp only [span_singleton_pow, heq, dvd_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ ¬HPow.hPow (α := Ideal R) (span {x}) (n + 1) ∣ span {a₀}
have hlt : ¬x ^ (n + 1) ∣ x ^ n * a
Tactic: simp only [span_singleton_pow, heq, dvd_span_singleton, mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ Ne (α := Ideal R) (span {a₀}) 0
have hI : ¬a₀ = 0
Tactic: simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ Ne (α := Ideal R) (span {x}) ⊥
have hJ₀ : ¬x = 0
Tactic: simp only [ne_eq, span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
hle : x ^ n ∣ a
hlt : ¬x ^ (n + 1) ∣ a
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a}))) = n
have obtain : ∀ (q : R) (hq : a = x ^ n * q),
  Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a}))) = n
Tactic: obtain ⟨q, hq⟩ := hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
hlt : ¬x ^ (n + 1) ∣ a
q : R
hq : a = x ^ n * q
⊢ Associates.count (α := Ideal R) (Associates.mk (span {x})) (Associates.factors (Associates.mk (span {a}))) = n
have apply : ¬x ∣ q
Tactic: apply count_associates_eq hx _ hq
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
hlt : ¬x ^ (n + 1) ∣ a
q : R
hq : a = x ^ n * q
⊢ ¬x ∣ q
have contrapose : ∀ (hdvd : x ∣ q), x ^ (n + 1) ∣ a
Tactic: contrapose hlt with hdvd
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
hdvd : x ∣ q
⊢ x ^ (n + 1) ∣ a
have obtain : ∀ (q' : R) (hq' : q = x * q'), x ^ (n + 1) ∣ a
Tactic: obtain ⟨q', hq'⟩ := hdvd
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
q' : R
hq' : q = x * q'
⊢ x ^ (n + 1) ∣ a
have h : a = x ^ (n + 1) * q'
Tactic: use q'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
q' : R
hq' : q = x * q'
⊢ a = x ^ (n + 1) * q'
have h : x ^ n * (x * q') = x ^ (n + 1) * q'
Tactic: rw [hq, hq']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), J ≤ P → K ≤ P → ¬P.IsPrime
hJ : I ≤ J
hK : I ≤ K
⊢ I ≤ J * K
have simp : ∀ (coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime) (hJ : J ∣ I) (hK : K ∣ I), J * K ∣ I
Tactic: simp only [← dvd_iff_le] at coprime hJ hK ⊢
Cleared hypotheses: coprime, hJ, hK
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ : J ∣ I
hK : K ∣ I
⊢ J * K ∣ I
have pos : ∀ (hJ0 : J = 0), J * K ∣ I
Tactic: by_cases hJ0 : J = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ : J ∣ I
hK : K ∣ I
pos : ∀ (hJ0 : J = 0), J * K ∣ I
⊢ J * K ∣ I
have neg : ∀ (hJ0 : ¬J = 0), J * K ∣ I
Tactic: by_cases hJ0 : J = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ : J ∣ I
hK : K ∣ I
hJ0 : ¬J = 0
⊢ J * K ∣ I
have neg : ∀ (I' : Ideal R) (hJ : J ∣ K * I'), J * K ∣ K * I'
Tactic: obtain ⟨I', rfl⟩ := hK
Cleared hypotheses: I, hJ, hK
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ J * K ∣ K * I'
have neg : K * J ∣ K * I'
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ K * J ∣ K * I'
have neg : ∀ {d : Ideal R}, d ∣ J → d ∣ K → ¬Prime d
Tactic: refine mul_dvd_mul_left K
    (UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors (b := K) hJ0 ?_ hJ)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ Eq.{u_1 + 1} (α := Ideal R) (s.inf fun (i : ι) ↦ (f i).asIdeal ^ e i) (∏ i ∈ s, (f i).asIdeal ^ e i)
have rw : Eq.{u_1 + 1} (α := Ideal R) (s.inf fun (i : ι) ↦ (f i).asIdeal ^ e i) (⨅ i ∈ s, (f i).asIdeal ^ e i)
Tactic: rw [prod_eq_iInf_of_pairwise_isCoprime]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
rw : Eq.{u_1 + 1} (α := Ideal R) (s.inf fun (i : ι) ↦ (f i).asIdeal ^ e i) (⨅ i ∈ s, (f i).asIdeal ^ e i)
⊢ Eq.{u_1 + 1} (α := Ideal R) (s.inf fun (i : ι) ↦ (f i).asIdeal ^ e i) (∏ i ∈ s, (f i).asIdeal ^ e i)
have rw₁ : (↑s : Set ι).Pairwise (Function.onFun.{u_4 + 1, u_1 + 1, 1} (β := Ideal R) IsCoprime fun (i : ι) ↦ (f i).asIdeal ^ e i)
Tactic: rw [prod_eq_iInf_of_pairwise_isCoprime]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ Eq.{u_1 + 1} (α := Ideal R) (s.inf fun (i : ι) ↦ (f i).asIdeal ^ e i) (⨅ i ∈ s, (f i).asIdeal ^ e i)
have rw : Eq.{u_1 + 1} (α := Ideal R) (⨅ a ∈ s, (f a).asIdeal ^ e a) (⨅ i ∈ s, (f i).asIdeal ^ e i)
Tactic: rw [Finset.inf_eq_iInf s fun i ↦ (f i).asIdeal ^ e i]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ Eq.{u_1 + 1} (α := Ideal R) (s.inf fun (i : ι) ↦ f i ^ e i) (∏ i ∈ s, f i ^ e i)
have rw : (↑s : Set ι).Pairwise (Function.onFun.{u_4 + 1, u_1 + 1, 1} (β := Ideal R) IsCoprime fun (i : ι) ↦ f i ^ e i)
Tactic: rw [prod_eq_iInf_of_pairwise_isCoprime, Finset.inf_eq_iInf s fun i ↦ (f i) ^ e i]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
ι : ?m.1
inst_3 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ Multiset.prod (Multiset.map (fun (P : Ideal R) ↦ P) (factors I)) = (factors I).prod
have rw : (factors I).prod = (factors I).prod
Tactic: rw [Multiset.map_id']