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 : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R :=
  Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR
spec : Irreducible
    (Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
      hR) ∧
  ∀ {x : R},
    x ≠ 0 →
      ∃ (n : ℕ),
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
            n)
          x :=
  ⋯
x : R
hx : x ≠ 0
q : R
hq :
  q ∈
    Multiset.replicate
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_2 : R}, x_2 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_2) hR ^
            x_1)
          x)
        ⋯)
      p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h :
  p ∣
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
        m *
      b
ha :
  ¬Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
          m *
        (↑u : R) =
      0
pos :
  ∀ (hm : m = 0),
    p ∣
        Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
            hR ^
          m ∨
      p ∣ b
⊢ p ∣
      Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
          hR ^
        m ∨
    p ∣ b
have neg : ∀ (hm : ¬m = 0),
  p ∣
      Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
          hR ^
        m ∨
    p ∣ b
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R :=
  Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR
spec : Irreducible
    (Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
      hR) ∧
  ∀ {x : R},
    x ≠ 0 →
      ∃ (n : ℕ),
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
            n)
          x :=
  ⋯
x : R
hx : x ≠ 0
q : R
hq :
  q ∈
    Multiset.replicate
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_2 : R}, x_2 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_2) hR ^
            x_1)
          x)
        ⋯)
      p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h :
  p ∣
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
        m *
      b
ha :
  ¬Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
          m *
        (↑u : R) =
      0
hm : m = 0
⊢ p ∣
      Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
          hR ^
        m ∨
    p ∣ b
have pos : ∀ (h : p ∣ b), p ∣ 1 ∨ p ∣ b
Tactic: simp only [hm, one_mul, pow_zero] 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 : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R :=
  Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR
spec : Irreducible
    (Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
      hR) ∧
  ∀ {x : R},
    x ≠ 0 →
      ∃ (n : ℕ),
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
            n)
          x :=
  ⋯
x : R
hx : x ≠ 0
q : R
hq :
  q ∈
    Multiset.replicate
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_2 : R}, x_2 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_2) hR ^
            x_1)
          x)
        ⋯)
      p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h :
  p ∣
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
        m *
      b
ha :
  ¬Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
          m *
        (↑u : R) =
      0
hm : ¬m = 0
⊢ p ∣
      Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
          hR ^
        m ∨
    p ∣ b
have neg : p ∣
  Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^ m
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R :=
  Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR
spec : Irreducible
    (Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
      hR) ∧
  ∀ {x : R},
    x ≠ 0 →
      ∃ (n : ℕ),
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
            n)
          x :=
  ⋯
x : R
hx : x ≠ 0
q : R
hq :
  q ∈
    Multiset.replicate
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_2 : R}, x_2 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_2) hR ^
            x_1)
          x)
        ⋯)
      p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h :
  p ∣
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
        m *
      b
ha :
  ¬Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
          m *
        (↑u : R) =
      0
hm : ¬m = 0
⊢ p ∣
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
      m
have neg : ∀ (m : ℕ)
  (h :
    p ∣
      Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
            hR ^
          m.succ *
        b)
  (ha :
    ¬Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
            m.succ *
          (↑u : R) =
        0)
  (hm : ¬m.succ = 0),
  p ∣
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
      m.succ
Tactic: obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
Cleared hypotheses: m, h, ha, hm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R :=
  Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR
spec : Irreducible
    (Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
      hR) ∧
  ∀ {x : R},
    x ≠ 0 →
      ∃ (n : ℕ),
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
            n)
          x :=
  ⋯
x : R
hx : x ≠ 0
q : R
hq :
  q ∈
    Multiset.replicate
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_2 : R}, x_2 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_2) hR ^
            x_1)
          x)
        ⋯)
      p
hpq : q = p
b : R
u : Rˣ
m : ℕ
h :
  p ∣
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
        m.succ *
      b
ha :
  ¬Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
          m.succ *
        (↑u : R) =
      0
hm : ¬m.succ = 0
⊢ p ∣
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
      m.succ
have neg : p ∣
  Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR *
    Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
      m
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R :=
  Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR
spec : Irreducible
    (Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
      hR) ∧
  ∀ {x : R},
    x ≠ 0 →
      ∃ (n : ℕ),
        Associated
          (Classical.choose (p := fun (x : R) ↦
              Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1) hR ^
            n)
          x :=
  ⋯
x : R
hx : x ≠ 0
⊢ Associated
    (Multiset.replicate
        (Classical.choose (p := fun (x_1 : ℕ) ↦
          Associated
            (Classical.choose (p := fun (x : R) ↦
                Irreducible x ∧ ∀ {x_2 : R}, x_2 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_2) hR ^
              x_1)
            x)
          ⋯)
        p).prod
    x
have h : Associated
  (p ^
    Classical.choose (p := fun (x_1 : ℕ) ↦
      Associated
        (Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_2 : R}, x_2 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_2)
            hR ^
          x_1)
        x)
      sorry)
  x
Tactic: rw [Multiset.prod_replicate]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ HasUnitMulPowIrreducibleFactorization R
have obtain : ∀ (p : R) (hp : Irreducible p), HasUnitMulPowIrreducibleFactorization R
Tactic: obtain ⟨p, hp⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
⊢ HasUnitMulPowIrreducibleFactorization R
have refine : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
Tactic: refine ⟨p, hp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
⊢ ∃ (n : ℕ), Associated (p ^ n) x
have obtain : ∀ (fx : Multiset R) (hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x), ∃ (n : ℕ), Associated (p ^ n) x
Tactic: obtain ⟨fx, hfx⟩ := WfDvdMonoid.exists_factors x hx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
⊢ ∃ (n : ℕ), Associated (p ^ n) x
have refine : Associated (p ^ fx.card) x
Tactic: refine ⟨Multiset.card fx, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
⊢ Associated (p ^ fx.card) x
have H : Associated fx.prod x
Tactic: have H := hfx.2
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associated fx.prod x
⊢ Associated (p ^ fx.card) x
have rw : ∀ (H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)),
  Eq (α := Associates R) (Associates.mk (p ^ fx.card)) (Associates.mk x)
Tactic: rw [← Associates.mk_eq_mk_iff_associated] 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 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)
⊢ Eq (α := Associates R) (Associates.mk (p ^ fx.card)) (Associates.mk x)
have rw : Eq (α := Associates R) (Multiset.prod (Multiset.replicate fx.card (Associates.mk p)))
  (Multiset.prod (Multiset.map Associates.mk fx))
Tactic: rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)
⊢ Eq (α := Associates R) (Multiset.prod (Multiset.replicate fx.card (Associates.mk p)))
    (Multiset.prod (Multiset.map Associates.mk fx))
have e_a : Eq (α := Multiset (Associates R)) (Multiset.replicate fx.card (Associates.mk p)) (Multiset.map Associates.mk fx)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)
⊢ Eq (α := Multiset (Associates R)) (Multiset.replicate fx.card (Associates.mk p)) (Multiset.map Associates.mk fx)
have e_a : Eq (α := Multiset (Associates R)) (Multiset.map Associates.mk fx) (Multiset.replicate fx.card (Associates.mk p))
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)
⊢ Eq (α := Multiset (Associates R)) (Multiset.map Associates.mk fx) (Multiset.replicate fx.card (Associates.mk p))
have e_a : Multiset.card (α := Associates R) (Multiset.map Associates.mk fx) = fx.card ∧
  ∀ (b : Associates R),
    Membership.mem (γ := Multiset (Associates R)) (Multiset.map Associates.mk fx) b → b = Associates.mk p
Tactic: rw [Multiset.eq_replicate]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)
⊢ Multiset.card (α := Associates R) (Multiset.map Associates.mk fx) = fx.card ∧
    ∀ (b : Associates R),
      Membership.mem (γ := Multiset (Associates R)) (Multiset.map Associates.mk fx) b → b = Associates.mk p
have e_a : ∀ (b : Associates R), ∀ x ∈ fx, Associates.mk x = b → b = Associates.mk p
Tactic: simp only [true_and, and_imp, Multiset.card_map, Multiset.mem_map, exists_imp]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)
q : R
hq : q ∈ fx
⊢ Eq (α := Associates R) (Associates.mk q) (Associates.mk p)
have e_a : Associated q p
Tactic: rw [Associates.mk_eq_mk_iff_associated]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsPrincipalIdealRing R
have principal : ∀ (S : Ideal R), Submodule.IsPrincipal S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
⊢ Submodule.IsPrincipal I
have pos : ∀ (I0 : I = ⊥), Submodule.IsPrincipal I
Tactic: by_cases I0 : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
pos : ∀ (I0 : I = ⊥), Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal I
have neg : ∀ (I0 : ¬I = ⊥), Submodule.IsPrincipal I
Tactic: by_cases I0 : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : I = ⊥
⊢ Submodule.IsPrincipal I
have pos : Submodule.IsPrincipal.{u, u} (R := R) (M := R) ⊥
Tactic: rw [I0]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : I = ⊥
⊢ Submodule.IsPrincipal.{u, u} (R := R) (M := R) ⊥
have h : Eq (α := Submodule R R) ⊥ (R ∙ 0)
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
⊢ Submodule.IsPrincipal I
have neg : ∀ (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0), Submodule.IsPrincipal I
Tactic: obtain ⟨x, hxI, hx0⟩ : ∃ x ∈ I, x ≠ (0 : R) := I.ne_bot_iff.mp I0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
⊢ Submodule.IsPrincipal I
have neg : ∀ (p : R), Irreducible p → ∀ (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x), Submodule.IsPrincipal I
Tactic: obtain ⟨p, _, H⟩ := HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
⊢ ∃ (n : ℕ), p ^ n ∈ I
have obtain : ∀ (n : ℕ) (u : Rˣ) (hxI : p ^ n * (↑u : R) ∈ I) (hx0 : p ^ n * (↑u : R) ≠ 0), ∃ (n : ℕ), p ^ n ∈ I
Tactic: obtain ⟨n, u, rfl⟩ := H hx0
Cleared hypotheses: x, hxI, hx0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
p : R
left : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
n : ℕ
u : Rˣ
hxI : p ^ n * (↑u : R) ∈ I
hx0 : p ^ n * (↑u : R) ≠ 0
⊢ ∃ (n : ℕ), p ^ n ∈ I
have refine : p ^ n ∈ I
Tactic: refine ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
⊢ Submodule.IsPrincipal I
have ex : ∃ (n : ℕ), p ^ n ∈ I
Tactic: have ex : ∃ n : ℕ, p ^ n ∈ I := by
    obtain ⟨n, u, rfl⟩ := H hx0
    refine ⟨n, ?_⟩
    simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hxI
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
ex : ∃ (n : ℕ), p ^ n ∈ I
⊢ Submodule.IsPrincipal I
have neg : ∃ (a : R), I = R ∙ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
ex : ∃ (n : ℕ), p ^ n ∈ I
⊢ ∃ (a : R), I = R ∙ a
have h : I = R ∙ p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex
Tactic: use p ^ Nat.find ex
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
ex : ∃ (n : ℕ), p ^ n ∈ I
⊢ I = span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}
have h : I ≤ span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
ex : ∃ (n : ℕ), p ^ n ∈ I
h : I ≤ span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}
⊢ I = span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}
have h₃ : span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex} ≤ I
Tactic: apply le_antisymm