From 2268b60d99420df654be37e732795625489a2dce Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Thu, 31 Oct 2024 13:16:31 -0400
Subject: [PATCH] cleanup and factor out instances

---
 Mathlib/RingTheory/Valuation/Archimedean.lean | 147 +++++++-----------
 Mathlib/RingTheory/Valuation/Basic.lean       |  27 ++++
 2 files changed, 87 insertions(+), 87 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/Archimedean.lean b/Mathlib/RingTheory/Valuation/Archimedean.lean
index af2aae871d30e..c7823a73df8e7 100644
--- a/Mathlib/RingTheory/Valuation/Archimedean.lean
+++ b/Mathlib/RingTheory/Valuation/Archimedean.lean
@@ -8,52 +8,71 @@ import Mathlib.Algebra.Order.Monoid.Submonoid
 import Mathlib.Algebra.Order.SuccPred.TypeTags
 import Mathlib.Data.Int.SuccPred
 import Mathlib.GroupTheory.ArchimedeanDensely
+import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.UniqueFactorizationDomain
 import Mathlib.RingTheory.Valuation.Integers
+import Mathlib.RingTheory.Valuation.ValuationRing
 
 /-!
 # Ring of integers under a given valuation in an multiplicatively archimedean codomain
 
 -/
 
-namespace Valuation.Integers
-
 section Field
 
 variable {F Γ₀ O : Type*} [Field F] [LinearOrderedCommGroupWithZero Γ₀]
   [CommRing O] [Algebra O F] {v : Valuation F Γ₀}
 
+instance : LinearOrderedCommGroupWithZero (MonoidHom.mrange v) where
+  __ : CommGroupWithZero (MonoidHom.mrange v) := inferInstance
+  __ : LinearOrder (MonoidHom.mrange v) := inferInstance
+  zero_le_one := Subtype.coe_le_coe.mp zero_le_one
+  mul_le_mul_left := by
+    simp only [Subtype.forall, MonoidHom.mem_mrange, forall_exists_index, Submonoid.mk_mul_mk,
+      Subtype.mk_le_mk, forall_apply_eq_imp_iff]
+    intro a b hab c
+    exact mul_le_mul_left' hab (v c)
+
+namespace Valuation.Integers
+
+lemma wfDvdMonoid_iff_wellFounded_gt_on_v (hv : Integers v O) :
+    WfDvdMonoid O ↔ WellFounded ((· > ·) on (v ∘ algebraMap O F)) := by
+  refine ⟨fun _ ↦ wellFounded_dvdNotUnit.mono ?_, fun h ↦ ⟨h.mono ?_⟩⟩ <;>
+  simp [Function.onFun, hv.dvdNotUnit_iff_lt]
+
+lemma wellFounded_gt_on_v_iff_discrete_mrange [Nontrivial (MonoidHom.mrange v)ˣ]
+    (hv : Integers v O) :
+    WellFounded ((· > ·) on (v ∘ algebraMap O F)) ↔
+      Nonempty (MonoidHom.mrange v ≃*o WithZero (Multiplicative ℤ)) := by
+  rw [← LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero
+    one_ne_zero, ← Set.wellFoundedOn_range]
+  classical
+  refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
+  · rintro ⟨_, x, rfl⟩
+    simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_setOf_eq, Set.mem_range,
+      Function.comp_apply]
+    intro hx
+    obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx
+    exact ⟨y, by simp⟩
+  · exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1
+  · intro
+    simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_setOf_eq,
+      forall_exists_index]
+    rintro x rfl
+    simp [← Subtype.coe_le_coe, hv.map_le_one]
+  · simp [Function.onFun]
+
 lemma isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean Γ₀] (hv : Integers v O) :
     IsPrincipalIdealRing O ↔ ¬ DenselyOrdered (Set.range v) := by
   refine ⟨fun _ ↦ not_denselyOrdered_of_isPrincipalIdealRing hv, fun H ↦ ?_⟩
-  let l : LinearOrderedCommGroupWithZero (MonoidHom.mrange v) :=
-  { zero := ⟨0, by simp⟩
-    zero_mul := by
-      intro a
-      exact Subtype.ext (zero_mul a.val)
-    mul_zero := by
-      intro a
-      exact Subtype.ext (mul_zero a.val)
-    zero_le_one := Subtype.coe_le_coe.mp (zero_le_one)
-    inv := fun x ↦ ⟨x⁻¹, by
-      obtain ⟨y, hy⟩ := x.prop
-      simp_rw [← hy, ← v.map_inv]
-      exact MonoidHom.mem_mrange.mpr ⟨_, rfl⟩⟩
-    exists_pair_ne := ⟨⟨v 0, by simp⟩, ⟨v 1, by simp [- _root_.map_one]⟩, by simp⟩
-    inv_zero := Subtype.ext inv_zero
-    mul_inv_cancel := by
-      rintro ⟨a, ha⟩ h
-      simp only [ne_eq, Subtype.ext_iff] at h
-      simpa using mul_inv_cancel₀ h }
-  have h0 : (0 : MonoidHom.mrange v) = ⟨0, by simp⟩ := rfl
   rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs|_
-  · have : ∀ x : (MonoidHom.mrange v)ˣ, x.val = 1 := by
-      intro x
-      rw [← Units.val_one, Units.eq_iff]
-      exact Subsingleton.elim _ _
+  · have h0 : (0 : MonoidHom.mrange v) = ⟨0, by simp⟩ := rfl
+    have (x : (MonoidHom.mrange v)ˣ) : x.val = 1 := by
+        rw [← Units.val_one, Units.eq_iff, Subsingleton.elim x 1]
     replace this : ∀ x ≠ 0, v x = 1 := by
       intros x hx
       specialize this (Units.mk0 ⟨v x, by simp⟩ _)
-      · simp [ne_eq, Subtype.ext_iff, h0, hx]
+      · simp [ne_eq, Subtype.ext_iff, hx, h0]
       simpa [Subtype.ext_iff] using this
     suffices ∀ I : Ideal O, I = ⊥ ∨ I = ⊤ by
       constructor
@@ -61,65 +80,19 @@ lemma isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean Γ₀] (hv : I
       rcases this I with rfl|rfl
       · exact ⟨0, Ideal.span_zero.symm⟩
       · exact ⟨1, Ideal.span_one.symm⟩
-    intro I
-    rcases eq_or_ne I ⊤ with rfl|hI
-    · simp
-    simp only [hI, or_false]
-    ext x
-    rcases eq_or_ne x 0 with rfl|hx
-    · simp
-    · specialize this (algebraMap O F x) (by simp [map_eq_zero_iff _ hv.hom_inj, hx])
-      simp only [Ideal.mem_bot, hx, iff_false]
-      contrapose! hI
-      exact Ideal.eq_top_of_isUnit_mem _ hI (isUnit_of_one' hv this)
-  replace H : ¬ DenselyOrdered (MonoidHom.mrange v) := H
-  rw [← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered (MonoidHom.mrange v)] at H
-  obtain ⟨e⟩ := H
-  constructor
-  intro S
-  rw [isPrincipal_iff_exists_isGreatest hv]
-  rcases eq_or_ne S ⊥ with rfl|hS
-  · simp only [Function.comp_apply, Submodule.bot_coe, Set.image_singleton, _root_.map_zero]
-    exact ⟨0, by simp⟩
-  let e' : (MonoidHom.mrange v)ˣ ≃o Multiplicative ℤ := ⟨
-    (MulEquiv.unzero (WithZero.withZeroUnitsEquiv.trans e)).toEquiv, by
-    intros
-    simp only [MulEquiv.unzero, WithZero.withZeroUnitsEquiv,
-      MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_mk, WithZero.recZeroCoe_coe,
-      OrderMonoidIso.coe_mulEquiv, MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Units.val_mk0,
-      Equiv.coe_fn_symm_mk, map_eq_zero, WithZero.coe_ne_zero, ↓reduceDIte, WithZero.unzero_coe,
-      MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, ← Units.val_le_val]
-    rw [← map_le_map_iff e, ← WithZero.coe_le_coe, WithZero.coe_unzero, WithZero.coe_unzero]⟩
-  let _ : SuccOrder (MonoidHom.mrange v)ˣ := .ofOrderIso e'.symm
-  have : IsSuccArchimedean (MonoidHom.mrange v)ˣ := .of_orderIso e'.symm
-  set T : Set (MonoidHom.mrange v)ˣ := {y | ∃ (x : O) (h : x ≠ 0), x ∈ S ∧
-      y = Units.mk0 ⟨v (algebraMap O F x), by simp⟩
-      (by simp [map_ne_zero_iff, Subtype.ext_iff, h0, map_eq_zero_iff _ hv.hom_inj, h])} with hT
-  have : BddAbove (α := (MonoidHom.mrange v)ˣ) T := by
-    refine ⟨1, ?_⟩
-    simp only [ne_eq, exists_and_left, mem_upperBounds, Set.mem_setOf_eq, forall_exists_index,
-      and_imp, hT]
-    rintro _ x _ hx' rfl
-    simp [← Units.val_le_val, ← Subtype.coe_le_coe, hv.map_le_one]
-  have hTn : T.Nonempty := by
-    rw [Submodule.ne_bot_iff] at hS
-    obtain ⟨x, hx, hx'⟩ := hS
-    refine ⟨Units.mk0 ⟨v (algebraMap O F x), by simp⟩ ?_, ?_⟩
-    · simp [map_ne_zero_iff, Subtype.ext_iff, h0, map_eq_zero_iff _ hv.hom_inj, hx']
-    · simp only [hT, ne_eq, exists_and_left, Set.mem_setOf_eq, Units.mk0_inj, Subtype.mk.injEq,
-      exists_prop', nonempty_prop]
-      exact ⟨_, hx, hx', rfl⟩
-  obtain ⟨_, ⟨x, hx, hxS, rfl⟩, hx'⟩ := this.exists_isGreatest_of_nonempty hTn
-  refine ⟨_, ⟨x, hxS, rfl⟩, ?_⟩
-  simp only [hT, ne_eq, exists_and_left, mem_upperBounds, Set.mem_setOf_eq, ← Units.val_le_val,
-    Units.val_mk0, ← Subtype.coe_le_coe, forall_exists_index, and_imp, Function.comp_apply,
-    Set.mem_image, SetLike.mem_coe, forall_apply_eq_imp_iff₂] at hx' ⊢
-  intro y hy
-  rcases eq_or_ne y 0 with rfl|hy'
-  · simp
-  specialize hx' _ y hy hy' rfl
-  simpa [← Units.val_le_val, ← Subtype.coe_le_coe] using hx'
-
-end Field
+    simp_rw [or_iff_not_imp_right, Submodule.eq_bot_iff]
+    intro I hI x hx
+    contrapose! hI with h0
+    specialize this (algebraMap O F x) (by simp [map_eq_zero_iff _ hv.hom_inj, h0])
+    exact Ideal.eq_top_of_isUnit_mem _ hx (isUnit_of_one' hv this)
+  have : IsDomain O := hv.hom_inj.isDomain
+  have : ValuationRing O := ValuationRing.of_integers v hv
+  have : IsBezout O := ValuationRing.instIsBezout
+  have := ((IsBezout.TFAE (R := O)).out 1 3)
+  rw [this, hv.wfDvdMonoid_iff_wellFounded_gt_on_v, hv.wellFounded_gt_on_v_iff_discrete_mrange,
+    LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]
+  exact H
 
 end Valuation.Integers
+
+end Field
diff --git a/Mathlib/RingTheory/Valuation/Basic.lean b/Mathlib/RingTheory/Valuation/Basic.lean
index 54e29458ccc66..65d64b1681329 100644
--- a/Mathlib/RingTheory/Valuation/Basic.lean
+++ b/Mathlib/RingTheory/Valuation/Basic.lean
@@ -849,3 +849,30 @@ end Supp
 
 -- end of section
 end AddValuation
+
+namespace Valuation
+
+variable {K Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+
+instance [Ring K] (v : Valuation K Γ₀) : CommMonoidWithZero (MonoidHom.mrange v) where
+  zero := ⟨0, 0, by simp⟩
+  zero_mul := by
+    intro a
+    exact Subtype.ext (zero_mul a.val)
+  mul_zero := by
+    intro a
+    exact Subtype.ext (mul_zero a.val)
+
+instance [DivisionRing K] (v : Valuation K Γ₀) : CommGroupWithZero (MonoidHom.mrange v) where
+  inv := fun x ↦ ⟨x⁻¹, by
+    obtain ⟨y, hy⟩ := x.prop
+    simp_rw [← hy, ← v.map_inv]
+    exact MonoidHom.mem_mrange.mpr ⟨_, rfl⟩⟩
+  exists_pair_ne := ⟨⟨v 0, by simp⟩, ⟨v 1, by simp [- _root_.map_one]⟩, by simp⟩
+  inv_zero := Subtype.ext inv_zero
+  mul_inv_cancel := by
+    rintro ⟨a, ha⟩ h
+    simp only [ne_eq, Subtype.ext_iff] at h
+    simpa using mul_inv_cancel₀ h
+
+end Valuation