awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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 : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this_2 : CharZero S
this_3 : Finite.{u_1 + 1} (S ⧸ P)
val : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP.{u_1} (S ⧸ P) p
n : ℕ+
hp : Nat.Prime p
e : Fintype.card.{u_1} (S ⧸ P) = p ^ (↑n : ℕ)
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
have hP : (absNorm : (a : Ideal S) → ℕ) P = p ^ (↑n : ℕ)
Tactic: have hP : P.absNorm = p ^ (n : ℕ) := (Nat.card_eq_fintype_card.trans e:)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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 : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this_2 : CharZero S
this_3 : Finite.{u_1 + 1} (S ⧸ P)
val : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP.{u_1} (S ⧸ P) p
n : ℕ+
hp : Nat.Prime p
e : Fintype.card.{u_1} (S ⧸ P) = p ^ (↑n : ℕ)
hP : (absNorm : (a : Ideal S) → ℕ) P = p ^ (↑n : ℕ)
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
have intro : (↑p : S) ∈ P
Tactic: refine ⟨p, n, n.2, ?_, hp, hP⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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 : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this_2 : CharZero S
this_3 : Finite.{u_1 + 1} (S ⧸ P)
val : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP.{u_1} (S ⧸ P) p
n : ℕ+
hp : Nat.Prime p
e : Fintype.card.{u_1} (S ⧸ P) = p ^ (↑n : ℕ)
hP : (absNorm : (a : Ideal S) → ℕ) P = p ^ (↑n : ℕ)
⊢ (↑p : S) ∈ P
have intro : (↑((absNorm : (a : Ideal S) → ℕ) P) : S) ∈ P
Tactic: rw [← Ideal.IsPrime.pow_mem_iff_mem (I := P) inferInstance _ n.pos, ← Nat.cast_pow, ← hP]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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) : ℤ)
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
have this : IsAddTorsionFree S
Tactic: have : IsAddTorsionFree S := .of_isTorsionFree ℤ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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 : IsAddTorsionFree S
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
have this₁ : CharZero S
Tactic: have := CharZero.of_isAddTorsionFree S S
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
have hpMax : IsMaximal (α := ℤ) (span {p})
Tactic: have hpMax : (Ideal.span {p}).IsMaximal :=
    ((Ideal.span_singleton_prime hp.ne_zero).mpr hp).isMaximal (by simpa using hp.ne_zero)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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})
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) 0) : ℤ)
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ 0
have h₁ : ∀ (Q : Ideal S) (hQ : Q.IsMaximal) (e : Eq (α := Ideal ℤ) (comap (F := ℤ →+* S) (algebraMap ℤ S) Q) (span {p})),
  ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ 0
Tactic: obtain ⟨Q, hQ, e⟩ := Ideal.exists_ideal_over_maximal_of_isIntegral (S := S) (Ideal.span {p})
      (fun x ↦ by simp +contextual)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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 : 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
have h₂ : ∀ (hI' : IsUnit.{u_1} (M := Ideal S) ⊤) (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) ⊤) : ℤ)),
  ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ ⊤
Tactic: obtain rfl : I = ⊤ := by simpa using hI'
Cleared hypotheses: I, hI', hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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 * I)) : ℤ)
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
have hI₁ : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) P) : ℤ) ∨ p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
Tactic: simp only [_root_.map_mul, Nat.cast_mul, hp.dvd_mul] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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) : ℤ)
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
have 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
Tactic: obtain ⟨Q, h₁, h₂, h₃⟩ := IH h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
have this₁ : P.IsMaximal
Tactic: have := (Ideal.isPrime_of_prime hP).isMaximal hP.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
have h₃ : LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
Tactic: refine ⟨P, this, (hpMax.eq_of_le (by simpa using this.ne_top) ?_).symm, dvd_mul_right _ _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
have 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)
Tactic: obtain ⟨q, n, hn, hqP, hq, H⟩ := Ideal.exists_prime_and_absNorm_eq_pow P
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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
⊢ LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
have hI₁ : ∃ 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
Cleared hypotheses: hI, hn, hqP, hq, H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
have h₃ : ∀ (m : ℕ) (hmn : m ≤ n) (hp : Associated p (HPow.hPow (α := ℤ) (↑q : ℤ) m)), LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
Tactic: obtain ⟨m, hmn, hp⟩ := hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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)
⊢ LE.le (α := Ideal ℤ) (span {p}) (under ℤ P)
have h₃ : Membership.mem (γ := Ideal ℤ) (under ℤ P) p
Tactic: rw [Ideal.span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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)
⊢ Membership.mem (γ := Ideal ℤ) (under ℤ P) p
have this₁ : m ≠ 0
Tactic: have : m ≠ 0 := fun h ↦ hpMax.ne_top (Ideal.span_singleton_eq_top.mpr (by simpa [h] using hp))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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) : ℤ)
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
have 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
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)
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ ∃ (P_1 : Ideal S), P_1.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P_1) (span {p}) ∧ P_1 ∣ P * I
have 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
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)
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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})
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
have h₁ : ∀ (hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) 0) : ℤ)),
  ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ 0
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)
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
have 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
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)
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I
have 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
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)
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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 : ℕ
⊢ Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}
have inl : ∀ (hn : n = 0), 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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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}
⊢ Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}
have inr : ∀ (hn : n > 0), 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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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}
have inr : (f '' {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}).Finite
Tactic: refine Set.Finite.of_finite_image (f := f) ?_ ?_