awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
principal principal₁ : ∀ (I : Ideal R), Submodule.IsPrincipal I
pos : ∀ (I : Ideal R) (I0 : I = ⊥), Submodule.IsPrincipal I
neg neg₁ : ∀ (I : Ideal R) (I0 : ¬I = ⊥), Submodule.IsPrincipal I
neg₂ : ∀ (I : Ideal R) (I0 : ¬I = ⊥) (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0), Submodule.IsPrincipal I
neg₃ :
  ∀ (I : Ideal R) (I0 : ¬I = ⊥) (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0) (p : R),
    Irreducible p → ∀ (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x), Submodule.IsPrincipal I
neg₄ :
  ∀ (I : Ideal R) (I0 : ¬I = ⊥) (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0) (p : R),
    Irreducible p →
      ∀ (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x) (ex : ∃ (n : ℕ), p ^ n ∈ I), Submodule.IsPrincipal I
neg₅ :
  ∀ (I : Ideal R) (I0 : ¬I = ⊥) (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0) (p : R),
    Irreducible p →
      ∀ (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x) (ex : ∃ (n : ℕ), p ^ n ∈ I), ∃ (a : R), I = R ∙ a
h :
  ∀ (I : Ideal R) (I0 : ¬I = ⊥) (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0) (p : R),
    Irreducible p →
      ∀ (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x) (ex : ∃ (n : ℕ), p ^ n ∈ I),
        I = R ∙ p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex
h₃ :
  ∀ (I : Ideal R) (I0 : ¬I = ⊥) (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0) (p : R),
    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}
h₄ :
  ∀ (I : Ideal R) (I0 : ¬I = ⊥) (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0) (p : R),
    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}
⊢ IsPrincipalIdealRing R
have h₅ : ∀ (I : Ideal R) (I0 : ¬I = ⊥) (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0) (p : R),
  Irreducible p →
    ∀ (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x) (ex : ∃ (n : ℕ), p ^ n ∈ I),
      span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex} ≤ I
Tactic: classical
  constructor
  intro I
  by_cases I0 : I = ⊥
  · rw [I0]
    use 0
    simp only [Set.singleton_zero, Submodule.span_zero]
  obtain ⟨x, hxI, hx0⟩ : ∃ x ∈ I, x ≠ (0 : R) := I.ne_bot_iff.mp I0
  obtain ⟨p, _, H⟩ := HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible h₁ h₂
  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
  constructor
  use p ^ Nat.find ex
  change I = Ideal.span _
  apply le_antisymm
  · intro r hr
    by_cases hr0 : r = 0
    · simp only [hr0, Submodule.zero_mem]
    obtain ⟨n, u, rfl⟩ := H hr0
    simp only [mem_span_singleton, Units.isUnit, IsUnit.dvd_mul_right]
    apply pow_dvd_pow
    apply Nat.find_min'
    simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hr
  · rw [span_singleton_le_iff_mem]
    exact Nat.find_spec ex
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsDiscreteValuationRing R
have rw : IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
Tactic: rw [iff_pid_with_one_nonzero_prime]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have PID : IsPrincipalIdealRing R
Tactic: haveI PID : IsPrincipalIdealRing R := aux_pid_of_ufd_of_unique_irreducible R h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₁ : ∃ (p : R), Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have obtain : ∀ (p : R) (hp : Irreducible p), IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
Tactic: obtain ⟨p, hp⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have refine_1 : Ne (α := Ideal R) (span {p}) ⊥
Tactic: refine ⟨PID, ⟨Ideal.span {p}, ⟨?_, ?_⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
refine_1 : Ne (α := Ideal R) (span {p}) ⊥
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have refine_2 : IsPrime (α := R) (span {p})
Tactic: refine ⟨PID, ⟨Ideal.span {p}, ⟨?_, ?_⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
refine_1 : Ne (α := Ideal R) (span {p}) ⊥
refine_2 : IsPrime (α := R) (span {p})
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
have refine_3 : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}
Tactic: refine ⟨PID, ⟨Ideal.span {p}, ⟨?_, ?_⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ Ne (α := Ideal R) (span {p}) ⊥
have refine_1 : ∃ (x : R), Membership.mem (γ := Submodule R R) (span {p}) x ∧ x ≠ 0
Tactic: rw [Submodule.ne_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ IsPrime (α := R) (span {p})
have refine_2 : Prime p
Tactic: rwa [Ideal.span_singleton_prime hp.ne_zero, ← UniqueFactorizationMonoid.irreducible_iff_prime]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
⊢ (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) I → I = span {p}
have refine_3 : (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (R ∙ Submodule.IsPrincipal.generator I) →
  Eq (α := Ideal R) (R ∙ Submodule.IsPrincipal.generator I) (span {p})
Tactic: rw [← Submodule.IsPrincipal.span_singleton_generator I]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Ne (α := Ideal R) (R ∙ Submodule.IsPrincipal.generator I) ⊥
hI : IsPrime (R ∙ Submodule.IsPrincipal.generator I)
⊢ Eq (α := Ideal R) (R ∙ Submodule.IsPrincipal.generator I) (span {p})
have refine_3 : Associated (Submodule.IsPrincipal.generator I) p
Tactic: apply span_singleton_eq_span_singleton.mpr
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Ne (α := Ideal R) (R ∙ Submodule.IsPrincipal.generator I) ⊥
hI : IsPrime (R ∙ Submodule.IsPrincipal.generator I)
⊢ Associated (Submodule.IsPrincipal.generator I) p
have apply : Irreducible (Submodule.IsPrincipal.generator I)
Tactic: apply h₂ _ hp
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Ne (α := Ideal R) (R ∙ Submodule.IsPrincipal.generator I) ⊥
hI : IsPrime (R ∙ Submodule.IsPrincipal.generator I)
⊢ Irreducible (Submodule.IsPrincipal.generator I)
have I0₁ : ¬Submodule.IsPrincipal.generator I = 0
Tactic: rw [Ne, Submodule.span_singleton_eq_bot] at I0
Cleared hypotheses: I0, hI
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : ¬Submodule.IsPrincipal.generator I = 0
hI : IsPrime (R ∙ Submodule.IsPrincipal.generator I)
⊢ Irreducible (Submodule.IsPrincipal.generator I)
have rwa : Prime (Submodule.IsPrincipal.generator I)
Tactic: rwa [UniqueFactorizationMonoid.irreducible_iff_prime, ← Ideal.span_singleton_prime I0]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : ¬Submodule.IsPrincipal.generator I = 0
hI : IsPrime (R ∙ Submodule.IsPrincipal.generator I)
rwa : Prime (Submodule.IsPrincipal.generator I)
⊢ Irreducible (Submodule.IsPrincipal.generator I)
have rwa₁ : IsPrime (α := R) (span {Submodule.IsPrincipal.generator I})
Tactic: rwa [UniqueFactorizationMonoid.irreducible_iff_prime, ← Ideal.span_singleton_prime I0]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := ⋯
⊢ IsDiscreteValuationRing R
have apply : ∃ (p : R), Irreducible p
Tactic: apply of_ufd_of_unique_irreducible _ hR.unique_irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := ⋯
⊢ ∃ (p : R), Irreducible p
have obtain : ∀ (p : R) (hp : Irreducible p) (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x), ∃ (p : R), Irreducible p
Tactic: obtain ⟨p, hp, H⟩ := hR
Cleared hypotheses: hR, this
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
A : Type u_2
B : Type u_3
E : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : IsDiscreteValuationRing A
inst_5 : EquivLike E A B
inst_6 : RingEquivClass E A B
e : E
⊢ Ne (α := Ideal B) (maximalIdeal B) ⊥
have obtain : ∀ (a : ↥(maximalIdeal A)) (ha : a ≠ 0), Ne (α := Ideal B) (maximalIdeal B) ⊥
Tactic: obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr
      <| IsDiscreteValuationRing.not_a_field A)
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
A : Type u_2
B : Type u_3
E : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : IsDiscreteValuationRing A
inst_5 : EquivLike E A B
inst_6 : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ Ne (α := Ideal B) (maximalIdeal B) ⊥
have rw : ∃ (x : B), Membership.mem (γ := Submodule B B) (maximalIdeal B) x ∧ x ≠ 0
Tactic: rw [Submodule.ne_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
A : Type u_2
B : Type u_3
E : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : IsDiscreteValuationRing A
inst_5 : EquivLike E A B
inst_6 : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ ∃ (x : B), Membership.mem (γ := Submodule B B) (maximalIdeal B) x ∧ x ≠ 0
have refine : Membership.mem (α := B) (γ := Submodule B B) (maximalIdeal B) ((e : (a : A) → B) (↑a : A) : B)
Tactic: refine ⟨e a, ⟨?_, by simp only [ne_eq, EmbeddingLike.map_eq_zero_iff, ZeroMemClass.coe_eq_zero,
      ha, not_false_eq_true]⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
A : Type u_2
B : Type u_3
E : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : IsDiscreteValuationRing A
inst_5 : EquivLike E A B
inst_6 : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ Membership.mem (α := B) (γ := Submodule B B) (maximalIdeal B) ((e : (a : A) → B) (↑a : A) : B)
have rw : Membership.mem (γ := Ideal A) (maximalIdeal A) (↑a : A)
Tactic: rw [IsLocalRing.mem_maximalIdeal, map_mem_nonunits_iff e, ← IsLocalRing.mem_maximalIdeal]
-- 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 : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
⊢ ∃ (n : ℕ), Associated x (ϖ ^ n)
have this : WfDvdMonoid R
Tactic: have : WfDvdMonoid R := IsNoetherianRing.wfDvdMonoid
-- 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
hirr : Irreducible ϖ
this : WfDvdMonoid R
⊢ ∃ (n : ℕ), Associated x (ϖ ^ n)
have obtain : ∀ (fx : Multiset R) (hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x), ∃ (n : ℕ), Associated x (ϖ ^ n)
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 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
⊢ ∃ (n : ℕ), Associated x (ϖ ^ n)
have h : Associated x (ϖ ^ fx.card)
Tactic: use Multiset.card fx
-- 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 : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
⊢ Associated x (ϖ ^ fx.card)
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 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associated fx.prod x
⊢ Associated x (ϖ ^ fx.card)
have h : ∀ (H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)),
  Eq (α := Associates R) (Associates.mk x) (Associates.mk (ϖ ^ fx.card))
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 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
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 x) (Associates.mk (ϖ ^ fx.card))
have h : Eq (α := Associates R) (Multiset.prod (Multiset.map Associates.mk fx))
  (Multiset.prod (Multiset.replicate fx.card (Associates.mk ϖ)))
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 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
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.map Associates.mk fx))
    (Multiset.prod (Multiset.replicate fx.card (Associates.mk ϖ)))
have h : Eq (α := Multiset (Associates R)) (Multiset.map Associates.mk fx) (Multiset.replicate fx.card (Associates.mk ϖ))
Tactic: congr 1
-- 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
hirr : Irreducible ϖ
this : WfDvdMonoid R
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 ϖ))
have h : 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 ϖ
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 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
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 ϖ
have h : ∀ (b : Associates R), ∀ x ∈ fx, Associates.mk x = b → b = Associates.mk ϖ
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 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)
x_1 : R
h : x_1 ∈ fx
⊢ Eq (α := Associates R) (Associates.mk x_1) (Associates.mk ϖ)
have h : Associated x_1 ϖ
Tactic: rw [Associates.mk_eq_mk_iff_associated]
-- 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
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)
x_1 : R
h : x_1 ∈ fx
⊢ Associated x_1 ϖ
have h : Irreducible x_1
Tactic: refine associated_of_irreducible _ ?_ hirr
-- 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
hirr : Irreducible ϖ
⊢ ∃ (n : ℕ) (u : Rˣ), x = (↑u : R) * ϖ ^ n
have obtain : ∀ (n : ℕ) (hn : Associated x (ϖ ^ n)), ∃ (n : ℕ) (u : Rˣ), x = (↑u : R) * ϖ ^ n
Tactic: obtain ⟨n, hn⟩ := associated_pow_irreducible hx hirr
-- 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
hirr : Irreducible ϖ
n : ℕ
hn : Associated x (ϖ ^ n)
⊢ ∃ (n : ℕ) (u : Rˣ), x = (↑u : R) * ϖ ^ n
have obtain : ∀ (u : Rˣ) (hx : ϖ ^ n * (↑u : R) ≠ 0) (hn : Associated (ϖ ^ n * (↑u : R)) (ϖ ^ n)),
  ∃ (n_1 : ℕ) (u_1 : Rˣ), ϖ ^ n * (↑u : R) = (↑u_1 : R) * ϖ ^ n_1
Tactic: obtain ⟨u, rfl⟩ := hn.symm
Cleared hypotheses: x, hx, hn
-- 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
ϖ : R
hirr : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ϖ ^ n * (↑u : R) ≠ 0
hn : Associated (ϖ ^ n * (↑u : R)) (ϖ ^ n)
⊢ ∃ (n_1 : ℕ) (u_1 : Rˣ), ϖ ^ n * (↑u : R) = (↑u_1 : R) * ϖ ^ n_1
have h : ϖ ^ n * (↑u : R) = (↑u : R) * ϖ ^ n
Tactic: use n, u
-- 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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
x : K
hx : x ≠ 0
⊢ ∃ (n : ℤ) (u : Rˣ), x = u • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) n
have obtain : ∀ (x y : R) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y)
  (hx : HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K) ≠ 0),
  ∃ (n : ℤ) (u : Rˣ),
    HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K) =
      u • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) n
Tactic: obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) x
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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
x y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
hx : HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K) ≠ 0
⊢ ∃ (n : ℤ) (u : Rˣ),
    HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K) =
      u • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) n
have obtain : ∀ (n : ℕ) (u : Rˣ)
  (hx :
    HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
        ((algebraMap R K : (a : R) → K) y : K) ≠
      0),
  ∃ (n_1 : ℤ) (u_1 : Rˣ),
    HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
        ((algebraMap R K : (a : R) → K) y : K) =
      u_1 • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) n_1
Tactic: obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible (x := x) (by simp_all) hϖ
Cleared hypotheses: x, hx