awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
pos :
  ∀ (h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)),
    Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have neg : ∀ (h : ¬Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)),
  Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
Tactic: by_cases h : absNorm (under ℤ I) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
⊢ Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ∅
have refine : ∀ (x : ℕ), x ∉ {d : ℕ | 0 < d ∧ (↑d : R) ∈ I}
Tactic: refine Set.eq_empty_of_forall_notMem ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
x : ℕ
⊢ x ∉ {d : ℕ | 0 < d ∧ (↑d : R) ∈ I}
have this : ∀ (hx₁ : 0 < x) (hx₂ : (↑x : R) ∈ I), False
Tactic: ⟨hx₁, hx₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
x : ℕ
hx₁ : 0 < x
hx₂ : (↑x : R) ∈ I
⊢ False
have hx₃ : x = 0
Tactic: rw [← cast_natCast, cast_mem_ideal_iff, h, natCast_dvd_natCast, Nat.zero_dvd] at hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
x : ℕ
hx₁ : 0 < x
hx₂ : x = 0
⊢ False
have hx₃ : x ≠ 0
Tactic: rw [Nat.pos_iff_ne_zero] at hx₁
Cleared hypotheses: hx₁, hx₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ∅
Tactic: have : {d : ℕ | 0 < d ∧ ↑d ∈ I} = ∅ := by
      refine Set.eq_empty_of_forall_notMem ?_
      intro x ⟨hx₁, hx₂⟩
      rw [← cast_natCast, cast_mem_ideal_iff, h, natCast_dvd_natCast, Nat.zero_dvd] at hx₂
      rw [Nat.pos_iff_ne_zero] at hx₁
      exact hx₁ hx₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ∅
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have pos : Eq (α := ℕ) 0 (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I})
Tactic: rw [h, this, Nat.sInf_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ∅
pos : Eq (α := ℕ) 0 (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I})
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have pos₁ : Eq (α := ℕ) 0 (sInf ∅)
Tactic: rw [h, this, Nat.sInf_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ∅
pos : Eq (α := ℕ) 0 (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I})
pos₁ : Eq (α := ℕ) 0 (sInf ∅)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have pos₂ : Eq (α := ℕ) 0 0
Tactic: rw [h, this, Nat.sInf_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : ¬Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have h₁ : Membership.mem (α := ℕ) (γ := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)
Tactic: have h₁ : absNorm (under ℤ I) ∈ {d : ℕ | 0 < d ∧ ↑d ∈ I} :=
      ⟨Nat.pos_of_ne_zero h, absNorm_under_mem I⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : ¬Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
h₁ : Membership.mem (α := ℕ) (γ := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have neg : LE.le (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
Tactic: refine le_antisymm ?_ (Nat.sInf_le h₁)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : ¬Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
h₁ : Membership.mem (α := ℕ) (γ := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)
⊢ LE.le (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have neg : ∀ (h₀ : LT.lt (α := ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)), False
Tactic: by_contra! h₀
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : ¬Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
h₁ : Membership.mem (α := ℕ) (γ := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)
h₀ : LT.lt (α := ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)
⊢ False
have h₂ : (↑(sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I}) : R) ∈ I
Tactic: have h₂ := (Nat.sInf_mem (Set.nonempty_of_mem h₁)).2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : ¬Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
h₁ : Membership.mem (α := ℕ) (γ := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)
h₀ : LT.lt (α := ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)
h₂ : (↑(sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I}) : R) ∈ I
⊢ False
have h₃ : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
Tactic: rw [← cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have inl : Finite.{u_2 + 1} (S ⧸ I) →
  Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
Tactic: cases finite_or_infinite (S ⧸ I)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
inl :
  Finite.{u_2 + 1} (S ⧸ I) →
    Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have inr : Infinite.{u_2 + 1} (S ⧸ I) →
  Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
Tactic: cases finite_or_infinite (S ⧸ I)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Finite.{u_2 + 1} (S ⧸ I)
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have inl : ∀ (this : Fintype (S ⧸ I)),
  Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
Tactic: have : Fintype (S ⧸ I) := Fintype.ofFinite (S ⧸ I)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
d : ℕ
⊢ (↑d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
have simp_rw : Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑d : S)) 0 ↔
  ∀ (x : S ⧸ I), (Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑d : S) * x = 0
Tactic: simp_rw [nsmul_eq_mul, ← map_natCast (Ideal.Quotient.mk I), ← Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (hypothesis)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have h_main : ∀ {d : ℕ}, (↑d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
Tactic: have h_main {d : ℕ} : (d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0 := by
      simp_rw [nsmul_eq_mul, ← map_natCast (Ideal.Quotient.mk I), ← Quotient.eq_zero_iff_mem]
      exact ⟨fun h _ ↦ by simp [h], fun h ↦ by simpa using h 1⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, (↑d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have inl : (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ Fintype.card.{u_2} (S ⧸ I)
Tactic: rw [Ideal.absNorm_apply I, Submodule.cardQuot_apply, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, (↑d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
⊢ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ Fintype.card.{u_2} (S ⧸ I)
have inl : AddMonoid.exponent.{u_2} (S ⧸ I) ∣ Fintype.card.{u_2} (S ⧸ I)
Tactic: simp_rw [absNorm_under_eq_sInf, h_main, ← AddMonoid.exponent_eq_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Infinite.{u_2 + 1} (S ⧸ I)
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
have inr : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
Tactic: rw [absNorm_apply I, Submodule.cardQuot_apply, Nat.card_eq_zero_of_infinite]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
⊢ ringChar.{u_2} (S ⧸ I) = (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)
have refine : ∀ (x : ℕ), Eq.{u_2 + 1} (α := S ⧸ I) (↑x : S ⧸ I) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
Tactic: refine ringChar.eq_iff.mpr <| (charP_iff _ _).mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
x : ℕ
⊢ Eq.{u_2 + 1} (α := S ⧸ I) (↑x : S ⧸ I) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
have change : Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑x : S)) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
Tactic: change Ideal.Quotient.mk I x = 0 ↔ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
x : ℕ
⊢ Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑x : S)) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
have rw : (↑x : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
Tactic: rw [Quotient.eq_zero_iff_mem, ← Int.cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
x : ℕ
rw : (↑x : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
⊢ Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑x : S)) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
have rw₁ : (↑(↑x : ℤ) : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
Tactic: rw [Quotient.eq_zero_iff_mem, ← Int.cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
x : ℕ
rw : (↑x : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
rw₁ : (↑(↑x : ℤ) : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
⊢ Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑x : S)) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
have rw₂ : Dvd.dvd (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) (↑x : ℤ) ↔
  (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
Tactic: rw [Quotient.eq_zero_iff_mem, ← Int.cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
x : ℕ
rw : (↑x : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
rw₁ : (↑(↑x : ℤ) : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
rw₂ :
  Dvd.dvd (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) (↑x : ℤ) ↔
    (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
⊢ Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑x : S)) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
have rw₃ : (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
Tactic: rw [Quotient.eq_zero_iff_mem, ← Int.cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
⊢ Prime ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P))
have rw : IsPrime (under ℤ P)
Tactic: rw [Nat.prime_iff_prime_int, ← span_singleton_prime, Int.ideal_span_absNorm_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
rw : IsPrime (under ℤ P)
⊢ Prime ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P))
have rw₁ : Ne (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)) : ℤ) 0
Tactic: rw [Nat.prime_iff_prime_int, ← span_singleton_prime, Int.ideal_span_absNorm_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
⊢ Ne (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)) : ℤ) 0
have refine : ¬Eq (α := Ideal ℤ) (under ℤ P) ⊥
Tactic: refine Int.natCast_ne_zero.mpr <| absNorm_eq_zero_iff.not.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
⊢ ¬Eq (α := Ideal ℤ) (under ℤ P) ⊥
have this : P ≠ ⊥
Tactic: have : P ≠ ⊥ := NeZero.ne _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
this : P ≠ ⊥
⊢ ¬Eq (α := Ideal ℤ) (under ℤ P) ⊥
have contrapose : ∀ (this : Eq (α := Ideal ℤ) (under ℤ P) ⊥), P = ⊥
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
have rw : (I ≠ ⊤ ∧ ∀ (b a : R), a • b ∈ I → b ∈ I ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R R) (a ^ n) ⊤ ≤ I) ↔
  I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Tactic: rw [IsPrimary, Submodule.IsPrimary, forall_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ I.IsPrimary
have rw : I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Tactic: rw [isPrimary_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
have left : I ≠ ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
left : I ≠ ⊤
⊢ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
have right : ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I.radical
have pos : ∀ (h : I + span {y} = ⊤), x ∈ I ∨ y ∈ I.radical
Tactic: by_cases h : I + span {y} = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
pos : ∀ (h : I + span {y} = ⊤), x ∈ I ∨ y ∈ I.radical
⊢ x ∈ I ∨ y ∈ I.radical
have neg : ∀ (h : ¬I + span {y} = ⊤), x ∈ I ∨ y ∈ I.radical
Tactic: by_cases h : I + span {y} = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical
have pos : span {x} * I ≤ I ∧ x * y ∈ I ∨ y ∈ I.radical
Tactic: rw [← span_singleton_le_iff_mem, ← mul_top (span {x}), ← h, mul_add,
        span_singleton_mul_span_singleton, add_le_iff, span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical
have neg : ∀ (m : Ideal R) (hm : m.IsMaximal) (hy : I + span {y} ≤ m), x ∈ I ∨ y ∈ I.radical
Tactic: obtain ⟨m, hm, hy⟩ := exists_le_maximal (I + span {y}) h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
m : Ideal R
hm : m.IsMaximal
hy : I + span {y} ≤ m
⊢ x ∈ I ∨ y ∈ I.radical
have hy₁ : I.radical ≤ m ∧ y ∈ m
Tactic: rw [add_le_iff, span_singleton_le_iff_mem, ← hm.isPrime.radical_le_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I.IsPrimary
φ : R →+* S
⊢ IsPrimary (Ideal.comap φ I)
have rw : ∀ (hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical) (φ : R →+* S),
  Ne (α := Ideal R) (Ideal.comap φ I) ⊤ ∧
    ∀ {x y : R},
      Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
        Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨ Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y
Tactic: rw [isPrimary_iff] at hI ⊢
Cleared hypotheses: hI, φ
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
⊢ Ne (α := Ideal R) (Ideal.comap φ I) ⊤ ∧
    ∀ {x y : R},
      Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
        Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨ Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y
have refine : ∀ (h : ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical) {x y : R},
  Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
    Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨ Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y
Tactic: refine hI.imp (comap_ne_top φ) fun h ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrimary (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
h : ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
⊢ ∀ {x y : R},
    Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
      Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨ Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y
have simp : ∀ {x y : R},
  HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) x : S) ((φ : (a : R) → S) y : S) ∈ I →
    Membership.mem (α := S) I ((φ : (a : R) → S) x : S) ∨ Membership.mem (α := S) I.radical ((φ : (a : R) → S) y : S)
Tactic: simp only [mem_comap, map_mul, ← comap_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipal (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
property : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (R ∙ x)
y : R
property_1 : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (R ∙ y)
⊢ (↑(Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) (R ∙ x) property *
          Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) (R ∙ y)
            property_1) :
      Ideal R) =
    R ∙ x * y
have simp_rw : HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) = R ∙ x * y
Tactic: simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipal (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
property : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (R ∙ x)
y : R
property_1 : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (R ∙ y)
simp_rw : HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) = R ∙ x * y
⊢ (↑(Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) (R ∙ x) property *
          Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) (R ∙ y)
            property_1) :
      Ideal R) =
    R ∙ x * y
have simp_rw₁ : HMul.hMul (α := Ideal R) (span {x}) (span {y}) = span {x * y}
Tactic: simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IsPrincipal (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x y : Associates R
⊢ (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) (x * y)) : Ideal R) =
    HMul.hMul (α := Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) x) : Ideal R)
      (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) y) : Ideal R)
have rw : (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
        (HMul.hMul (α := Associates R) (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))
          (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y)))) :
    Ideal R) =
  HMul.hMul (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) x))) :
      Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I })
          (Associates.mk (Quot.out (r := (⇑(Associated.setoid R) : R → R → Prop)) y))) :
      Ideal R)
Tactic: rw [← quot_out x, ← quot_out y]