awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
h : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
h₃ :
  ∀ (Q : Ideal S) (h₁ : Q.IsMaximal) (h₂ : Eq (α := Ideal ℤ) (under ℤ Q) (span {p})) (h₃ : Q ∣ I),
    ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I

Tactic:
obtain ⟨Q, h₁, h₂, h₃⟩ := IH h
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
h : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
Q : Ideal S
h₁ : Q.IsMaximal
h₂ : Eq (α := Ideal ℤ) (under ℤ Q) (span {p})
h₃ : Q ∣ I
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I

Tactic:
⟨Q, h₁, h₂, dvd_mul_of_dvd_right h₃ _⟩

Premises used: dvd_mul_of_dvd_right, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
h : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
Q : Ideal S
h₁ : Q.IsMaximal
h₂ : Eq (α := Ideal ℤ) (under ℤ Q) (span {p})
h₃ : Q ∣ I
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I

Tactic:
exact ⟨Q, h₁, h₂, dvd_mul_of_dvd_right h₃ _⟩
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
⊢ P.IsMaximal

Tactic:
have := (Ideal.isPrime_of_prime hP).isMaximal hP.ne_zero
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
this : P.IsMaximal
⊢ Ne (α := Ideal ℤ) (under ℤ P) ⊤

Tactic:
simpa using this.ne_top

Premises used: Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
this : P.IsMaximal
h₃ : LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I

Tactic:
refine ⟨P, this, (hpMax.eq_of_le (by simpa using this.ne_top) ?_).symm, dvd_mul_right _ _⟩
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
this : P.IsMaximal
h₃ :
  ∀ (q n : ℕ) (hn : 0 < n) (hqP : (↑q : S) ∈ P) (hq : Nat.Prime q) (H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n),
    LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
⊢ LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)

Tactic:
obtain ⟨q, n, hn, hqP, hq, H⟩ := Ideal.exists_prime_and_absNorm_eq_pow P

Premises used: Ideal.exists_prime_and_absNorm_eq_pow
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
⊢ ∃ i ≤ n, Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) i)

Tactic:
rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI

Premises used: Nat.prime_iff_prime_int, Iff.mp, dvd_prime_pow, Nat.cast_pow
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
hI₁ : ∃ i ≤ n, Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) i)
⊢ 0 < n

Tactic:
rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI

Premises used: Nat.prime_iff_prime_int, Iff.mp, dvd_prime_pow, Nat.cast_pow
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
hI₁ : ∃ i ≤ n, Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) i)
hn₁ : 0 < n
⊢ (↑q : S) ∈ P

Tactic:
rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI

Premises used: Nat.prime_iff_prime_int, Iff.mp, dvd_prime_pow, Nat.cast_pow
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
hI₁ : ∃ i ≤ n, Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) i)
hn₁ : 0 < n
hqP₁ : (↑q : S) ∈ P
⊢ Nat.Prime q

Tactic:
rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI

Premises used: Nat.prime_iff_prime_int, Iff.mp, dvd_prime_pow, Nat.cast_pow
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
hI₁ : ∃ i ≤ n, Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) i)
hn₁ : 0 < n
hqP₁ : (↑q : S) ∈ P
hq₁ : Nat.Prime q
⊢ (absNorm : (a : Ideal S) → ℕ) P = q ^ n

Tactic:
rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI

Premises used: Nat.prime_iff_prime_int, Iff.mp, dvd_prime_pow, Nat.cast_pow
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hI : ∃ i ≤ n, Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) i)
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
h₃ :
  ∀ (m : ℕ) (hmn : m ≤ n) (hp : Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) m)),
    LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
⊢ LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)

Tactic:
obtain ⟨m, hmn, hp⟩ := hI
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp_1 : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) m)
h₃ : Membership.mem (γ := Ideal ℤ) (under ℤ P) p
⊢ LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)

Tactic:
rw [Ideal.span_singleton_le_iff_mem]

Premises used: Ideal.span_singleton_le_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp_1 : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) m)
h : m = 0
⊢ IsUnit p

Tactic:
simpa [h] using hp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp_1 : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) m)
⊢ m ≠ 0

Tactic:
have : m ≠ 0 := fun h ↦ hpMax.ne_top (Ideal.span_singleton_eq_top.mpr (by simpa [h] using hp))
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp_1 : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
this_3 : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) m)
this : m ≠ 0
⊢ Membership.mem (γ := Ideal ℤ) (under ℤ P) (↑q : ℤ)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp_1 : Prime p
this_1 : IsAddTorsionFree S
this_2 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
this_3 : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : (↑q : S) ∈ P
hq : Nat.Prime q
H : (absNorm : (a : Ideal S) → ℕ) P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) m)
this : m ≠ 0
⊢ Membership.mem (γ := Ideal ℤ) (under ℤ P) p

Tactic:
exact Ideal.mem_of_dvd _ hp.symm.dvd (Ideal.pow_mem_of_mem _ (by simpa) _ this.bot_lt)

Premises used: Associated.dvd, Ideal.mem_of_dvd, Ideal.pow_mem_of_mem, Associated.symm, Ne.bot_lt
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ) ∨ p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
h₃ :
  ∀ (h : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
h₄ :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ)),
    ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I

Tactic:
cases hI with
    | inr h =>
      obtain ⟨Q, h₁, h₂, h₃⟩ := IH h
      exact ⟨Q, h₁, h₂, dvd_mul_of_dvd_right h₃ _⟩
    | inl hI =>
      have := (Ideal.isPrime_of_prime hP).isMaximal hP.ne_zero
      refine ⟨P, this, (hpMax.eq_of_le (by simpa using this.ne_top) ?_).symm, dvd_mul_right _ _⟩
      obtain ⟨q, n, hn, hqP, hq, H⟩ := Ideal.exists_prime_and_absNorm_eq_pow P
      rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI
      obtain ⟨m, hmn, hp⟩ := hI
      rw [Ideal.span_singleton_le_iff_mem]
      have : m ≠ 0 := fun h ↦ hpMax.ne_top (Ideal.span_singleton_eq_top.mpr (by simpa [h] using hp))
      exact Ideal.mem_of_dvd _ hp.symm.dvd (Ideal.pow_mem_of_mem _ (by simpa) _ this.bot_lt)

Premises used: Ideal.span_singleton_le_iff_mem, Nat.cast_pow
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℤ
hp : Prime p
I : Ideal S
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
h₁ :
  ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) 0) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ 0
h₂ :
  ∀ (I : Ideal S) (hI' : IsUnit I) (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
    ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
h₃ :
  ∀ (I P : Ideal S) (hI' : I ≠ 0) (hP : Prime P)
    (IH :
      ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)),
        ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I)
    (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) (P * I)) : ℤ)),
    ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I

Tactic:
induction I using UniqueFactorizationMonoid.induction_on_prime with
  | h₁ =>
    obtain ⟨Q, hQ, e⟩ := Ideal.exists_ideal_over_maximal_of_isIntegral (S := S) (Ideal.span {p})
      (fun x ↦ by simp +contextual)
    exact ⟨Q, hQ, e, dvd_zero _⟩
  | h₂ I hI' =>
    obtain rfl : I = ⊤ := by simpa using hI'
    cases hp.not_dvd_one (by simpa using hI)
  | h₃ I P hI' hP IH =>
    simp only [_root_.map_mul, Nat.cast_mul, hp.dvd_mul] at hI
    cases hI with
    | inr h =>
      obtain ⟨Q, h₁, h₂, h₃⟩ := IH h
      exact ⟨Q, h₁, h₂, dvd_mul_of_dvd_right h₃ _⟩
    | inl hI =>
      have := (Ideal.isPrime_of_prime hP).isMaximal hP.ne_zero
      refine ⟨P, this, (hpMax.eq_of_le (by simpa using this.ne_top) ?_).symm, dvd_mul_right _ _⟩
      obtain ⟨q, n, hn, hqP, hq, H⟩ := Ideal.exists_prime_and_absNorm_eq_pow P
      rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI
      obtain ⟨m, hmn, hp⟩ := hI
      rw [Ideal.span_singleton_le_iff_mem]
      have : m ≠ 0 := fun h ↦ hpMax.ne_top (Ideal.span_singleton_eq_top.mpr (by simpa [h] using hp))
      exact Ideal.mem_of_dvd _ hp.symm.dvd (Ideal.pow_mem_of_mem _ (by simpa) _ this.bot_lt)

Premises used: Prime.dvd_mul, Prime.not_dvd_one, Ideal.span_singleton_le_iff_mem, map_mul, Nat.cast_mul, Ideal.exists_ideal_over_maximal_of_isIntegral, Ideal.span, Nat.cast_pow, Singleton.singleton, rfl
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℕ
hp : Nat.Prime p
I : Ideal S
hI : p ∣ (absNorm : (a : Ideal S) → ℕ) I
⊢ Nat.Prime (Int.natAbs (↑p : ℤ))

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
p : ℕ
hp : Nat.Prime p
I : Ideal S
hI : p ∣ (absNorm : (a : Ideal S) → ℕ) I
⊢ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)

Tactic:
exact_mod_cast hI
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
inst_5 : CharZero S
n : ℕ
inl : ∀ (hn : n = 0), Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}
inr : ∀ (hn : n > 0), Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}
⊢ Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}

Tactic:
obtain hn | hn := Nat.eq_zero_or_pos n

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
inst_5 : CharZero S
n : ℕ
hn : n = 0
⊢ Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}

Tactic:
simp only [hn, absNorm_eq_zero_iff, Set.setOf_eq_eq_singleton, Set.finite_singleton]

Premises used: Set.setOf_eq_eq_singleton, Ideal.absNorm_eq_zero_iff, Set.finite_singleton
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
⊢ Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}

Tactic:
Set.Finite.of_finite_image (f := f) ?_ ?_

Premises used: Set.Finite.of_finite_image
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
inr : (f '' {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}).Finite
inr₁ : Set.InjOn f {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}
⊢ Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}

Tactic:
refine Set.Finite.of_finite_image (f := f) ?_ ?_

Premises used: Set.Finite.of_finite_image
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
this : Finite.{u_1 + 1} (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)}))
g : Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) →
  Set (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  SetLike.coe
⊢ (f '' {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}).Finite

Tactic:
Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn

Premises used: Function.Injective.injOn, SetLike.coe_injective, Set.Finite.of_finite_image
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
this : Finite.{u_1 + 1} (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)}))
g : Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) →
  Set (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  SetLike.coe
refine : (g '' f '' {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}).Finite
⊢ (f '' {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}).Finite

Tactic:
refine Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn

Premises used: Function.Injective.injOn, SetLike.coe_injective, Set.Finite.of_finite_image