awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hϖ : Irreducible ϖ
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x
have inr : ∀ (n : ℕ) (u : Rˣ) (hx : (↑u : R) * ϖ ^ n ≠ 0),
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n) : ℕ∞) (0 : ℕ∞) ↔
    IsUnit ((↑u : R) * ϖ ^ n)
Tactic: obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible hx hϖ
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ↔
    Associated x y
have mp : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) →
  Associated x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
mp :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) →
    Associated x y
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ↔
    Associated x y
have mpr : Associated x y →
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
⊢ Associated x y
have pos : ∀ (hx : x = 0), Associated x y
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
pos : ∀ (hx : x = 0), Associated x y
⊢ Associated x y
have neg : ∀ (hx : ¬x = 0), Associated x y
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : x = 0
⊢ Associated x y
have pos : ∀ (h : Eq (α := ℕ∞) (⊤ : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)) (hx : x = 0), Associated 0 y
Tactic: simp_all only [AddValuation.map_zero]
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h : Eq (α := ℕ∞) (⊤ : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : x = 0
⊢ Associated 0 y
have pos : Associated.{u_1} (M := R) 0 0
Tactic: rw [addVal_eq_top_iff.mp h.symm]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
⊢ Associated x y
have pos : ∀ (hy : y = 0), Associated x y
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
pos : ∀ (hy : y = 0), Associated x y
⊢ Associated x y
have neg : ∀ (hy : ¬y = 0), Associated x y
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : y = 0
⊢ Associated x y
have pos : ∀ (h : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)) (hx : ¬x = 0) (hy : y = 0), False
Tactic: simp_all only [AddValuation.map_zero, associated_zero_iff_eq_zero]
Cleared hypotheses: h, hx, hy
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : ¬y = 0
⊢ Associated x y
have neg : ∀ (ϖ : R) (hϖ : Irreducible ϖ), Associated x y
Tactic: obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
⊢ Associated x y
have neg : ∀ (m : ℕ) (α : Rˣ) (hx' : x = (↑α : R) * ϖ ^ m), Associated x y
Tactic: obtain ⟨m, α, hx'⟩ := eq_unit_mul_pow_irreducible hx hϖ
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
⊢ Associated x y
have neg : ∀ (n : ℕ) (β : Rˣ) (hy' : y = (↑β : R) * ϖ ^ n), Associated x y
Tactic: obtain ⟨n, β, hy'⟩ := eq_unit_mul_pow_irreducible hy hϖ
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
n : ℕ
β : Rˣ
hy' : y = (↑β : R) * ϖ ^ n
⊢ Associated x y
have neg : ∀
  (h :
    HMul.hMul (α := ℕ∞) (β := ℕ∞) ((↑m : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞) =
      HMul.hMul (α := ℕ∞) (β := ℕ∞) ((↑n : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞)),
  Associated (ϖ ^ m) (ϖ ^ n)
Tactic: simp only [hx', AddValuation.map_mul, addVal_eq_zero_of_unit, AddValuation.map_pow,
      nsmul_eq_mul, zero_add, hy', associated_unit_mul_right_iff,
      associated_unit_mul_left_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
n : ℕ
β : Rˣ
hy' : y = (↑β : R) * ϖ ^ n
h :
  HMul.hMul (α := ℕ∞) (β := ℕ∞) ((↑m : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞) =
    HMul.hMul (α := ℕ∞) (β := ℕ∞) ((↑n : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞)
⊢ Associated (ϖ ^ m) (ϖ ^ n)
have h₁ : m = n
Tactic: simp only [addVal_uniformizer hϖ, mul_one, ENat.coe_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
n : ℕ
β : Rˣ
hy' : y = (↑β : R) * ϖ ^ n
h : m = n
⊢ Associated (ϖ ^ m) (ϖ ^ n)
have neg : Associated (ϖ ^ n) (ϖ ^ n)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
this :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
⊢ (fun (n : ℕ∞ᵒᵈ) ↦
        (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
            ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
          Ideal R))
      ((fun (I : Ideal R) ↦
          ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
            ℕ∞ᵒᵈ))
        I) =
    I
have rwa : ∀
  (this :
    ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) =
      I),
  (fun (n : ℕ∞ᵒᵈ) ↦
        (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
            ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
          Ideal R))
      ((fun (I : Ideal R) ↦
          ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
            ℕ∞ᵒᵈ))
        I) =
    I
Tactic: rwa [Ideal.span_singleton_generator] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
⊢ (fun (n : ℕ∞ᵒᵈ) ↦
        (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
            ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
          Ideal R))
      ((fun (I : Ideal R) ↦
          ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
            ℕ∞ᵒᵈ))
        I) =
    I
have suffices : Eq.{u_1 + 1} (α := Ideal R)
  (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
    Ideal R)
  (span {x} : Ideal R)
Tactic: suffices (addVal R x).recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) = span {x} by
      rwa [Ideal.span_singleton_generator] at this
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have pos : ∀ (hx0 : x = 0),
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
pos :
  ∀ (hx0 : x = 0),
    Eq.{u_1 + 1} (α := Ideal R)
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
          (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
        Ideal R)
      (span {x} : Ideal R)
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg : ∀ (hx0 : ¬x = 0),
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg : ∀ (ϖ : R) (hϖ : Irreducible ϖ),
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
Tactic: obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg : ∀ (n : ℕ) (u : Rˣ) (hu : x = (↑u : R) * ϖ ^ n),
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
Tactic: obtain ⟨n, u, hu⟩ := eq_unit_mul_pow_irreducible hx0 hϖ
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = (↑u : R) * ϖ ^ n
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg : Eq.{u_1 + 1} (α := Ideal R)
  (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n)) :
    Ideal R)
  (span {(↑u : R) * ϖ ^ n} : Ideal R)
Tactic: rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_coe, hϖ.maximalIdeal_eq, span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = (↑u : R) * ϖ ^ n
neg :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n)) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg₁ : Eq.{u_1 + 1} (α := Ideal R)
  (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
      (↑n : ℕ∞) :
    Ideal R)
  (span {(↑u : R) * ϖ ^ n} : Ideal R)
Tactic: rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_coe, hϖ.maximalIdeal_eq, span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = (↑u : R) * ϖ ^ n
neg :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n)) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₁ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg₂ : Eq.{u_1 + 1} (α := Ideal R)
  (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
      (↑n : ℕ∞) :
    Ideal R)
  (span {ϖ ^ n} : Ideal R)
Tactic: rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_coe, hϖ.maximalIdeal_eq, span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = (↑u : R) * ϖ ^ n
neg :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n)) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₁ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₂ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {ϖ ^ n} : Ideal R)
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg₃ : HPow.hPow (α := Ideal R) (maximalIdeal R) n = span {ϖ ^ n}
Tactic: rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_coe, hϖ.maximalIdeal_eq, span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = (↑u : R) * ϖ ^ n
neg :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n)) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₁ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₂ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {ϖ ^ n} : Ideal R)
neg₃ : HPow.hPow (α := Ideal R) (maximalIdeal R) n = span {ϖ ^ n}
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg₄ : HPow.hPow (α := Ideal R) (span {ϖ}) n = span {ϖ ^ n}
Tactic: rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_coe, hϖ.maximalIdeal_eq, span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = (↑u : R) * ϖ ^ n
neg :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n)) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₁ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₂ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {ϖ ^ n} : Ideal R)
neg₃ : HPow.hPow (α := Ideal R) (maximalIdeal R) n = span {ϖ ^ n}
neg₄ : HPow.hPow (α := Ideal R) (span {ϖ}) n = span {ϖ ^ n}
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
have neg₅ : Eq (α := Ideal R) (span {ϖ ^ n}) (span {ϖ ^ n})
Tactic: rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_coe, hϖ.maximalIdeal_eq, span_singleton_pow]