-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem ideal_eq_span_pow_irreducible {s : Ideal R} (hs : s ≠ ⊥) {ϖ : R} (hirr : Irreducible ϖ) :
    ∃ n : ℕ, s = Ideal.span {ϖ ^ n}

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
⊢ ∃ n, s = span {ϖ ^ n}

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

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
⊢ ∃ n, s = span {ϖ ^ n}

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
⊢ s = span {ϖ ^ n}

Tactic:
have : span _ = _ := Ideal.span_singleton_generator s

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
this : span {generator s} = s
⊢ s = span {ϖ ^ n}

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
this : span {generator s} = s
⊢ s = span {ϖ ^ n}

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

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
this : span {generator s} = s
⊢ Associated (generator s) (generator s * ↑u)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ ∃ n, s = span {ϖ ^ n}

Tactic:
have gen_ne_zero : generator s ≠ 0 := by
  rw [Ne, ← eq_bot_iff_generator_eq_zero]
  assumption

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
⊢ ∃ n, s = span {ϖ ^ n}

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
this : span {generator s} = s
⊢ Associated (generator s) (generator s * ↑u)

Tactic:
use u

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ generator s ≠ 0

Tactic:
rw [Ne, ← eq_bot_iff_generator_eq_zero]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ ¬s = ⊥

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
⊢ ∃ n, s = span {ϖ ^ n}

Tactic:
use n

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
⊢ s = span {ϖ ^ n}

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ ¬s = ⊥

Tactic:
assumption

Result:
no goals