-- Mathlib/RingTheory/Valuation/Archimedean.lean
lemma isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean Γ₀] (hv : Integers v O) :
    IsPrincipalIdealRing O ↔ ¬ DenselyOrdered (Set.range v)

Proof state:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝ : IsDomain O
this : ValuationRing O
⊢ IsPrincipalIdealRing O

Tactic:
have : IsBezout O := ValuationRing.instIsBezout

Result:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsBezout O
⊢ IsPrincipalIdealRing O

Proof state:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝² : IsDomain O
this✝¹ : ValuationRing O
this✝ : IsBezout O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ IsPrincipalIdealRing O

Tactic:
rw [this, hv.wfDvdMonoid_iff_wellFounded_gt_on_v, hv.wellFounded_gt_on_v_iff_discrete_mrange,
  LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]

Result:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝² : IsDomain O
this✝¹ : ValuationRing O
this✝ : IsBezout O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ ¬DenselyOrdered ↥(MonoidHom.mrange v)

Proof state:
case inl
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
hs : Subsingleton (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing O

Tactic:
have := bijective_algebraMap_of_subsingleton_units_mrange hv

Result:
case inl
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
hs : Subsingleton (↥(MonoidHom.mrange v))ˣ
this : Function.Bijective ⇑(algebraMap O F)
⊢ IsPrincipalIdealRing O

Proof state:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsBezout O
⊢ IsPrincipalIdealRing O

Tactic:
have := ((IsBezout.TFAE (R := O)).out 1 3)

Result:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝² : IsDomain O
this✝¹ : ValuationRing O
this✝ : IsBezout O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ IsPrincipalIdealRing O

Proof state:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
⊢ IsPrincipalIdealRing O ↔ ¬DenselyOrdered ↑(Set.range ⇑v)

Tactic:
refine ⟨fun _ ↦ not_denselyOrdered_of_isPrincipalIdealRing hv, fun H ↦ ?_⟩

Result:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
⊢ IsPrincipalIdealRing O

Proof state:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing O

Tactic:
have : IsDomain O := hv.hom_inj.isDomain

Result:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this : IsDomain O
⊢ IsPrincipalIdealRing O

Proof state:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝² : IsDomain O
this✝¹ : ValuationRing O
this✝ : IsBezout O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ ¬DenselyOrdered ↥(MonoidHom.mrange v)

Tactic:
exact H

Result:
no goals

Proof state:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
⊢ IsPrincipalIdealRing O

Tactic:
rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs|_

Result:
case inl
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
hs : Subsingleton (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing O

case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing O

Proof state:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this : IsDomain O
⊢ IsPrincipalIdealRing O

Tactic:
have : ValuationRing O := ValuationRing.of_integers v hv

Result:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝ : IsDomain O
this : ValuationRing O
⊢ IsPrincipalIdealRing O

Proof state:
case inl
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean Γ₀
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
hs : Subsingleton (↥(MonoidHom.mrange v))ˣ
this : Function.Bijective ⇑(algebraMap O F)
⊢ IsPrincipalIdealRing O

Tactic:
exact .of_surjective _ (RingEquiv.ofBijective _ this).symm.surjective

Result:
no goals