-- 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 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}
h₅ 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
⊢ IsPrincipalIdealRing R

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

Premises used: IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible, pow_dvd_pow, Units.mul_inv_cancel_right, Ideal.span_singleton_le_iff_mem, le_antisymm, Nat.find_min', Submodule.zero_mem, Ideal.span, Units.isUnit, Ideal.mem_span_singleton, IsUnit.dvd_mul_right, OfNat.ofNat, Submodule.span_zero, rfl, Set.singleton_zero