awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
x y : A
hxy : x * y ∈ P
refine_2 : ∀ (hxy : P ∣ HMul.hMul (α := Ideal A) (span {x}) (span {y})), P ∣ span {x} ∨ P ∣ span {y}
⊢ x ∈ P ∨ y ∈ P

Tactic:
simp only [← dvd_span_singleton, ← span_singleton_mul_span_singleton] at hxy ⊢

Premises used: Ideal.span_singleton_mul_span_singleton, Ideal.dvd_span_singleton
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
x y : A
hxy : P ∣ HMul.hMul (α := Ideal A) (span {x}) (span {y})
⊢ P ∣ span {x} ∨ P ∣ span {y}

Tactic:
h.dvd_or_dvd hxy

Premises used: Prime.dvd_or_dvd, Set.Mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
x y : A
hxy : P ∣ HMul.hMul (α := Ideal A) (span {x}) (span {y})
⊢ P ∣ span {x} ∨ P ∣ span {y}

Tactic:
exact h.dvd_or_dvd hxy

Premises used: Prime.dvd_or_dvd
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
⊢ Prime P

Tactic:
⟨hP, mt isUnit_iff.mp h.ne_top, fun I J hIJ => ?_⟩

Premises used: Prime, mt, And.intro, Ideal.isUnit_iff, Iff.mp, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
refine : ∀ (I J : Ideal A) (hIJ : P ∣ I * J), P ∣ I ∨ P ∣ J
⊢ Prime P

Tactic:
refine ⟨hP, mt isUnit_iff.mp h.ne_top, fun I J hIJ => ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
I J : Ideal A
hIJ : P ∣ I * J
⊢ P ∣ I ∨ P ∣ J

Tactic:
simpa only [dvd_iff_le] using h.mul_le.mp (le_of_dvd hIJ)

Premises used: Ideal.dvd_iff_le, Ideal.le_of_dvd, Ideal.IsPrime.mul_le, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
R : Type u_4
inst_2 : CommRing R
inst_3 : Algebra R A
p : Ideal R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
hP : Membership.mem (γ := Set (Ideal A)) (p.primesOver A) P
⊢ Prime P

Tactic:
prime_of_isPrime (ne_bot_of_mem_primesOver hp hP) hP.1

Premises used: Ideal.ne_bot_of_mem_primesOver, And.left, Ideal.prime_of_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
⊢ Prime P ↔ P.IsPrime

Tactic:
⟨isPrime_of_prime, prime_of_isPrime hP⟩

Premises used: Iff.intro, Ideal.isPrime_of_prime, Ideal.prime_of_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
⊢ P.IsPrime ↔ P = ⊥ ∨ Prime P

Tactic:
⟨fun hp => (eq_or_ne P ⊥).imp_right fun hp0 => prime_of_isPrime hp0 hp, fun hp =>
    hp.elim (fun h => h.symm ▸ isPrime_bot) isPrime_of_prime⟩

Premises used: Eq.rec, Bot.bot, Ideal.isPrime_bot, Iff.intro, eq_or_ne, Ideal.isPrime_of_prime, Or.elim, Eq.symm, Or.imp_right, Ideal.prime_of_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
inl : Prime (M := Ideal A) (span {0}) ↔ Prime.{u_2} (M := A) 0
inr : ∀ (ha : a ≠ 0), Prime (M := Ideal A) (span {a}) ↔ Prime a
⊢ Prime (M := Ideal A) (span {a}) ↔ Prime a

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
inl : ¬Prime.{u_2} (M := Ideal A) 0 ↔ ¬Prime.{u_2} (M := A) 0
⊢ Prime (M := Ideal A) (span {0}) ↔ Prime.{u_2} (M := A) 0

Tactic:
rw [Set.singleton_zero, span_zero, ← zero_eq_bot, ← not_iff_not]

Premises used: not_iff_not, Ideal.zero_eq_bot, Ideal.span_zero, Set.singleton_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
⊢ ¬Prime.{u_2} (M := Ideal A) 0 ↔ ¬Prime.{u_2} (M := A) 0

Tactic:
simp only [not_prime_zero, not_false_eq_true]

Premises used: not_prime_zero, not_false_eq_true
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ Ne (α := Ideal A) (span {a}) ⊥

Tactic:
simpa only [ne_eq, span_singleton_eq_bot] using ha

Premises used: Ideal.span_singleton_eq_bot, ne_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ Ne (α := Ideal A) (span {a}) ⊥

Tactic:
have ha' : span {a} ≠ ⊥ := by simpa only [ne_eq, span_singleton_eq_bot] using ha
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
ha : a ≠ 0
ha' : Ne (α := Ideal A) (span {a}) ⊥
inr : IsPrime (α := A) (span {a}) ↔ Prime a
inr₁ inr₂ : Prime a ↔ Prime a
⊢ Prime (M := Ideal A) (span {a}) ↔ Prime a

Tactic:
rw [prime_iff_isPrime ha', span_singleton_prime ha]

Premises used: Ideal.prime_iff_isPrime, Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
inst_2 : Submodule.IsPrincipal P
⊢ Prime (generator P)

Tactic:
have : IsPrime P := isPrime_of_prime h
  prime_generator_of_isPrime _ h.ne_zero

Premises used: Submodule.IsPrincipal.prime_generator_of_isPrime, Prime.ne_zero, Ideal.isPrime_of_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
rw : p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p

Tactic:
rw [← dvd_iff_le]

Premises used: Ideal.dvd_iff_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
pos : ∀ (hp : p = 0), p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
neg : ∀ (hp : ¬p = 0), p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : p = 0
⊢ I ≠ 0

Tactic:
rw [← zero_eq_bot] at hI

Premises used: Ideal.zero_eq_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : p = 0
hI₁ : I ≠ 0
⊢ p = 0

Tactic:
rw [← zero_eq_bot] at hI

Premises used: Ideal.zero_eq_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ 0
hp : p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
simp only [hp, zero_notMem_normalizedFactors, zero_dvd_iff, hI, false_iff, not_and,
      not_false_eq_true, implies_true]

Premises used: zero_dvd_iff, false_iff, implies_true, not_false_eq_true, not_and, UniqueFactorizationMonoid.zero_notMem_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
neg : Prime p ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I
neg₁ : p.IsPrime ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I
neg₂ : p ≠ ⊥
neg₃ : p.IsPrime ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I
neg₄ neg₅ neg₆ : p ≠ ⊥
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
rwa [mem_normalizedFactors_iff hI, prime_iff_isPrime]

Premises used: Ideal.mem_normalizedFactors_iff, Ideal.prime_iff_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst_3 : Algebra R A
inst_4 : IsDomain R
inst_5 : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
rw : P.IsPrime → (p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P)
⊢ Membership.mem (γ := Set (Ideal A)) (p.primesOver A) P ↔
    Membership.mem (γ := Multiset (Ideal A)) (normalizedFactors (map (F := R →+* A) (algebraMap R A) p)) P

Tactic:
rw [primesOver, Set.mem_setOf_eq, mem_normalizedFactors_iff (map_ne_bot_of_ne_bot hp),
    liesOver_iff, under_def, and_congr_right_iff, map_le_iff_le_comap]

Premises used: Ideal.primesOver, Ideal.liesOver_iff, Set.mem_setOf_eq, and_congr_right_iff, Ideal.map_le_iff_le_comap, Ideal.mem_normalizedFactors_iff, Ideal.under_def, Ideal.map_ne_bot_of_ne_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst_3 : Algebra R A
inst_4 : IsDomain R
inst_5 : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
hP : P.IsPrime
⊢ p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P

Tactic:
⟨fun h ↦ le_of_eq h, fun h' ↦ ((IsCoatom.le_iff_eq (isMaximal_def.mp h) ?_).mp h').symm⟩

Premises used: Iff.intro, Iff.mp, IsCoatom.le_iff_eq, le_of_eq, Eq.symm, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst_3 : Algebra R A
inst_4 : IsDomain R
inst_5 : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
hP : P.IsPrime
refine :
  ∀ (h' : p ≤ comap (F := R →+* A) (algebraMap R A) P), Ne (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) P) ⊤
⊢ p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P

Tactic:
refine ⟨fun h ↦ le_of_eq h, fun h' ↦ ((IsCoatom.le_iff_eq (isMaximal_def.mp h) ?_).mp h').symm⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst_3 : Algebra R A
inst_4 : IsDomain R
inst_5 : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
hP : P.IsPrime
h' : p ≤ comap (F := R →+* A) (algebraMap R A) P
⊢ Ne (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) P) ⊤

Tactic:
comap_ne_top (algebraMap R A) (IsPrime.ne_top hP)

Premises used: Algebra.algebraMap, Ideal.comap_ne_top, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst_3 : Algebra R A
inst_4 : IsDomain R
inst_5 : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
hP : P.IsPrime
h' : p ≤ comap (F := R →+* A) (algebraMap R A) P
⊢ Ne (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) P) ⊤

Tactic:
exact comap_ne_top (algebraMap R A) (IsPrime.ne_top hP)

Premises used: Algebra.algebraMap, Ideal.comap_ne_top, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
⊢ StrictAnti.{0, u_2} (β := Ideal A) fun (x : ℕ) ↦ I ^ x

Tactic:
strictAnti_nat_of_succ_lt fun e =>
    dvdNotUnit_iff_lt.mp ⟨pow_ne_zero _ hI0, I, mt isUnit_iff.mp hI1, pow_succ I e⟩

Premises used: pow_succ, pow_ne_zero, mt, And.intro, Exists.intro, Ideal.isUnit_iff, Iff.mp, strictAnti_nat_of_succ_lt, Ideal.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ LT.lt.{u_2} (α := Ideal A) ((fun (x : ℕ) ↦ I ^ x) e) ((fun (x : ℕ) ↦ I ^ x) 1)

Tactic:
I.pow_right_strictAnti hI0 hI1 he

Premises used: Ideal.pow_right_strictAnti
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
h : I = (fun (x : ℕ) ↦ I ^ x) 1
⊢ I ^ e < I

Tactic:
convert! I.pow_right_strictAnti hI0 hI1 he

Premises used: Ideal.pow_right_strictAnti
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
h h₁ : I = I
⊢ I = HPow.hPow (β := ℕ) I 1

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
⊢ ∃ x ∈ I ^ e, x ∉ I ^ (e + 1)

Tactic:
SetLike.exists_of_lt (I.pow_right_strictAnti hI0 hI1 e.lt_succ_self)

Premises used: SetLike.exists_of_lt, Nat.lt_succ_self, Ideal.pow_right_strictAnti
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
⊢ I = P ^ i

Tactic:
le_antisymm hle ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
refine : P ^ i ≤ I
⊢ I = P ^ i

Tactic:
refine le_antisymm hle ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
⊢ Prime P

Tactic:
have P_prime' := prime_of_isPrime hP P_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
⊢ I ≠ ⊥

Tactic:
have h1 : I ≠ ⊥ := (lt_of_le_of_lt bot_le hlt).ne'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
⊢ P ^ i ≠ 0

Tactic:
have := pow_ne_zero i hP
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
⊢ P ^ (i + 1) ≠ 0

Tactic:
have h3 := pow_ne_zero (i + 1) hP
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)

Tactic:
rw [← dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
    normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
    Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt

Premises used: Prime.irreducible, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Ideal.dvdNotUnit_iff_lt, Multiset.lt_replicate_succ, UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
hlt₁ : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
⊢ I ≤ P ^ i

Tactic:
rw [← dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
    normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
    Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt

Premises used: Prime.irreducible, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Ideal.dvdNotUnit_iff_lt, Multiset.lt_replicate_succ, UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
hlt₁ : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle₁ : I ≤ P ^ i
⊢ Prime P

Tactic:
rw [← dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
    normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
    Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt

Premises used: Prime.irreducible, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Ideal.dvdNotUnit_iff_lt, Multiset.lt_replicate_succ, UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
hlt₁ : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle₁ : I ≤ P ^ i
P_prime'₁ : Prime P
⊢ I ≠ ⊥

Tactic:
rw [← dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
    normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
    Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt

Premises used: Prime.irreducible, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Ideal.dvdNotUnit_iff_lt, Multiset.lt_replicate_succ, UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
hlt₁ : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle₁ : I ≤ P ^ i
P_prime'₁ : Prime P
h1₁ : I ≠ ⊥
⊢ P ^ i ≠ 0

Tactic:
rw [← dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
    normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
    Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt

Premises used: Prime.irreducible, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Ideal.dvdNotUnit_iff_lt, Multiset.lt_replicate_succ, UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
hlt₁ : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle₁ : I ≤ P ^ i
P_prime'₁ : Prime P
h1₁ : I ≠ ⊥
this₁ : P ^ i ≠ 0
⊢ P ^ (i + 1) ≠ 0

Tactic:
rw [← dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
    normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
    Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt

Premises used: Prime.irreducible, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Ideal.dvdNotUnit_iff_lt, Multiset.lt_replicate_succ, UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
rw : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hx : I ≠ 0
hy : P ^ i ≠ 0
⊢ P ^ i ≤ I

Tactic:
rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors, normalizedFactors_pow,
    normalizedFactors_irreducible P_prime'.irreducible, Multiset.nsmul_singleton]

Premises used: Prime.irreducible, Ideal.dvd_iff_le, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)

Tactic:
assumption
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ I ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
⊢ P ^ (i + 1) < P ^ i

Tactic:
lt_of_le_of_ne (pow_le_pow_right (Nat.le_succ _))
    (mt (pow_inj_of_not_isUnit (mt isUnit_iff.mp P_prime.ne_top) hP).mp i.succ_ne_self)

Premises used: Nat.succ_ne_self, mt, Nat.le_succ, Ideal.pow_le_pow_right, Ideal.isUnit_iff, Iff.mp, Ideal.IsPrime.ne_top, pow_inj_of_not_isUnit, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
x : A
n : ℕ
I : Ideal A
simp_rw : HPow.hPow (α := Associates (Ideal A)) (Associates.mk I) n ∣ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n
simp_rw₁ : Dvd.dvd (α := Associates (Ideal A)) (Associates.mk (I ^ n)) (Associates.mk (Ideal.span {x})) ↔ x ∈ I ^ n
simp_rw₂ : I ^ n ∣ Ideal.span {x} ↔ x ∈ I ^ n
⊢ HPow.hPow (α := Associates (Ideal A)) (Associates.mk I) n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n

Tactic:
simp_rw [← Associates.dvd_eq_le, ← Associates.mk_pow, Associates.mk_dvd_mk,
    Ideal.dvd_span_singleton]

Premises used: Associates.dvd_eq_le, Associates.mk_pow, Associates.mk_dvd_mk, Ideal.dvd_span_singleton
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
rw : I ≤ 1 / J ↔ J ≤ I⁻¹
rw₁ : I ≤ 1 / J ↔ J ≤ 1 / I
rw₂ : I ≤ 1 / J ↔ J * I ≤ 1
rw₃ : I * J ≤ 1 ↔ J * I ≤ 1
rw₄ rw₅ : J * I ≤ 1 ↔ J * I ≤ 1
⊢ I ≤ J⁻¹ ↔ J ≤ I⁻¹

Tactic:
rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]

Premises used: FractionalIdeal.le_div_iff_mul_le, FractionalIdeal.inv_eq, mul_comm