awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
a :
  LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (_ :
      RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p ≤
        RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p),
      (↑(p.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
⊢ (↑(p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.primeHeight
have a₁ : ⨆ (_ :
    RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p ≤
      RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p),
    (↑(p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
  (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p).asIdeal.primeHeight
Tactic: apply le_trans (b := ⨆ (_ : p.last ≤ p.last), ↑p.length)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height ≤
    ⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height
have a : (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p).asIdeal.height ≤
  ⨆ (_ :
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal ≠
      ⊤),
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height
Tactic: apply le_trans (b := ⨆ (_ : (p.last).asIdeal ≠ ⊤), p.last.asIdeal.height)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
a :
  (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height ≤
    ⨆ (_ :
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal ≠
        ⊤),
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal.height
⊢ (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height ≤
    ⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height
have a₁ : LE.le (α := ℕ∞)
  (⨆ (_ :
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal ≠
      ⊤),
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height)
  (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
Tactic: apply le_trans (b := ⨆ (_ : (p.last).asIdeal ≠ ⊤), p.last.asIdeal.height)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) : WithBot ℕ∞) = ringKrullDim R
have rw : Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
Tactic: rw [← sup_height_eq_ringKrullDim, WithBot.coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
have a : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
a : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
⊢ Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
have a₁ : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height)
have a : ∀ (I : Ideal R), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
Tactic: refine iSup_mono' fun I => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
have pos : ∀ (I_top : I = ⊤), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
Tactic: by_cases I_top : I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
pos : ∀ (I_top : I = ⊤), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
have neg : ∀ (I_top : ¬I = ⊤), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
Tactic: by_cases I_top : I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
have neg : ∀ (P : Ideal R) (hP : P ∈ I.minimalPrimes),
  ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
Tactic: obtain ⟨P, hP⟩ := Set.nonempty_coe_sort.mp (nonempty_minimalPrimes I_top)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
have neg : I.height ≤ P.height
Tactic: refine ⟨P, iSup_pos (α := ℕ∞) I_top ▸ le_iSup_of_le (hP.left.left) ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ I.height ≤ P.height
have this : P.IsPrime
Tactic: have := hP.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) : WithBot ℕ∞) = ringKrullDim R
have rw : Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
Tactic: rw [← Ideal.sup_height_eq_ringKrullDim, WithBot.coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
have a : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
a : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
⊢ Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
have a₁ : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height)
have a : ∀ (I : Ideal R), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
Tactic: refine iSup_mono' fun I => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
have a : ∃ (i' : Ideal R),
  LE.le (α := ℕ∞) (⨆ (_ : Ne.{u_1 + 1} (α := Ideal R) ⊤ ⊤), height.{u_1} (R := R) ⊤) (⨆ (_ : i'.IsMaximal), i'.height)
Tactic: obtain rfl | I_top := eq_or_ne I ⊤
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
a :
  ∃ (i' : Ideal R),
    LE.le (α := ℕ∞) (⨆ (_ : Ne.{u_1 + 1} (α := Ideal R) ⊤ ⊤), height.{u_1} (R := R) ⊤) (⨆ (_ : i'.IsMaximal), i'.height)
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
have a₁ : ∀ (I_top : I ≠ ⊤), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
Tactic: obtain rfl | I_top := eq_or_ne I ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : I ≠ ⊤
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
have a : ∀ (M : Ideal R) (hM : M.IsMaximal) (hIM : I ≤ M),
  ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
Tactic: obtain ⟨M, hM, hIM⟩ := exists_le_maximal I I_top
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ (↑(⨆ (I : Ideal R), ⨆ (x : I.IsMaximal), I.primeHeight) : WithBot ℕ∞) = ringKrullDim R
have simp_rw : (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) : WithBot ℕ∞) = ringKrullDim R
Tactic: simp_rw [← Ideal.height_eq_primeHeight, Ideal.sup_isMaximal_height_eq_ringKrullDim]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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)
⊢ KrullDimLE n R
have simp_rw : ∀ (h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim.{u_2} (Rₚ P) ≤ (↑n : WithBot ℕ∞)),
  ringKrullDim R ≤ (↑n : WithBot ℕ∞)
Tactic: simp_rw [Ring.krullDimLE_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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 ℕ∞)
⊢ ringKrullDim R ≤ (↑n : WithBot ℕ∞)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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
⊢ ringKrullDim R ≤ (↑n : WithBot ℕ∞)
have rw : LE.le (α := WithBot ℕ∞) (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) : WithBot ℕ∞) (↑n : WithBot ℕ∞)
Tactic: rw [← Ideal.sup_isMaximal_height_eq_ringKrullDim]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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 ℕ∞)
have refine : ∀ (P : Ideal R) (hP : P.IsMaximal), P.height ≤ (↑n : ℕ∞)
Tactic: refine (WithBot.coe_le_coe).mpr (iSup₂_le_iff.mpr fun P hP ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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
⊢ P.height ≤ (↑n : ℕ∞)
have rw : ringKrullDim.{u_2} (Rₚ P) ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)
Tactic: rw [← WithBot.coe_le_coe, ← IsLocalization.AtPrime.ringKrullDim_eq_height P (Rₚ P)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
n : ℕ
⊢ ringChar (HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)})) = n
have refine : ∀ (x : ℕ),
  Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)})) (↑x : ℤ ⧸ Ideal.span {(↑n : ℤ)}) 0 ↔ n ∣ x
Tactic: refine ringChar.eq_iff.mpr <| (charP_iff _ _).mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
n x : ℕ
⊢ Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}) : (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)}) (↑x : ℤ)) 0 ↔
    n ∣ x
have rw : Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) (↑x : ℤ) ↔ n ∣ x
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem, ← Int.cast_natCast, Ideal.mem_span_singleton,
    Int.cast_natCast, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
n x : ℕ
rw : Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑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
have rw₁ : Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(↑n : ℤ) : ℤ)}) (↑x : ℤ) ↔ n ∣ x
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem, ← Int.cast_natCast, Ideal.mem_span_singleton,
    Int.cast_natCast, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
n x : ℕ
rw : Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) (↑x : ℤ) ↔ n ∣ x
rw₁ : Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(↑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
have rw₂ : Dvd.dvd (α := ℤ) (↑(↑n : ℤ) : ℤ) (↑x : ℤ) ↔ n ∣ x
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem, ← Int.cast_natCast, Ideal.mem_span_singleton,
    Int.cast_natCast, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
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
⊢ Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}) : (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)}) (↑x : ℤ)) 0 ↔
    n ∣ x
have rw₃ : Dvd.dvd (α := ℤ) (↑n : ℤ) (↑x : ℤ) ↔ n ∣ x
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem, ← Int.cast_natCast, Ideal.mem_span_singleton,
    Int.cast_natCast, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
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
⊢ Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}) : (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)}) (↑x : ℤ)) 0 ↔
    n ∣ x
have rw₄ : n ∣ x ↔ n ∣ x
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem, ← Int.cast_natCast, Ideal.mem_span_singleton,
    Int.cast_natCast, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I_1 I : Ideal R
⊢ I.LiesOver (A := ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)})
have rw : Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)}) (under ℤ I)
Tactic: rw [liesOver_iff, under_def, Int.ideal_span_absNorm_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I_1 I : Ideal R
rw : Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)}) (under ℤ I)
⊢ I.LiesOver (A := ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)})
have rw₁ : Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (comap (F := ℤ →+* R) (algebraMap ℤ R) I)) : ℤ)})
  (comap (F := ℤ →+* R) (algebraMap ℤ R) I)
Tactic: rw [liesOver_iff, under_def, Int.ideal_span_absNorm_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
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)
⊢ I.LiesOver (A := ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)})
have rw₂ : Eq (α := Ideal ℤ) (comap (F := ℤ →+* R) (algebraMap ℤ R) I) (comap (F := ℤ →+* R) (algebraMap ℤ R) I)
Tactic: rw [liesOver_iff, under_def, Int.ideal_span_absNorm_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
d : ℤ
⊢ (↑d : R) ∈ I ↔ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) ∣ d
have rw : (↑d : R) ∈ I ↔ Membership.mem (γ := Ideal ℤ) (span {(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)}) d
Tactic: rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
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
⊢ (↑d : R) ∈ I ↔ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) ∣ d
have rw₁ : (↑d : R) ∈ I ↔ Membership.mem (γ := Ideal ℤ) (under ℤ I) d
Tactic: rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
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
⊢ (↑d : R) ∈ I ↔ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) ∣ d
have rw₂ : (↑d : R) ∈ I ↔ Membership.mem (γ := Ideal ℤ) (comap (F := ℤ →+* R) (algebraMap ℤ R) I) d
Tactic: rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
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
⊢ (↑d : R) ∈ I ↔ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) ∣ d
have rw₃ : (↑d : R) ∈ I ↔ Membership.mem (α := R) I ((algebraMap ℤ R : (a : ℤ) → R) d : R)
Tactic: rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
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)
⊢ (↑d : R) ∈ I ↔ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) ∣ d
have rw₄ : (↑d : R) ∈ I ↔ (↑d : R) ∈ I
Tactic: rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
⊢ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : R) ∈ I
have rw : (↑(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) : R) ∈ I
Tactic: rw [← cast_natCast, cast_mem_ideal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
rw : (↑(↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) : R) ∈ I
⊢ (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : R) ∈ I
have rw₁ : Dvd.dvd (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ)
Tactic: rw [← cast_natCast, cast_mem_ideal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Int (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (sInf {d : ℕ | 0 < d ∧ (↑d : R) ∈ I} : ℕ)
have pos : ∀ (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