-- 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 : IsPrime (Submodule.span R {q})
hq : q ≠ 0
⊢ Submodule.span R {q} = maximalIdeal R

Tactic:
erw [span_singleton_prime hq] at hQ2

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 : Prime q
hq : q ≠ 0
⊢ Submodule.span R {q} = maximalIdeal R

Proof state:
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

Tactic:
assumption

Result:
no goals

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

Tactic:
apply hQ1

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

Proof state:
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})
⊢ q ≠ 0

Tactic:
rintro rfl

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

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 ≤ maximalIdeal R
⊢ maximalIdeal R ≠ ⊥

Tactic:
intro h

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
hPM : P ≤ maximalIdeal R
h : maximalIdeal R = ⊥
⊢ False

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

Tactic:
constructor

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

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime) → IsDiscreteValuationRing R

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

Tactic:
intro RDVR

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

Proof state:
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)

Tactic:
exact ⟨Rlocal, inferInstance⟩

Result:
no goals

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

Tactic:
rintro ⟨RPID, Punique⟩

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

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} ≠ ⊥
hq : q ≠ 0
hQ2 : maximalIdeal R = span {q}
⊢ Submodule.span R {q} = maximalIdeal R

Tactic:
exact hQ2.symm

Result:
no goals

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} ≠ ⊥
hq : q ≠ 0
hQ2 : Irreducible q
⊢ Submodule.span R {q} = maximalIdeal R

Tactic:
rw [irreducible_iff_uniformizer] at hQ2

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 : maximalIdeal R = span {q}
⊢ Submodule.span R {q} = maximalIdeal R

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

Tactic:
simp

Result:
no goals

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 ≤ maximalIdeal R
h : maximalIdeal R = ⊥
⊢ False

Tactic:
rw [h, le_bot_iff] at hPM

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
hPM : P = ⊥
h : maximalIdeal R = ⊥
⊢ False

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

Tactic:
haveI : IsLocalRing R := IsLocalRing.of_unique_nonzero_prime Punique

Result:
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

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
⊢ maximalIdeal R ≠ ⊥

Tactic:
have hPM : P ≤ maximalIdeal R := le_maximalIdeal hP2.1

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
hPM : P ≤ maximalIdeal R
⊢ maximalIdeal R ≠ ⊥