awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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.{u_3 + 1} (α := B) ((e : (a : A) → B) (↑a : A) : B) (0 : B)

Tactic:
simp only [ne_eq, EmbeddingLike.map_eq_zero_iff, ZeroMemClass.coe_eq_zero,
      ha, not_false_eq_true]

Premises used: ZeroMemClass.coe_eq_zero, ne_eq, not_false_eq_true, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
refine : Membership.mem (α := B) (γ := Submodule B B) (maximalIdeal B) ((e : (a : A) → B) (↑a : A) : B)
⊢ ∃ (x : B), Membership.mem (γ := Submodule B B) (maximalIdeal B) x ∧ x ≠ 0

Tactic:
refine ⟨e a, ⟨?_, by simp only [ne_eq, EmbeddingLike.map_eq_zero_iff, ZeroMemClass.coe_eq_zero,
      ha, not_false_eq_true]⟩⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
rw : Membership.mem (γ := Ideal A) (maximalIdeal A) (↑a : A)
⊢ Membership.mem (α := B) (γ := Submodule B B) (maximalIdeal B) ((e : (a : A) → B) (↑a : A) : B)

Tactic:
rw [IsLocalRing.mem_maximalIdeal, map_mem_nonunits_iff e, ← IsLocalRing.mem_maximalIdeal]

Premises used: IsLocalRing.mem_maximalIdeal, map_mem_nonunits_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 (γ := Ideal A) (maximalIdeal A) (↑a : A)

Tactic:
a.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 (γ := Ideal A) (maximalIdeal A) (↑a : A)

Tactic:
exact a.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
⊢ WfDvdMonoid R

Tactic:
have : WfDvdMonoid R := IsNoetherianRing.wfDvdMonoid
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
obtain : ∀ (fx : Multiset R) (hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x), ∃ (n : ℕ), Associated x (ϖ ^ n)
⊢ ∃ (n : ℕ), Associated x (ϖ ^ n)

Tactic:
obtain ⟨fx, hfx⟩ := WfDvdMonoid.exists_factors x hx

Premises used: WfDvdMonoid.exists_factors
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 x (ϖ ^ fx.card)
⊢ ∃ (n : ℕ), Associated x (ϖ ^ n)

Tactic:
use Multiset.card fx

Premises used: Multiset.card
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 fx.prod x

Tactic:
have H := hfx.2
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
h :
  ∀ (H : Eq (α := Associates R) (Associates.mk fx.prod) (Associates.mk x)),
    Eq (α := Associates R) (Associates.mk x) (Associates.mk (ϖ ^ fx.card))
⊢ Associated x (ϖ ^ fx.card)

Tactic:
rw [← Associates.mk_eq_mk_iff_associated] at H ⊢

Premises used: Associates.mk_eq_mk_iff_associated
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
h :
  Eq (α := Associates R) (Multiset.prod (Multiset.map Associates.mk fx))
    (Multiset.prod (Multiset.replicate fx.card (Associates.mk ϖ)))
⊢ Eq (α := Associates R) (Associates.mk x) (Associates.mk (ϖ ^ fx.card))

Tactic:
rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]

Premises used: Multiset.prod_replicate, Associates.mk_pow, Associates.prod_mk
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
h : Eq (α := Multiset (Associates R)) (Multiset.map Associates.mk fx) (Multiset.replicate fx.card (Associates.mk ϖ))
⊢ Eq (α := Associates R) (Multiset.prod (Multiset.map Associates.mk fx))
    (Multiset.prod (Multiset.replicate fx.card (Associates.mk ϖ)))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
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 ϖ
⊢ Eq (α := Multiset (Associates R)) (Multiset.map Associates.mk fx) (Multiset.replicate fx.card (Associates.mk ϖ))

Tactic:
rw [Multiset.eq_replicate]

Premises used: Multiset.eq_replicate
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
h : ∀ (b : Associates R), ∀ x ∈ fx, Associates.mk x = b → b = Associates.mk ϖ
⊢ 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:
simp only [true_and, and_imp, Multiset.card_map, Multiset.mem_map, exists_imp]

Premises used: and_imp, Multiset.mem_map, exists_imp, true_and, Multiset.card_map
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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_1 : x_1 ∈ fx
h : Associated x_1 ϖ
⊢ Eq (α := Associates R) (Associates.mk x_1) (Associates.mk ϖ)

Tactic:
rw [Associates.mk_eq_mk_iff_associated]

Premises used: Associates.mk_eq_mk_iff_associated
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ϖ

Tactic:
associated_of_irreducible _ ?_ hirr

Premises used: IsDiscreteValuationRing.associated_of_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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_1 : x_1 ∈ fx
h : Irreducible x_1
⊢ Associated x_1 ϖ

Tactic:
refine associated_of_irreducible _ ?_ hirr

Premises used: IsDiscreteValuationRing.associated_of_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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_1 h : x_1 ∈ fx
⊢ Irreducible x_1

Tactic:
apply hfx.1

Premises used: And.left
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
⊢ x_1 ∈ fx

Tactic:
assumption
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
obtain : ∀ (n : ℕ) (hn : Associated x (ϖ ^ n)), ∃ (n : ℕ) (u : Rˣ), x = (↑u : R) * ϖ ^ n
⊢ ∃ (n : ℕ) (u : Rˣ), x = (↑u : R) * ϖ ^ n

Tactic:
obtain ⟨n, hn⟩ := associated_pow_irreducible hx hirr

Premises used: IsDiscreteValuationRing.associated_pow_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
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
⊢ ∃ (n : ℕ) (u : Rˣ), x = (↑u : R) * ϖ ^ n

Tactic:
obtain ⟨u, rfl⟩ := hn.symm

Premises used: Associated.symm, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
h : ϖ ^ n * (↑u : R) = (↑u : R) * ϖ ^ n
⊢ ∃ (n_1 : ℕ) (u_1 : Rˣ), ϖ ^ n * (↑u : R) = (↑u_1 : R) * ϖ ^ n_1

Tactic:
use n, u
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 * (↑u : R) = (↑u : R) * ϖ ^ n

Tactic:
apply mul_comm

Premises used: mul_comm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
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
⊢ ∃ (n : ℤ) (u : Rˣ), x = u • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) n

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
⊢ x ≠ 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
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
⊢ ∃ (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 ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible (x := x) (by simp_all) hϖ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ϖ
y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
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
⊢ y ≠ 0

Tactic:
simpa using hy
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ϖ
y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
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
obtain :
  ∀ (m : ℕ) (v : Rˣ) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ((↑v : R) * ϖ ^ m))
    (hx :
      HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
          ((algebraMap R K : (a : R) → K) ((↑v : R) * ϖ ^ m) : 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) ((↑v : R) * ϖ ^ m) : K) =
        u_1 • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) n_1
⊢ ∃ (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 ⟨m, v, rfl⟩ := eq_unit_mul_pow_irreducible (by simpa using hy) hϖ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ((↑v : R) * ϖ ^ m)
hx :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
      ((algebraMap R K : (a : R) → K) ((↑v : R) * ϖ ^ m) : K) ≠
    0
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) (0 : K)

Tactic:
simpa using hϖ.ne_zero

Premises used: Irreducible.ne_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ((↑v : R) * ϖ ^ m)
hx :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
      ((algebraMap R K : (a : R) → K) ((↑v : R) * ϖ ^ m) : K) ≠
    0
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) (0 : K)

Tactic:
have hϖ' : algebraMap R K ϖ ≠ 0 := by simpa using hϖ.ne_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ((↑v : R) * ϖ ^ m)
hx :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
      ((algebraMap R K : (a : R) → K) ((↑v : R) * ϖ ^ m) : K) ≠
    0
hϖ' : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) (0 : K)
⊢ ∃ (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) ((↑v : R) * ϖ ^ m) : K) =
      u_1 • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) n_1

Tactic:
⟨n - m, u / v, ?_⟩

Premises used: HSub.hSub, HDiv.hDiv, Nat.cast, Exists.intro
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ((↑v : R) * ϖ ^ m)
hx :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
      ((algebraMap R K : (a : R) → K) ((↑v : R) * ϖ ^ m) : K) ≠
    0
hϖ' : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) (0 : K)
refine :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
      ((algebraMap R K : (a : R) → K) ((↑v : R) * ϖ ^ m) : K) =
    (u / v) • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ))
⊢ ∃ (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) ((↑v : R) * ϖ ^ m) : K) =
      u_1 • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) n_1

Tactic:
refine ⟨n - m, u / v, ?_⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ((↑v : R) * ϖ ^ m)
hx :
  HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
      ((algebraMap R K : (a : R) → K) ((↑v : R) * ϖ ^ m) : K) ≠
    0
hϖ' : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) (0 : K)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) ((↑u : R) * ϖ ^ n) : K)
      ((algebraMap R K : (a : R) → K) ((↑v : R) * ϖ ^ m) : K) =
    (u / v) • HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) ϖ : K) (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ))

Tactic:
simp [hϖ', zpow_sub₀, div_smul_div_comm, Units.smul_def u, Units.smul_def v, Algebra.smul_def]

Premises used: zpow_sub₀, Units.smul_def, div_smul_div_comm, Algebra.smul_def
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
rw : ¬s = ⊥
⊢ generator s ≠ 0

Tactic:
rw [Ne, ← eq_bot_iff_generator_eq_zero]

Premises used: Ne, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ ¬s = ⊥

Tactic:
assumption
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ generator s ≠ 0

Tactic:
have gen_ne_zero : generator s ≠ 0 := by
    rw [Ne, ← eq_bot_iff_generator_eq_zero]
    assumption
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
rcases : ∀ (n : ℕ) (u : Rˣ) (hnu : generator s * (↑u : R) = ϖ ^ n), ∃ (n : ℕ), s = span {ϖ ^ n}
⊢ ∃ (n : ℕ), s = span {ϖ ^ n}

Tactic:
rcases associated_pow_irreducible gen_ne_zero hirr with ⟨n, u, hnu⟩

Premises used: IsDiscreteValuationRing.associated_pow_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * (↑u : R) = ϖ ^ n
h : s = span {ϖ ^ n}
⊢ ∃ (n : ℕ), s = span {ϖ ^ n}

Tactic:
use n
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * (↑u : R) = ϖ ^ n
⊢ span {generator s} = s

Tactic:
have : span _ = _ := Ideal.span_singleton_generator s
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * (↑u : R) = ϖ ^ n
this : span {generator s} = s
h : Associated (generator s) (generator s * (↑u : R))
⊢ s = span {ϖ ^ n}

Tactic:
rw [← this, ← hnu, span_singleton_eq_span_singleton]

Premises used: Ideal.span_singleton_eq_span_singleton
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * (↑u : R) = ϖ ^ n
this : span {generator s} = s
w : Rˣ
h : generator s * (↑u : R) = generator s * (↑u : R)
⊢ Associated (generator s) (generator s * (↑u : R))

Tactic:
use u
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
rw : ∃ (u : Rˣ), p ^ m * (↑u : R) = q ^ n
⊢ Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod

Tactic:
rw [Multiset.prod_replicate, Multiset.prod_replicate, Associated]

Premises used: Multiset.prod_replicate, Associated