case mp
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ DiscreteValuationRing R → IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P

case mpr
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P) → DiscreteValuationRing R
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ DiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
constructor
case mp
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
case mp
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ DiscreteValuationRing R → IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
intro RDVR
case mp.mk
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
case mp
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
rcases id RDVR with ⟨Rlocal⟩
case mp.mk.left
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R

case mp.mk.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∃! P, P ≠ ⊥ ∧ IsPrime P
case mp.mk
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
constructor
case mp.mk.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∃! P, P ≠ ⊥ ∧ IsPrime P
case mp.mk.left
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R

case mp.mk.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∃! P, P ≠ ⊥ ∧ IsPrime P
assumption
case mp.mk.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P => P ≠ ⊥ ∧ IsPrime P) (maximalIdeal R) ∧ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = maximalIdeal R
case mp.mk.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∃! P, P ≠ ⊥ ∧ IsPrime P
use LocalRing.maximalIdeal R
case mp.mk.right.left
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P => P ≠ ⊥ ∧ IsPrime P) (maximalIdeal R)

case mp.mk.right.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = maximalIdeal R
case mp.mk.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P => P ≠ ⊥ ∧ IsPrime P) (maximalIdeal R) ∧ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = maximalIdeal R
constructor
case mp.mk.right.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = maximalIdeal R
case mp.mk.right.left
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P => P ≠ ⊥ ∧ IsPrime P) (maximalIdeal R)

case mp.mk.right.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = maximalIdeal R
exact ⟨Rlocal, inferInstance⟩
case mp.mk.right.right.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
Q : Ideal R
hQ1 : Q ≠ ⊥
hQ2 : IsPrime Q
⊢ Q = maximalIdeal R
case mp.mk.right.right
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = maximalIdeal R
rintro Q ⟨hQ1, hQ2⟩
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {q})
⊢ Submodule.span R {q} = maximalIdeal R
case mp.mk.right.right.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
Q : Ideal R
hQ1 : Q ≠ ⊥
hQ2 : IsPrime Q
⊢ Q = maximalIdeal R
obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing 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
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {q})
⊢ Submodule.span R {q} = maximalIdeal R
have hq : q ≠ 0 := by
  rintro rfl
  apply hQ1
  simp
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : Prime q
hq : q ≠ 0
⊢ Submodule.span R {q} = maximalIdeal R
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing 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
erw [span_singleton_prime hq] at hQ2
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hq : q ≠ 0
hQ2 : Irreducible q
⊢ Submodule.span R {q} = maximalIdeal R
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : Prime q
hq : q ≠ 0
⊢ Submodule.span R {q} = maximalIdeal R
replace hQ2 := hQ2.irreducible
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hq : q ≠ 0
hQ2✝ : Irreducible q
hQ2 : maximalIdeal R = span {q}
⊢ Submodule.span R {q} = maximalIdeal R
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hq : q ≠ 0
hQ2 : Irreducible q
⊢ Submodule.span R {q} = maximalIdeal R
rw [irreducible_iff_uniformizer] at hQ2
no goals
case mp.mk.right.right.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hq : q ≠ 0
hQ2✝ : Irreducible q
hQ2 : maximalIdeal R = span {q}
⊢ Submodule.span R {q} = maximalIdeal R
exact hQ2.symm
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
hQ1 : Submodule.span R {0} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {0})
⊢ False
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : Submodule.span R {q} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {q})
⊢ q ≠ 0
rintro rfl
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
hQ1 : Submodule.span R {0} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {0})
⊢ Submodule.span R {0} = ⊥
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
hQ1 : Submodule.span R {0} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {0})
⊢ False
apply hQ1
no goals
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : DiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toLocalRing✝ : LocalRing R
Rlocal : maximalIdeal R ≠ ⊥
hQ1 : Submodule.span R {0} ≠ ⊥
hQ2 : IsPrime (Submodule.span R {0})
⊢ Submodule.span R {0} = ⊥
simp
case mpr.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ IsPrime P
⊢ DiscreteValuationRing R
case mpr
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P) → DiscreteValuationRing R
rintro ⟨RPID, Punique⟩
case mpr.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ IsPrime P
this : LocalRing R
⊢ DiscreteValuationRing R
case mpr.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ IsPrime P
⊢ DiscreteValuationRing R
haveI : LocalRing R := LocalRing.of_unique_nonzero_prime Punique
case mpr.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ IsPrime P
this : LocalRing R
⊢ maximalIdeal R ≠ ⊥
case mpr.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ IsPrime P
this : LocalRing R
⊢ DiscreteValuationRing R
refine' { not_a_field' := _ }
case mpr.intro.intro.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : LocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = P
hP1 : P ≠ ⊥
hP2 : IsPrime P
⊢ maximalIdeal R ≠ ⊥
case mpr.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
Punique : ∃! P, P ≠ ⊥ ∧ IsPrime P
this : LocalRing R
⊢ maximalIdeal R ≠ ⊥
rcases Punique with ⟨P, ⟨hP1, hP2⟩, _⟩
case mpr.intro.intro.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : LocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = P
hP1 : P ≠ ⊥
hP2 : IsPrime P
hPM : P ≤ maximalIdeal R
⊢ maximalIdeal R ≠ ⊥
case mpr.intro.intro.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : LocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = P
hP1 : P ≠ ⊥
hP2 : IsPrime P
⊢ maximalIdeal R ≠ ⊥
have hPM : P ≤ maximalIdeal R := le_maximalIdeal hP2.1
case mpr.intro.intro.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : LocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = P
hP1 : P ≠ ⊥
hP2 : IsPrime P
hPM : P ≤ maximalIdeal R
h : maximalIdeal R = ⊥
⊢ False
case mpr.intro.intro.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : LocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = P
hP1 : P ≠ ⊥
hP2 : IsPrime P
hPM : P ≤ maximalIdeal R
⊢ maximalIdeal R ≠ ⊥
intro h
case mpr.intro.intro.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : LocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = P
hP1 : P ≠ ⊥
hP2 : IsPrime P
hPM : P = ⊥
h : maximalIdeal R = ⊥
⊢ False
case mpr.intro.intro.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : LocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = P
hP1 : P ≠ ⊥
hP2 : IsPrime P
hPM : P ≤ maximalIdeal R
h : maximalIdeal R = ⊥
⊢ False
rw [h, le_bot_iff] at hPM
no goals
case mpr.intro.intro.intro.intro
R✝ : Type u
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
inst✝² : DiscreteValuationRing R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : LocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = P
hP1 : P ≠ ⊥
hP2 : IsPrime P
hPM : P = ⊥
h : maximalIdeal R = ⊥
⊢ False
exact hP1 hPM