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
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
inl : ∀ (H : n < 1), Associated p ϖ
inr : ∀ (hn : Associated (HPow.hPow (β := ℕ) ϖ 1) p) (this : Irreducible (HPow.hPow (β := ℕ) ϖ 1)), Associated p ϖ
⊢ Associated p ϖ
have inr₁ : ∀ (H : 1 < n), Associated p ϖ
Tactic: rcases lt_trichotomy n 1 with (H | rfl | H)
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
H : n < 1
⊢ n = 0
have revert : ∀ (n : ℕ) (H : n < 1), n = 0
Tactic: revert H n
Cleared hypotheses: n, H
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
⊢ Associated p ϖ
have hn₁ : Associated (HPow.hPow (β := ℕ) ϖ 0) p
Tactic: obtain rfl : n = 0 := by
      clear hn this
      revert H n
      decide
Cleared hypotheses: n, hn, this, H
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
hn₁ : Associated (HPow.hPow (β := ℕ) ϖ 0) p
⊢ Associated p ϖ
have this₁ : Irreducible (HPow.hPow (β := ℕ) ϖ 0)
Tactic: obtain rfl : n = 0 := by
      clear hn this
      revert H n
      decide
Cleared hypotheses: n, hn, this, H
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
hn₁ : Associated (HPow.hPow (β := ℕ) ϖ 0) p
this₁ : Irreducible (HPow.hPow (β := ℕ) ϖ 0)
⊢ Associated p ϖ
have H₁ : LT.lt (α := ℕ) 0 1
Tactic: obtain rfl : n = 0 := by
      clear hn this
      revert H n
      decide
Cleared hypotheses: n, hn, this, H
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : 1 < n
⊢ Associated p ϖ
have inr : ∀ (n : ℕ) (hn : Associated (ϖ ^ (1 + n + 1)) p) (this : Irreducible (ϖ ^ (1 + n + 1))) (H : 1 < 1 + n + 1),
  Associated p ϖ
Tactic: obtain ⟨n, rfl⟩ : ∃ k, n = 1 + k + 1 := Nat.exists_eq_add_of_lt H
Cleared hypotheses: n, hn, this, H
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ ^ (1 + n + 1))
H : 1 < 1 + n + 1
⊢ Associated p ϖ
have this₁ : Irreducible (ϖ * ϖ ^ (1 + n))
Tactic: rw [pow_succ'] at this
Cleared hypotheses: this, H
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
⊢ Associated p ϖ
have inr : ∀ (H0 : IsUnit ϖ), Associated p ϖ
Tactic: rcases this.isUnit_or_isUnit rfl with (H0 | H0)
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
inr : ∀ (H0 : IsUnit ϖ), Associated p ϖ
⊢ Associated p ϖ
have inr₁ : ∀ (H0 : IsUnit (ϖ ^ (1 + n))), Associated p ϖ
Tactic: rcases this.isUnit_or_isUnit rfl with (H0 | H0)
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ ^ (1 + n))
⊢ Associated p ϖ
have H0₁ : IsUnit (ϖ * ϖ ^ n)
Tactic: rw [add_comm, pow_succ'] at H0
Cleared hypotheses: H0
-- 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
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod x
have h : (∀
    b ∈
      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)
          sorry)
        p,
    Prime b) ∧
  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)
          sorry)
        p).prod
    x
Tactic: use Multiset.replicate (Classical.choose (spec.2 hx)) p
-- 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
⊢ (∀
      b ∈
        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,
      Prime b) ∧
    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 : ∀
  b ∈
    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)
        sorry)
      p,
  Prime b
Tactic: constructor
-- 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
h :
  ∀
    b ∈
      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,
    Prime b
⊢ (∀
      b ∈
        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,
      Prime b) ∧
    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
  (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)
        sorry)
      p).prod
  x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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
⊢ Prime q
have hpq : q = p
Tactic: have hpq := Multiset.eq_of_mem_replicate hq
-- 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
⊢ Prime q
have h : Prime p
Tactic: rw [hpq]
-- 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
⊢ Prime p
have h : ∀ (a b : R), p ∣ a * b → p ∣ a ∨ p ∣ b
Tactic: refine ⟨spec.1.ne_zero, spec.1.not_isUnit, ?_⟩
-- 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
a b : R
h : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b
have pos : ∀ (ha : a = 0), p ∣ a ∨ p ∣ b
Tactic: by_cases ha : a = 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
a b : R
h : p ∣ a * b
pos : ∀ (ha : a = 0), p ∣ a ∨ p ∣ b
⊢ p ∣ a ∨ p ∣ b
have neg : ∀ (ha : ¬a = 0), p ∣ a ∨ p ∣ b
Tactic: by_cases ha : a = 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
a b : R
h : p ∣ a * b
ha : a = 0
⊢ p ∣ a ∨ p ∣ b
have pos : p ∣ 0 ∨ p ∣ b
Tactic: rw [ha]
-- 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
a b : R
h : p ∣ a * b
ha : ¬a = 0
⊢ p ∣ a ∨ p ∣ b
have neg : ∀ (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 *
          (↑u : R) *
        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),
  p ∣
      Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
            hR ^
          m *
        (↑u : R) ∨
    p ∣ b
Tactic: obtain ⟨m, u, rfl⟩ := spec.2 ha
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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 *
        (↑u : R) *
      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
⊢ p ∣
      Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
            hR ^
          m *
        (↑u : R) ∨
    p ∣ b
have 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
Tactic: rw [mul_assoc, mul_left_comm, Units.dvd_mul_left] at h
Cleared hypotheses: h, ha
-- 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
⊢ p ∣
      Classical.choose (p := fun (x : R) ↦ Irreducible x ∧ ∀ {x_1 : R}, x_1 ≠ 0 → ∃ (n : ℕ), Associated (x ^ n) x_1)
            hR ^
          m *
        (↑u : R) ∨
    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 ∨
  p ∣ b
Tactic: rw [Units.dvd_mul_right]
-- 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
⊢ 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 : ∀ (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