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
n : ℕ
⊢ (absNorm : (a : Ideal S) → ℕ) (span {(↑n : S)}) = n ^ finrank ℤ S

Tactic:
simp [absNorm_span_singleton, Algebra.norm_natCast]

Premises used: Algebra.norm_natCast, Ideal.absNorm_span_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
I : Ideal S
x : S
h : x ∈ I
rw : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {x}) : ℕ)
⊢ Dvd.dvd (α := ℤ) ((↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ) : ℤ) ((Algebra.norm ℤ : (a : S) → ℤ) x : ℤ)

Tactic:
rw [← Int.dvd_natAbs, ← absNorm_span_singleton x, Int.natCast_dvd_natCast]

Premises used: Int.dvd_natAbs, Ideal.absNorm_span_singleton, Int.natCast_dvd_natCast
-- 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
I : Ideal S
x : S
h : x ∈ I
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {x}) : ℕ)

Tactic:
absNorm_dvd_absNorm_of_le ((span_singleton_le_iff_mem _).mpr h)

Premises used: Iff.mpr, Ideal.absNorm_dvd_absNorm_of_le, 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
I : Ideal S
x : S
h : x ∈ I
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {x}) : ℕ)

Tactic:
exact absNorm_dvd_absNorm_of_le ((span_singleton_le_iff_mem _).mpr h)

Premises used: Iff.mpr, Ideal.absNorm_dvd_absNorm_of_le, 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
r : S
s : Set S
rw rw₁ : Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) r) ∣ Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) r)
⊢ (absNorm : (a : Ideal S) → ℕ) (span {r}) ∣ Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) r)

Tactic:
rw [absNorm_span_singleton]

Premises used: Ideal.absNorm_span_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
I : Ideal S
mp : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) → I = ⊥
mpr : I = ⊥ → Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ I = ⊥

Tactic:
constructor
-- 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
I : Ideal S
hI : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
mp : I ≤ ⊥
⊢ I = ⊥

Tactic:
rw [← le_bot_iff]

Premises used: le_bot_iff
-- 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
I : Ideal S
hI : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
x : S
hx : x ∈ I
mp : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {x}) : ℕ)
⊢ Membership.mem (γ := Submodule S S) ⊥ x

Tactic:
rw [mem_bot, ← Algebra.norm_eq_zero_iff (R := ℤ), ← Int.natAbs_eq_zero,
      ← Ideal.absNorm_span_singleton, ← zero_dvd_iff, ← hI]

Premises used: Ideal.mem_bot, zero_dvd_iff, Int.natAbs_eq_zero, Algebra.norm_eq_zero_iff, Ideal.absNorm_span_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
I : Ideal S
hI : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
x : S
hx : x ∈ I
mp : span {x} ≤ I
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {x}) : ℕ)

Tactic:
apply Ideal.absNorm_dvd_absNorm_of_le

Premises used: Ideal.absNorm_dvd_absNorm_of_le
-- 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
I : Ideal S
hI : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
x : S
hx : x ∈ I
mp mp₁ mp₂ mp₃ : x ∈ I
⊢ span {x} ≤ I

Tactic:
rwa [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
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) ⊥ : ℕ) (0 : ℕ)

Tactic:
absNorm_bot

Premises used: Ideal.absNorm_bot
-- 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
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) ⊥ : ℕ) (0 : ℕ)

Tactic:
exact absNorm_bot

Premises used: Ideal.absNorm_bot
-- 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
I : Ideal S
simp_rw :
  ¬Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
simp_rw₁ : ¬I = ⊥ ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
simp_rw₂ : ¬I = ⊥ ↔ I ≠ 0
⊢ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I

Tactic:
simp_rw [ne_eq, Ideal.absNorm_eq_zero_iff, mem_nonZeroDivisors_iff_ne_zero, Submodule.zero_eq_bot]

Premises used: ne_eq, Submodule.zero_eq_bot, mem_nonZeroDivisors_iff_ne_zero, Ideal.absNorm_eq_zero_iff
-- 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
I : Ideal S
rw :
  LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ↔
    Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
rw₁ rw₂ :
  Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
⊢ LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I

Tactic:
rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors
-- 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
I : ↥(Ideal S)⁰
⊢ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) : ℕ) (0 : ℕ)

Tactic:
absNorm_ne_zero_iff_mem_nonZeroDivisors.mpr (SetLike.coe_mem I)

Premises used: Iff.mpr, SetLike.coe_mem, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors
-- 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
I : ↥(Ideal S)⁰
⊢ LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) : ℕ)

Tactic:
absNorm_pos_iff_mem_nonZeroDivisors.mpr (SetLike.coe_mem I)

Premises used: Iff.mpr, Ideal.absNorm_pos_iff_mem_nonZeroDivisors, SetLike.coe_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
I : Ideal S
hI : I ≠ ⊥
rwa : AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I) ≠ 0
rwa₁ : Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
rwa₂ : ¬Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
rwa₃ rwa₄ rwa₅ rwa₆ : ¬I = ⊥
⊢ AddSubgroup.FiniteIndex.{u_1} (G := S) (toAddSubgroup I)

Tactic:
rwa [AddSubgroup.finiteIndex_iff, ← absNorm_eq_index, Ne, absNorm_eq_zero_iff]

Premises used: Ne, Ideal.absNorm_eq_index, Ideal.absNorm_eq_zero_iff, AddSubgroup.finiteIndex_iff
-- 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
I : Ideal S
hI : I ≠ ⊥
J : Ideal S
⊢ FiniteIndex.{u_1} (G := S) (toAddSubgroup I)

Tactic:
have := finiteIndex 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
I : Ideal S
hI : I ≠ ⊥
J : Ideal S
this : FiniteIndex.{u_1} (G := S) (toAddSubgroup I)
⊢ IsFiniteRelIndex.{u_1} (G := S) (toAddSubgroup I) (toAddSubgroup J)

Tactic:
isFiniteRelIndex_of_finiteIndex

Premises used: AddSubgroup.isFiniteRelIndex_of_finiteIndex
-- 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
I : Ideal S
hI : I ≠ ⊥
J : Ideal S
this : FiniteIndex.{u_1} (G := S) (toAddSubgroup I)
⊢ IsFiniteRelIndex.{u_1} (G := S) (toAddSubgroup I) (toAddSubgroup J)

Tactic:
exact isFiniteRelIndex_of_finiteIndex

Premises used: AddSubgroup.isFiniteRelIndex_of_finiteIndex
-- 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 : Ideal S
inst_5 : P.IsMaximal
⊢ IsAddTorsionFree S

Tactic:
have : IsAddTorsionFree S := .of_isTorsionFree ℤ _
-- 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 : Ideal S
inst_5 : P.IsMaximal
this : IsAddTorsionFree S
⊢ CharZero S

Tactic:
have := CharZero.of_isAddTorsionFree S S
-- 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 : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this : CharZero S
⊢ Finite.{u_1 + 1} (S ⧸ P)

Tactic:
have : Finite (S ⧸ P) := Submodule.finiteQuotientOfFreeOfRankEq (P.restrictScalars ℤ)
    (Ideal.finrank_eq_finrank (Module.Free.chooseBasis _ _) _
      (Ideal.IsMaximal.ne_bot_of_isIntegral_int P))
-- 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 : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this_2 : CharZero S
this : Finite.{u_1 + 1} (S ⧸ P)
intro :
  ∀ (val : Fintype (S ⧸ P)),
    ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n

Tactic:
cases nonempty_fintype (S ⧸ P)

Premises used: HasQuotient.Quotient, nonempty_fintype
-- 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 : 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
intro :
  ∀ (p : ℕ) (hpR : CharP.{u_1} (S ⧸ P) p),
    ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n

Tactic:
obtain ⟨p, hpR⟩ := CharP.exists (S ⧸ P)

Premises used: CharP.exists, HasQuotient.Quotient
-- 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 : 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
intro :
  ∀ (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
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n

Tactic:
obtain ⟨n, hp, e⟩ := FiniteField.card (S ⧸ P) p

Premises used: HasQuotient.Quotient, FiniteField.card
-- 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 : 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 : ℕ)
⊢ (absNorm : (a : Ideal S) → ℕ) P = p ^ (↑n : ℕ)

Tactic:
have hP : P.absNorm = p ^ (n : ℕ) := (Nat.card_eq_fintype_card.trans e:)
-- 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 : 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

Tactic:
⟨p, n, n.2, ?_, hp, hP⟩

Premises used: PNat.val, And.intro, Exists.intro, Subtype.property
-- 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 : 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 : ℕ)
intro : (↑p : S) ∈ P
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n

Tactic:
refine ⟨p, n, n.2, ?_, hp, 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 : 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 : ℕ)
intro : (↑((absNorm : (a : Ideal S) → ℕ) P) : S) ∈ P
⊢ (↑p : S) ∈ P

Tactic:
rw [← Ideal.IsPrime.pow_mem_iff_mem (I := P) inferInstance _ n.pos, ← Nat.cast_pow, ← hP]

Premises used: Ideal.IsPrime.pow_mem_iff_mem, inferInstance, PNat.pos, 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 : 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 : ℕ)
⊢ (↑((absNorm : (a : Ideal S) → ℕ) P) : S) ∈ P

Tactic:
P.absNorm_mem

Premises used: Set.Mem, Ideal.absNorm_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 : 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 : ℕ)
⊢ (↑((absNorm : (a : Ideal S) → ℕ) P) : S) ∈ P

Tactic:
exact P.absNorm_mem

Premises used: Ideal.absNorm_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 : Prime p
I : Ideal S
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
⊢ IsAddTorsionFree S

Tactic:
have : IsAddTorsionFree S := .of_isTorsionFree ℤ _
-- 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 : IsAddTorsionFree S
⊢ CharZero S

Tactic:
have := CharZero.of_isAddTorsionFree S S
-- 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
⊢ Ne (α := Ideal ℤ) (span {p}) ⊥

Tactic:
simpa using hp.ne_zero

Premises used: Prime.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
I : Ideal S
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
this_1 : IsAddTorsionFree S
this : CharZero S
⊢ 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)
-- 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})
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) 0) : ℤ)
x : ℤ
⊢ Membership.mem (γ := Submodule ℤ ℤ) (RingHom.ker (F := ℤ →+* S) (algebraMap ℤ S)) x →
    Membership.mem (γ := Submodule ℤ ℤ) (span {p}) x

Tactic:
simp +contextual
-- 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})
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) 0) : ℤ)
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
⊢ ∃ (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)

Premises used: Ideal.exists_ideal_over_maximal_of_isIntegral, Ideal.span, Singleton.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
p : ℤ
hp : Prime p
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) 0) : ℤ)
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:
⟨Q, hQ, e, dvd_zero _⟩

Premises used: dvd_zero, 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})
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) 0) : ℤ)
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:
exact ⟨Q, hQ, e, dvd_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 : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
I : Ideal S
hI' : IsUnit I
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
⊢ I = ⊤

Tactic:
simpa using 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 : 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) : ℤ)
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 ∣ ⊤
⊢ ∃ (P : Ideal S), P.IsMaximal ∧ Eq (α := Ideal ℤ) (under ℤ P) (span {p}) ∧ P ∣ I

Tactic:
obtain rfl : I = ⊤ := by simpa using hI'

Premises used: 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 : Prime p
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
hI' : IsUnit.{u_1} (M := Ideal S) ⊤
hI : p ∣ (↑((absNorm : (a : Ideal S) → ℕ) ⊤) : ℤ)
⊢ p ∣ 1

Tactic:
simpa using 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 : Prime p
this_1 : IsAddTorsionFree S
this : CharZero S
hpMax : IsMaximal (α := ℤ) (span {p})
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:
cases hp.not_dvd_one (by simpa using hI)

Premises used: Prime.not_dvd_one
-- 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 * I)) : ℤ)
⊢ 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

Premises used: Prime.dvd_mul, map_mul, Nat.cast_mul