awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (_ : Ne.{u_1 + 1} (α := Ideal R) ⊤ ⊤), height.{u_1} (R := R) ⊤)
    (⨆ (_ : IsMaximal.{u_1} (α := R) ⊥), height.{u_1} (R := R) ⊥)

Tactic:
grind [iSup_le_iff, Ideal.IsPrime.ne_top]

Premises used: iSup_le_iff, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ ∃ (i' : Ideal R),
    LE.le (α := ℕ∞) (⨆ (_ : Ne.{u_1 + 1} (α := Ideal R) ⊤ ⊤), height.{u_1} (R := R) ⊤) (⨆ (_ : i'.IsMaximal), i'.height)

Tactic:
exact ⟨⊥, by grind [iSup_le_iff, Ideal.IsPrime.ne_top]⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : I ≠ ⊤
a :
  ∀ (M : Ideal R) (hM : M.IsMaximal) (hIM : I ≤ M),
    ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)

Tactic:
obtain ⟨M, hM, hIM⟩ := exists_le_maximal I I_top

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hIM : I ≤ M
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)

Tactic:
⟨M, iSup_mono' (fun hI ↦ ⟨hM, height_mono hIM⟩)⟩

Premises used: iSup_mono', Ideal.height_mono, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hIM : I ≤ M
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)

Tactic:
exact ⟨M, iSup_mono' (fun hI ↦ ⟨hM, height_mono hIM⟩)⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
simp_rw : (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) : WithBot ℕ∞) = ringKrullDim R
⊢ (↑(⨆ (I : Ideal R), ⨆ (x : I.IsMaximal), I.primeHeight) : WithBot ℕ∞) = ringKrullDim R

Tactic:
simp_rw [← Ideal.height_eq_primeHeight, Ideal.sup_isMaximal_height_eq_ringKrullDim]

Premises used: Ideal.sup_isMaximal_height_eq_ringKrullDim, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], KrullDimLE.{u_2} n (Rₚ P)
simp_rw :
  ∀ (h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)),
    ringKrullDim R ≤ (↑n : WithBot ℕ∞)
⊢ KrullDimLE n R

Tactic:
simp_rw [Ring.krullDimLE_iff] at h ⊢

Premises used: Ring.krullDimLE_iff
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)
h_1 : Nontrivial R
rw : LE.le (α := WithBot ℕ∞) (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) : WithBot ℕ∞) (↑n : WithBot ℕ∞)
⊢ ringKrullDim R ≤ (↑n : WithBot ℕ∞)

Tactic:
rw [← Ideal.sup_isMaximal_height_eq_ringKrullDim]

Premises used: Ideal.sup_isMaximal_height_eq_ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)
h_1 : Nontrivial R
⊢ LE.le (α := WithBot ℕ∞) (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) : WithBot ℕ∞) (↑n : WithBot ℕ∞)

Tactic:
(WithBot.coe_le_coe).mpr (iSup₂_le_iff.mpr fun P hP ↦ ?_)

Premises used: Iff.mpr, WithBot.coe_le_coe, iSup₂_le_iff
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)
h_1 : Nontrivial R
refine : ∀ (P : Ideal R) (hP : P.IsMaximal), P.height ≤ (↑n : ℕ∞)
⊢ LE.le (α := WithBot ℕ∞) (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) : WithBot ℕ∞) (↑n : WithBot ℕ∞)

Tactic:
refine (WithBot.coe_le_coe).mpr (iSup₂_le_iff.mpr fun P hP ↦ ?_)

Premises used: Iff.mpr, WithBot.coe_le_coe, iSup₂_le_iff
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)
h_1 : Nontrivial R
P : Ideal R
hP : P.IsMaximal
rw : ringKrullDim.{u_2} (Rₚ P) ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)
⊢ P.height ≤ (↑n : ℕ∞)

Tactic:
rw [← WithBot.coe_le_coe, ← IsLocalization.AtPrime.ringKrullDim_eq_height P (Rₚ P)]

Premises used: WithBot.coe_le_coe, IsLocalization.AtPrime.ringKrullDim_eq_height
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)
h_1 : Nontrivial R
P : Ideal R
hP : P.IsMaximal
⊢ ringKrullDim.{u_2} (Rₚ P) ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)

Tactic:
h P
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)
h_1 : Nontrivial R
P : Ideal R
hP : P.IsMaximal
⊢ ringKrullDim.{u_2} (Rₚ P) ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)

Tactic:
exact h P
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
n : ℕ
⊢ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)})) = n

Tactic:
simp [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply]

Premises used: Ideal.absNorm_apply, Submodule.cardQuot_apply
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Ideal.IsMaximal (α := ℤ) (Ideal.span {(↑p : ℤ)})

Tactic:
Ideal.Quotient.maximal_of_isField _ <|
    (Int.quotientSpanNatEquivZMod p).toMulEquiv.isField (Field.toIsField _)

Premises used: RingEquiv.toMulEquiv, Field.toIsField, Int.quotientSpanNatEquivZMod, MulEquiv.isField, Ideal.Quotient.maximal_of_isField
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
n : ℕ
⊢ ringChar (HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)})) = n

Tactic:
ringChar.eq_iff.mpr <| (charP_iff _ _).mpr fun x ↦ ?_

Premises used: Iff.mpr, charP_iff, ringChar.eq_iff
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
n : ℕ
refine :
  ∀ (x : ℕ),
    Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)})) (↑x : ℤ ⧸ Ideal.span {(↑n : ℤ)}) 0 ↔ n ∣ x
⊢ ringChar (HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)})) = n

Tactic:
refine ringChar.eq_iff.mpr <| (charP_iff _ _).mpr fun x ↦ ?_

Premises used: Iff.mpr, charP_iff, ringChar.eq_iff
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
n x : ℕ
rw : Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) (↑x : ℤ) ↔ n ∣ x
rw₁ : Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(↑n : ℤ) : ℤ)}) (↑x : ℤ) ↔ n ∣ x
rw₂ : Dvd.dvd (α := ℤ) (↑(↑n : ℤ) : ℤ) (↑x : ℤ) ↔ n ∣ x
rw₃ : Dvd.dvd (α := ℤ) (↑n : ℤ) (↑x : ℤ) ↔ n ∣ x
rw₄ rw₅ : n ∣ x ↔ n ∣ x
⊢ Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}) : (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)}) (↑x : ℤ)) 0 ↔
    n ∣ x

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem, ← Int.cast_natCast, Ideal.mem_span_singleton,
    Int.cast_natCast, Int.natCast_dvd_natCast]

Premises used: Int.cast_natCast, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : Ring R
I_1 I : Ideal R
rw : Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)}) (under ℤ I)
rw₁ :
  Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (comap (F := ℤ →+* R) (algebraMap ℤ R) I)) : ℤ)})
    (comap (F := ℤ →+* R) (algebraMap ℤ R) I)
rw₂ rw₃ : Eq (α := Ideal ℤ) (comap (F := ℤ →+* R) (algebraMap ℤ R) I) (comap (F := ℤ →+* R) (algebraMap ℤ R) I)
⊢ I.LiesOver (A := ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)})

Tactic:
rw [liesOver_iff, under_def, Int.ideal_span_absNorm_eq_self]

Premises used: Ideal.liesOver_iff, Ideal.under_def, Int.ideal_span_absNorm_eq_self
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
d : ℤ
rw : (↑d : R) ∈ I ↔ Membership.mem (γ := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)}) d
rw₁ : (↑d : R) ∈ I ↔ Membership.mem (γ := Ideal ℤ) (under ℤ I) d
rw₂ : (↑d : R) ∈ I ↔ Membership.mem (γ := Ideal ℤ) (comap (F := ℤ →+* R) (algebraMap ℤ R) I) d
rw₃ : (↑d : R) ∈ I ↔ Membership.mem (α := R) I ((algebraMap ℤ R : (a : ℤ) → R) d : R)
rw₄ rw₅ : (↑d : R) ∈ I ↔ (↑d : R) ∈ I
⊢ (↑d : R) ∈ I ↔ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) ∣ d

Tactic:
rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]

Premises used: eq_intCast, Ideal.under_def, Int.ideal_span_absNorm_eq_self, Ideal.mem_span_singleton, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
rw : (↑(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) : R) ∈ I
rw₁ rw₂ :
  Dvd.dvd (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)
⊢ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : R) ∈ I

Tactic:
rw [← cast_natCast, cast_mem_ideal_iff]

Premises used: Int.cast_natCast, Int.cast_mem_ideal_iff
-- Module: Mathlib.RingTheory.Ideal.Int
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} : ℕ)
neg :
  ∀ (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} : ℕ)

Tactic:
by_cases h : absNorm (under ℤ I) = 0

Premises used: Ideal.absNorm, Int, DFunLike.coe, Ideal.under
-- Module: Mathlib.RingTheory.Ideal.Int
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} ∅

Tactic:
Set.eq_empty_of_forall_notMem ?_

Premises used: Set.eq_empty_of_forall_notMem
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
refine : ∀ (x : ℕ), x ∉ {d : ℕ | 0 < d ∧ (↑d : R) ∈ I}
⊢ Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} ∅

Tactic:
refine Set.eq_empty_of_forall_notMem ?_

Premises used: Set.eq_empty_of_forall_notMem
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
x : ℕ
this : ∀ (hx₁ : 0 < x) (hx₂ : (↑x : R) ∈ I), False
⊢ x ∉ {d : ℕ | 0 < d ∧ (↑d : R) ∈ I}

Tactic:
⟨hx₁, hx₂⟩
-- Module: Mathlib.RingTheory.Ideal.Int
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
⊢ x = 0

Tactic:
rw [← cast_natCast, cast_mem_ideal_iff, h, natCast_dvd_natCast, Nat.zero_dvd] at hx₂

Premises used: Int.cast_natCast, Nat.zero_dvd, Int.cast_mem_ideal_iff, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Ideal.Int
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
⊢ x ≠ 0

Tactic:
rw [Nat.pos_iff_ne_zero] at hx₁

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Int
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
hx₃ : x ≠ 0
⊢ x = 0

Tactic:
rw [Nat.pos_iff_ne_zero] at hx₁

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
x : ℕ
hx₁ : x ≠ 0
hx₂ : x = 0
⊢ False

Tactic:
hx₁ hx₂
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
x : ℕ
hx₁ : x ≠ 0
hx₂ : x = 0
⊢ False

Tactic:
exact hx₁ hx₂
-- Module: Mathlib.RingTheory.Ideal.Int
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} ∅

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₂
-- Module: Mathlib.RingTheory.Ideal.Int
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 ∅)
pos₂ pos₃ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)

Tactic:
rw [h, this, Nat.sInf_empty]

Premises used: Nat.sInf_empty
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
h : ¬Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
⊢ 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⟩
-- Module: Mathlib.RingTheory.Ideal.Int
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} : ℕ)

Tactic:
le_antisymm ?_ (Nat.sInf_le h₁)

Premises used: le_antisymm, Nat.sInf_le
-- Module: Mathlib.RingTheory.Ideal.Int
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) : ℕ)
neg : LE.le (α := ℕ) ((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} : ℕ)

Tactic:
refine le_antisymm ?_ (Nat.sInf_le h₁)

Premises used: le_antisymm, Nat.sInf_le
-- Module: Mathlib.RingTheory.Ideal.Int
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) : ℕ)
neg :
  ∀ (h₀ : LT.lt (α := ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ)),
    False
⊢ LE.le (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)

Tactic:
by_contra! h₀
-- Module: Mathlib.RingTheory.Ideal.Int
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) : ℕ)
⊢ (↑(sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I}) : R) ∈ I

Tactic:
have h₂ := (Nat.sInf_mem (Set.nonempty_of_mem h₁)).2
-- Module: Mathlib.RingTheory.Ideal.Int
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
⊢ 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₂

Premises used: Int.cast_natCast, Int.cast_mem_ideal_iff, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Ideal.Int
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₂ : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
⊢ False

Tactic:
lt_iff_not_ge.mp h₀ <| Nat.le_of_dvd (Nat.sInf_mem (Set.nonempty_of_mem h₁)).1 h₂

Premises used: lt_iff_not_ge, Nat.sInf_mem, And.left, Iff.mp, Set.nonempty_of_mem, Nat.le_of_dvd
-- Module: Mathlib.RingTheory.Ideal.Int
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₂ : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
⊢ False

Tactic:
exact lt_iff_not_ge.mp h₀ <| Nat.le_of_dvd (Nat.sInf_mem (Set.nonempty_of_mem h₁)).1 h₂

Premises used: lt_iff_not_ge, Nat.sInf_mem, And.left, Iff.mp, Set.nonempty_of_mem, Nat.le_of_dvd
-- Module: Mathlib.RingTheory.Ideal.Int
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 : ℕ)
inr :
  Infinite.{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 : ℕ)

Tactic:
cases finite_or_infinite (S ⧸ I)

Premises used: finite_or_infinite, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Ideal.Int
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)
inl :
  ∀ (this : Fintype (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 : ℕ)

Tactic:
have : Fintype (S ⧸ I) := Fintype.ofFinite (S ⧸ I)
-- Module: Mathlib.RingTheory.Ideal.Int
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 : ℕ
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
⊢ (↑d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0

Tactic:
simp_rw [nsmul_eq_mul, ← map_natCast (Ideal.Quotient.mk I), ← Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.mk, Ideal.Quotient.eq_zero_iff_mem, map_natCast, nsmul_eq_mul
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h_1 : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
d : ℕ
h : 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 [h]
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h_1 : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
d : ℕ
h : ∀ (x : S ⧸ I), (Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑d : S) * x = 0
⊢ Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑d : S)) 0

Tactic:
simpa using h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Int
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 : ℕ
⊢ 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:
exact ⟨fun h _ ↦ by simp [h], fun h ↦ by simpa using h 1⟩
-- Module: Mathlib.RingTheory.Ideal.Int
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

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⟩
-- Module: Mathlib.RingTheory.Ideal.Int
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
inl : (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ Fintype.card.{u_2} (S ⧸ I)
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)

Tactic:
rw [Ideal.absNorm_apply I, Submodule.cardQuot_apply, Nat.card_eq_fintype_card]

Premises used: Ideal.absNorm_apply, Nat.card_eq_fintype_card, Submodule.cardQuot_apply