awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 : ∀ (S : Ideal R), Submodule.IsPrincipal S
⊢ IsPrincipalIdealRing R

Tactic:
constructor
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
neg : ∀ (I0 : ¬I = ⊥), Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal I

Tactic:
by_cases I0 : I = ⊥
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 = ⊥
pos : Submodule.IsPrincipal.{u, u} (R := R) (M := R) ⊥
⊢ Submodule.IsPrincipal I

Tactic:
rw [I0]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 = ⊥
h : Eq (α := Submodule R R) ⊥ (R ∙ 0)
⊢ Submodule.IsPrincipal.{u, u} (R := R) (M := R) ⊥

Tactic:
use 0
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 = ⊥
⊢ Eq (α := Submodule R R) ⊥ (R ∙ 0)

Tactic:
simp only [Set.singleton_zero, Submodule.span_zero]

Premises used: Submodule.span_zero, Set.singleton_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 ∈ I, x ≠ 0

Tactic:
I.ne_bot_iff.mp I0

Premises used: Set.Mem, Submodule.ne_bot_iff, Iff.mp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 = ⊥
neg : ∀ (x : R) (hxI : x ∈ I) (hx0 : x ≠ 0), Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal I

Tactic:
obtain ⟨x, hxI, hx0⟩ : ∃ x ∈ I, x ≠ (0 : R) := I.ne_bot_iff.mp I0

Premises used: Submodule.ne_bot_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
neg : ∀ (p : R), Irreducible p → ∀ (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x), Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal I

Tactic:
obtain ⟨p, _, H⟩ := HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible h₁ h₂

Premises used: IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
obtain : ∀ (n : ℕ) (u : Rˣ) (hxI : p ^ n * (↑u : R) ∈ I) (hx0 : p ^ n * (↑u : R) ≠ 0), ∃ (n : ℕ), p ^ n ∈ I
⊢ ∃ (n : ℕ), p ^ n ∈ I

Tactic:
obtain ⟨n, u, rfl⟩ := H hx0

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

Tactic:
⟨n, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
refine : p ^ n ∈ I
⊢ ∃ (n : ℕ), p ^ n ∈ I

Tactic:
refine ⟨n, ?_⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
⊢ p ^ n ∈ I

Tactic:
simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hxI

Premises used: Units.mul_inv_cancel_right, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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

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
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
neg : ∃ (a : R), I = R ∙ a
⊢ Submodule.IsPrincipal I

Tactic:
constructor
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 = R ∙ p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex
⊢ ∃ (a : R), I = R ∙ a

Tactic:
use p ^ Nat.find ex

Premises used: Nat.find
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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}
h₃ : span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex} ≤ I
⊢ I = span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
r : R
hr : r ∈ I
pos : ∀ (hr0 : r = 0), Membership.mem (γ := Submodule R R) (span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}) r
neg : ∀ (hr0 : ¬r = 0), Membership.mem (γ := Submodule R R) (span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}) r
⊢ Membership.mem (γ := Submodule R R) (span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}) r

Tactic:
by_cases hr0 : r = 0
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
r : R
hr : r ∈ I
hr0 : r = 0
⊢ Membership.mem (γ := Submodule R R) (span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}) r

Tactic:
simp only [hr0, Submodule.zero_mem]

Premises used: Submodule.zero_mem
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
r : R
hr : r ∈ I
hr0 : ¬r = 0
neg :
  ∀ (n : ℕ) (u : Rˣ) (hr : p ^ n * (↑u : R) ∈ I) (hr0 : ¬p ^ n * (↑u : R) = 0),
    Membership.mem (γ := Submodule R R) (span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}) (p ^ n * (↑u : R))
⊢ Membership.mem (γ := Submodule R R) (span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}) r

Tactic:
obtain ⟨n, u, rfl⟩ := H hr0

Premises used: rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
n : ℕ
u : Rˣ
hr : p ^ n * (↑u : R) ∈ I
hr0 : ¬p ^ n * (↑u : R) = 0
neg : p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex ∣ p ^ n
⊢ Membership.mem (γ := Submodule R R) (span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex}) (p ^ n * (↑u : R))

Tactic:
simp only [mem_span_singleton, Units.isUnit, IsUnit.dvd_mul_right]

Premises used: Units.isUnit, Ideal.mem_span_singleton, IsUnit.dvd_mul_right
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
n : ℕ
u : Rˣ
hr : p ^ n * (↑u : R) ∈ I
hr0 : ¬p ^ n * (↑u : R) = 0
neg : Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex ≤ n
⊢ p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex ∣ p ^ n

Tactic:
apply pow_dvd_pow

Premises used: pow_dvd_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
n : ℕ
u : Rˣ
hr : p ^ n * (↑u : R) ∈ I
hr0 : ¬p ^ n * (↑u : R) = 0
neg : p ^ n ∈ I
⊢ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex ≤ n

Tactic:
apply Nat.find_min'

Premises used: Nat.find_min'
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
n : ℕ
u : Rˣ
hr : p ^ n * (↑u : R) ∈ I
hr0 : ¬p ^ n * (↑u : R) = 0
⊢ p ^ n ∈ I

Tactic:
simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hr

Premises used: Units.mul_inv_cancel_right, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 : p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex ∈ I
⊢ span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex} ≤ I

Tactic:
rw [span_singleton_le_iff_mem]

Premises used: Ideal.span_singleton_le_iff_mem
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
⊢ p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex ∈ I

Tactic:
Nat.find_spec ex

Premises used: Nat.find_spec
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
⊢ p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n ∈ I) ex ∈ I

Tactic:
exact Nat.find_spec ex

Premises used: Nat.find_spec
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
rw : IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
⊢ IsDiscreteValuationRing R

Tactic:
rw [iff_pid_with_one_nonzero_prime]

Premises used: IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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

Tactic:
haveI PID : IsPrincipalIdealRing R := aux_pid_of_ufd_of_unique_irreducible R h₁ h₂
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
obtain : ∀ (p : R) (hp : Irreducible p), IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime

Tactic:
obtain ⟨p, hp⟩ := h₁
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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

Tactic:
⟨PID, ⟨Ideal.span {p}, ⟨?_, ?_⟩, ?_⟩⟩

Premises used: And.intro, Exists.intro, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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})
refine_3 : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}
⊢ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime

Tactic:
refine ⟨PID, ⟨Ideal.span {p}, ⟨?_, ?_⟩, ?_⟩⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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 : ∃ (x : R), Membership.mem (γ := Submodule R R) (span {p}) x ∧ x ≠ 0
⊢ Ne (α := Ideal R) (span {p}) ⊥

Tactic:
rw [Submodule.ne_bot_iff]

Premises used: Submodule.ne_bot_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
⊢ ∃ (x : R), Membership.mem (γ := Submodule R R) (span {p}) x ∧ x ≠ 0

Tactic:
⟨p, Ideal.mem_span_singleton.mpr (dvd_refl p), hp.ne_zero⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Irreducible.ne_zero, Ideal.mem_span_singleton, dvd_refl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
⊢ ∃ (x : R), Membership.mem (γ := Submodule R R) (span {p}) x ∧ x ≠ 0

Tactic:
exact ⟨p, Ideal.mem_span_singleton.mpr (dvd_refl p), hp.ne_zero⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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_2 : Prime p
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : Irreducible p
⊢ IsPrime (α := R) (span {p})

Tactic:
rwa [Ideal.span_singleton_prime hp.ne_zero, ← UniqueFactorizationMonoid.irreducible_iff_prime]

Premises used: UniqueFactorizationMonoid.irreducible_iff_prime, Irreducible.ne_zero, Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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
refine_3 :
  (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) (R ∙ Submodule.IsPrincipal.generator I) →
    Eq (α := Ideal R) (R ∙ Submodule.IsPrincipal.generator I) (span {p})
⊢ (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) I → I = span {p}

Tactic:
rw [← Submodule.IsPrincipal.span_singleton_generator I]

Premises used: Submodule.IsPrincipal.span_singleton_generator
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
refine_3 : Associated (Submodule.IsPrincipal.generator I) p
⊢ Eq (α := Ideal R) (R ∙ Submodule.IsPrincipal.generator I) (span {p})

Tactic:
apply span_singleton_eq_span_singleton.mpr

Premises used: Iff.mpr, Ideal.span_singleton_eq_span_singleton
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
apply : Irreducible (Submodule.IsPrincipal.generator I)
⊢ Associated (Submodule.IsPrincipal.generator I) p

Tactic:
apply h₂ _ hp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
⊢ ¬Submodule.IsPrincipal.generator I = 0

Tactic:
rw [Ne, Submodule.span_singleton_eq_bot] at I0

Premises used: Submodule.span_singleton_eq_bot, Ne
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
I0₁ : ¬Submodule.IsPrincipal.generator I = 0
⊢ IsPrime (R ∙ Submodule.IsPrincipal.generator I)

Tactic:
rw [Ne, Submodule.span_singleton_eq_bot] at I0

Premises used: Submodule.span_singleton_eq_bot, Ne
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
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)
rwa₁ rwa₂ rwa₃ rwa₄ : IsPrime (α := R) (span {Submodule.IsPrincipal.generator I})
⊢ Irreducible (Submodule.IsPrincipal.generator I)

Tactic:
rwa [UniqueFactorizationMonoid.irreducible_iff_prime, ← Ideal.span_singleton_prime I0]

Premises used: UniqueFactorizationMonoid.irreducible_iff_prime, Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := ⋯
apply : ∃ (p : R), Irreducible p
⊢ IsDiscreteValuationRing R

Tactic:
apply of_ufd_of_unique_irreducible _ hR.unique_irreducible

Premises used: IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.unique_irreducible, IsDiscreteValuationRing.of_ufd_of_unique_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := ⋯
obtain :
  ∀ (p : R) (hp : Irreducible p) (H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x), ∃ (p : R), Irreducible p
⊢ ∃ (p : R), Irreducible p

Tactic:
obtain ⟨p, hp, H⟩ := hR
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R
hp : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
this : UniqueFactorizationMonoid R := ⋯
⊢ ∃ (p : R), Irreducible p

Tactic:
⟨p, hp⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R
hp : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ (n : ℕ), Associated (p ^ n) x
this : UniqueFactorizationMonoid R := ⋯
⊢ ∃ (p : R), Irreducible p

Tactic:
exact ⟨p, hp⟩
-- 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
obtain : ∀ (a : ↥(maximalIdeal A)) (ha : a ≠ 0), Ne (α := Ideal B) (maximalIdeal B) ⊥
⊢ 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)

Premises used: Iff.mpr, Submodule.nonzero_mem_of_bot_lt, bot_lt_iff_ne_bot, IsDiscreteValuationRing.not_a_field
-- 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 : ∃ (x : B), Membership.mem (γ := Submodule B B) (maximalIdeal B) x ∧ x ≠ 0
⊢ Ne (α := Ideal B) (maximalIdeal B) ⊥

Tactic:
rw [Submodule.ne_bot_iff]

Premises used: Submodule.ne_bot_iff