-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem iff_pid_with_one_nonzero_prime (R : Type u) [CommRing R] [IsDomain R] :
    IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ IsPrime P

Proof state:
case h.right.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : Prime q
hq : q ≠ 0
⊢ Submodule.span R {q} = maximalIdeal R

Tactic:
replace hQ2 := hQ2.irreducible

Result:
case h.right.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hq : q ≠ 0
hQ2 : Irreducible q
⊢ Submodule.span R {q} = maximalIdeal R

Proof state:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P => P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R) ∧ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Tactic:
constructor

Result:
case h.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P => P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R)

case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Proof state:
case mpr.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ P.IsPrime
this : IsLocalRing R
⊢ maximalIdeal R ≠ ⊥

Tactic:
rcases Punique with ⟨P, ⟨hP1, hP2⟩, _⟩

Result:
case mpr.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : IsLocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = P
hP1 : P ≠ ⊥
hP2 : P.IsPrime
⊢ maximalIdeal R ≠ ⊥

Proof state:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
rcases id RDVR with ⟨Rlocal⟩

Result:
case mp.mk
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Proof state:
case h.right.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
Q : Ideal R
hQ1 : Q ≠ ⊥
hQ2 : Q.IsPrime
⊢ Q = maximalIdeal R

Tactic:
obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1

Result:
case h.right.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {q})
⊢ Submodule.span R {q} = maximalIdeal R

Proof state:
case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Tactic:
rintro Q ⟨hQ1, hQ2⟩

Result:
case h.right.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
Q : Ideal R
hQ1 : Q ≠ ⊥
hQ2 : Q.IsPrime
⊢ Q = maximalIdeal R

Proof state:
case mp.mk
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
constructor

Result:
case mp.mk.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R

case mp.mk.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Proof state:
case h.right.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {q})
⊢ Submodule.span R {q} = maximalIdeal R

Tactic:
have hq : q ≠ 0 := by
  rintro rfl
  apply hQ1
  simp

Result:
case h.right.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {q})
hq : q ≠ 0
⊢ Submodule.span R {q} = maximalIdeal R

Proof state:
case mp.mk.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
use IsLocalRing.maximalIdeal R

Result:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P => P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R) ∧ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Proof state:
case mpr.intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : IsLocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = P
hP1 : P ≠ ⊥
hP2 : P.IsPrime
hPM : P = ⊥
h : maximalIdeal R = ⊥
⊢ False

Tactic:
exact hP1 hPM

Result:
no goals

Proof state:
case mpr.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ P.IsPrime
this : IsLocalRing R
⊢ IsDiscreteValuationRing R

Tactic:
refine { not_a_field' := ?_ }

Result:
case mpr.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ P.IsPrime
this : IsLocalRing R
⊢ maximalIdeal R ≠ ⊥