From 001e35b9c9094d2ce17ba26965e8fdf8f51fc7dd Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Thu, 9 Jun 2022 14:32:23 -0600
Subject: [PATCH 01/15] defs

---
 src/ring_theory/valuation/basic.lean          | 58 +++++++++++++++++++
 .../valuation/valuation_subring.lean          | 43 ++++++++++++++
 2 files changed, 101 insertions(+)

diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
index 7e55211a18b33..209e725ff8398 100644
--- a/src/ring_theory/valuation/basic.lean
+++ b/src/ring_theory/valuation/basic.lean
@@ -419,6 +419,64 @@ begin
       { rw ← h at hx', exact le_of_eq hx' } } }
 end
 
+lemma is_equiv_iff_val_lt_one
+  [linear_ordered_comm_group_with_zero Γ₀]
+  [linear_ordered_comm_group_with_zero Γ'₀]
+  {K : Type*} [division_ring K]
+  (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
+  v.is_equiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1 :=
+begin
+  split,
+  { intros h x,
+    simp only [lt_iff_le_and_ne, and_congr ((is_equiv_iff_val_le_one _ _).1 h)
+      ((is_equiv_iff_val_eq_one _ _).1 h).not] },
+  { rw is_equiv_iff_val_eq_one,
+    intros h x,
+    by_cases hx : x = 0, { simp only [(zero_iff _).2 hx, zero_ne_one] },
+    split,
+    { intro hh,
+      by_contra h_1,
+      cases ne_iff_lt_or_gt.1 h_1,
+      { simpa [hh, lt_self_iff_false] using h.2 h_2 },
+      { rw [← inv_one, eq_inv_iff_eq_inv, ← map_inv] at hh,
+        exact hh.le.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2)) } },
+    { intro hh,
+      by_contra h_1,
+      cases ne_iff_lt_or_gt.1 h_1,
+      { simpa [hh, lt_self_iff_false] using h.1 h_2 },
+      { rw [← inv_one, eq_inv_iff_eq_inv, ← map_inv] at hh,
+        exact hh.le.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2)) } } }
+end
+
+lemma is_equiv_iff_val_sub_one_lt_one
+  [linear_ordered_comm_group_with_zero Γ₀]
+  [linear_ordered_comm_group_with_zero Γ'₀]
+  {K : Type*} [division_ring K]
+  (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
+  v.is_equiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1 :=
+begin
+  rw is_equiv_iff_val_lt_one,
+  refine ⟨λ h x, @h (x - 1), λ h x, by simpa using @h (x + 1)⟩,
+end
+
+lemma is_equiv_tfae
+  [linear_ordered_comm_group_with_zero Γ₀]
+  [linear_ordered_comm_group_with_zero Γ'₀]
+  {K : Type*} [division_ring K]
+  (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
+  [ v.is_equiv v'
+  , ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1
+  , ∀ {x}, v x = 1 ↔ v' x = 1
+  , ∀ {x}, v x < 1 ↔ v' x < 1
+  , ∀ {x}, v (x-1) < 1 ↔ v' (x-1) < 1].tfae :=
+begin
+  tfae_have : 1 ↔ 2, { apply is_equiv_iff_val_le_one },
+  tfae_have : 1 ↔ 3, { apply is_equiv_iff_val_eq_one },
+  tfae_have : 1 ↔ 4, { apply is_equiv_iff_val_lt_one },
+  tfae_have : 1 ↔ 5, { apply is_equiv_iff_val_sub_one_lt_one },
+  tfae_finish
+end
+
 end
 
 section supp
diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 2ffc52f0df5e5..6b0a93e78c210 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -435,4 +435,47 @@ unit_group_order_embedding.strict_mono
 
 end unit_group
 
+section maximal_ideal
+
+def maximal_ideal : subsemigroup K :=
+{ carrier := { x | A.valuation x < 1 },
+  mul_mem' := λ a b ha hb, by { simpa using mul_lt_mul₀ ha hb } }
+
+lemma mem_maximal_ideal_iff (x : K) : x ∈ A.maximal_ideal ↔ A.valuation x < 1 := iff.refl _
+
+lemma eq_iff_maximal_ideal (A B : valuation_subring K) :
+  A = B ↔ A.maximal_ideal = B.maximal_ideal :=
+begin
+  simp_rw [← A.valuation_subring_valuation, ← B.valuation_subring_valuation,
+    ← valuation.is_equiv_iff_valuation_subring,
+    A.valuation_subring_valuation, B.valuation_subring_valuation,
+    valuation.is_equiv_iff_val_lt_one, set_like.ext_iff, mem_maximal_ideal_iff],
+end
+
+/-- `A.maximal_ideal` agrees with the maximal ideal of `A`. -/
+def maximal_ideal_equiv : A.maximal_ideal ≃ local_ring.maximal_ideal A :=
+{ to_fun := λ a, ⟨⟨a,(A.valuation_le_one_iff _).1 (le_of_lt a.2)⟩,(A.valuation_lt_one_iff _).2 a.2⟩,
+  inv_fun := λ a, ⟨a,(A.valuation_lt_one_iff _).1 a.2⟩,
+  left_inv := λ a, by { ext, refl },
+  right_inv := λ a, by { ext, refl } }
+
+@[simp]
+lemma coe_maximal_ideal_equiv_apply (a : A.maximal_ideal) :
+  (A.maximal_ideal_equiv a : K) = a := rfl
+
+@[simp]
+lemma coe_maximal_ideal_equiv_symm_apply (a : local_ring.maximal_ideal A) :
+  (A.maximal_ideal_equiv.symm a : K) = a := rfl
+
+@[simp]
+lemma maximal_ideal_equiv_map_mul (a b : A.maximal_ideal) :
+  A.maximal_ideal_equiv (a * b) = (A.maximal_ideal_equiv a : A) • A.maximal_ideal_equiv b := rfl
+
+@[simp]
+lemma maximal_ideal_equiv_symm_map_smul (a b : local_ring.maximal_ideal A) :
+  A.maximal_ideal_equiv.symm ((a : A) • b) =
+  A.maximal_ideal_equiv.symm a * A.maximal_ideal_equiv.symm b := rfl
+
+end maximal_ideal
+
 end valuation_subring

From ed690423d128761f9459cc4266ea86202c852da8 Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Thu, 9 Jun 2022 14:44:46 -0600
Subject: [PATCH 02/15] simps

---
 .../valuation/valuation_subring.lean          | 20 ++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 6b0a93e78c210..da13584a4cde3 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -443,15 +443,21 @@ def maximal_ideal : subsemigroup K :=
 
 lemma mem_maximal_ideal_iff (x : K) : x ∈ A.maximal_ideal ↔ A.valuation x < 1 := iff.refl _
 
-lemma eq_iff_maximal_ideal (A B : valuation_subring K) :
-  A = B ↔ A.maximal_ideal = B.maximal_ideal :=
-begin
-  simp_rw [← A.valuation_subring_valuation, ← B.valuation_subring_valuation,
-    ← valuation.is_equiv_iff_valuation_subring,
-    A.valuation_subring_valuation, B.valuation_subring_valuation,
-    valuation.is_equiv_iff_val_lt_one, set_like.ext_iff, mem_maximal_ideal_iff],
+lemma maximal_ideal_injective :
+  function.injective (maximal_ideal : valuation_subring K → subsemigroup _) :=
+λ A B h, begin
+  rw [← A.valuation_subring_valuation, ← B.valuation_subring_valuation,
+    ← valuation.is_equiv_iff_valuation_subring, valuation.is_equiv_iff_val_lt_one],
+  rw set_like.ext_iff at h,
+  intros x,
+  by_cases hx : x = 0, { simp only [hx, valuation.map_zero, zero_lt_one₀] },
+  exact h (units.mk0 x hx)
 end
 
+lemma eq_iff_maximal_ideal {A B : valuation_subring K} :
+  A = B ↔ A.maximal_ideal = B.maximal_ideal :=
+maximal_ideal_injective.eq_iff.symm
+
 /-- `A.maximal_ideal` agrees with the maximal ideal of `A`. -/
 def maximal_ideal_equiv : A.maximal_ideal ≃ local_ring.maximal_ideal A :=
 { to_fun := λ a, ⟨⟨a,(A.valuation_le_one_iff _).1 (le_of_lt a.2)⟩,(A.valuation_lt_one_iff _).2 a.2⟩,

From 4145d1b40f1f4d836893cef398cdf60340ad0ded Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Thu, 9 Jun 2022 15:12:00 -0600
Subject: [PATCH 03/15] lemma

---
 src/ring_theory/valuation/basic.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
index 209e725ff8398..2060d08460dd6 100644
--- a/src/ring_theory/valuation/basic.lean
+++ b/src/ring_theory/valuation/basic.lean
@@ -293,6 +293,13 @@ begin
   simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h
 end
 
+lemma one_lt_val_iff
+  {K : Type*} [division_ring K] (v : valuation K Γ₀) {x : K} (h : x ≠ 0) :
+  1 < v x ↔ v x⁻¹ < 1 :=
+begin
+  simpa using (inv_lt_inv₀ (v.ne_zero_iff.2 h) one_ne_zero).symm,
+end
+
 /-- The subgroup of elements whose valuation is less than a certain unit.-/
 def lt_add_subgroup (v : valuation R Γ₀) (γ : Γ₀ˣ) : add_subgroup R :=
 { carrier   := {x | v x < γ},

From 6ea865282c82b9544a1d6358b6cbea8efd51b7f9 Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Thu, 9 Jun 2022 17:04:23 -0600
Subject: [PATCH 04/15] comment

---
 src/ring_theory/valuation/valuation_subring.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index da13584a4cde3..831adcb414144 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -437,6 +437,7 @@ end unit_group
 
 section maximal_ideal
 
+/-- The unique maximal ideal of a valuation subring, as a subsemigroup of `K`-/
 def maximal_ideal : subsemigroup K :=
 { carrier := { x | A.valuation x < 1 },
   mul_mem' := λ a b ha hb, by { simpa using mul_lt_mul₀ ha hb } }

From 8b220a2848decca82a331f97f8dc1a88fc6e8b5e Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Fri, 10 Jun 2022 13:40:34 -0600
Subject: [PATCH 05/15] update lemma

---
 src/ring_theory/valuation/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
index 2060d08460dd6..dee7b9747c769 100644
--- a/src/ring_theory/valuation/basic.lean
+++ b/src/ring_theory/valuation/basic.lean
@@ -463,7 +463,7 @@ lemma is_equiv_iff_val_sub_one_lt_one
   v.is_equiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1 :=
 begin
   rw is_equiv_iff_val_lt_one,
-  refine ⟨λ h x, @h (x - 1), λ h x, by simpa using @h (x + 1)⟩,
+  exact (equiv.sub_right 1).surjective.forall
 end
 
 lemma is_equiv_tfae

From 9687b52fe4a883f41b8bca6b82eec6be85f51a90 Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Wed, 15 Jun 2022 17:52:19 -0600
Subject: [PATCH 06/15] changed maximal ideal to nonunits

---
 .../valuation/valuation_subring.lean          | 28 +++++++++----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 831adcb414144..1c29f74b62d8f 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -435,17 +435,17 @@ unit_group_order_embedding.strict_mono
 
 end unit_group
 
-section maximal_ideal
+section nonunits
 
-/-- The unique maximal ideal of a valuation subring, as a subsemigroup of `K`-/
-def maximal_ideal : subsemigroup K :=
+/-- The nonunits of a valuation subring, as a subsemigroup of `K`-/
+def nonunits : subsemigroup K :=
 { carrier := { x | A.valuation x < 1 },
   mul_mem' := λ a b ha hb, by { simpa using mul_lt_mul₀ ha hb } }
 
-lemma mem_maximal_ideal_iff (x : K) : x ∈ A.maximal_ideal ↔ A.valuation x < 1 := iff.refl _
+lemma mem_nonunits_iff (x : K) : x ∈ A.nonunits ↔ A.valuation x < 1 := iff.refl _
 
-lemma maximal_ideal_injective :
-  function.injective (maximal_ideal : valuation_subring K → subsemigroup _) :=
+lemma nonunits_injective :
+  function.injective (nonunits : valuation_subring K → subsemigroup _) :=
 λ A B h, begin
   rw [← A.valuation_subring_valuation, ← B.valuation_subring_valuation,
     ← valuation.is_equiv_iff_valuation_subring, valuation.is_equiv_iff_val_lt_one],
@@ -455,19 +455,19 @@ lemma maximal_ideal_injective :
   exact h (units.mk0 x hx)
 end
 
-lemma eq_iff_maximal_ideal {A B : valuation_subring K} :
-  A = B ↔ A.maximal_ideal = B.maximal_ideal :=
-maximal_ideal_injective.eq_iff.symm
+lemma eq_iff_nonunits {A B : valuation_subring K} :
+  A = B ↔ A.nonunits = B.nonunits :=
+nonunits_injective.eq_iff.symm
 
-/-- `A.maximal_ideal` agrees with the maximal ideal of `A`. -/
-def maximal_ideal_equiv : A.maximal_ideal ≃ local_ring.maximal_ideal A :=
+/-- `A.nonunits` agrees with the maximal ideal of `A`. -/
+def maximal_ideal_equiv : A.nonunits ≃ local_ring.maximal_ideal A :=
 { to_fun := λ a, ⟨⟨a,(A.valuation_le_one_iff _).1 (le_of_lt a.2)⟩,(A.valuation_lt_one_iff _).2 a.2⟩,
   inv_fun := λ a, ⟨a,(A.valuation_lt_one_iff _).1 a.2⟩,
   left_inv := λ a, by { ext, refl },
   right_inv := λ a, by { ext, refl } }
 
 @[simp]
-lemma coe_maximal_ideal_equiv_apply (a : A.maximal_ideal) :
+lemma coe_maximal_ideal_equiv_apply (a : A.nonunits) :
   (A.maximal_ideal_equiv a : K) = a := rfl
 
 @[simp]
@@ -475,7 +475,7 @@ lemma coe_maximal_ideal_equiv_symm_apply (a : local_ring.maximal_ideal A) :
   (A.maximal_ideal_equiv.symm a : K) = a := rfl
 
 @[simp]
-lemma maximal_ideal_equiv_map_mul (a b : A.maximal_ideal) :
+lemma maximal_ideal_equiv_map_mul (a b : A.nonunits) :
   A.maximal_ideal_equiv (a * b) = (A.maximal_ideal_equiv a : A) • A.maximal_ideal_equiv b := rfl
 
 @[simp]
@@ -483,6 +483,6 @@ lemma maximal_ideal_equiv_symm_map_smul (a b : local_ring.maximal_ideal A) :
   A.maximal_ideal_equiv.symm ((a : A) • b) =
   A.maximal_ideal_equiv.symm a * A.maximal_ideal_equiv.symm b := rfl
 
-end maximal_ideal
+end nonunits
 
 end valuation_subring

From 222f853449cdbb74da6cb7e923c05fbff2dd00f8 Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Wed, 22 Jun 2022 14:06:41 -0600
Subject: [PATCH 07/15] renamed lemmas

---
 .../valuation/valuation_subring.lean          | 21 ++++++++++---------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 1c29f74b62d8f..590a549fd85a3 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -460,28 +460,29 @@ lemma eq_iff_nonunits {A B : valuation_subring K} :
 nonunits_injective.eq_iff.symm
 
 /-- `A.nonunits` agrees with the maximal ideal of `A`. -/
-def maximal_ideal_equiv : A.nonunits ≃ local_ring.maximal_ideal A :=
+def nonunits_equiv_maximal_ideal : A.nonunits ≃ local_ring.maximal_ideal A :=
 { to_fun := λ a, ⟨⟨a,(A.valuation_le_one_iff _).1 (le_of_lt a.2)⟩,(A.valuation_lt_one_iff _).2 a.2⟩,
   inv_fun := λ a, ⟨a,(A.valuation_lt_one_iff _).1 a.2⟩,
   left_inv := λ a, by { ext, refl },
   right_inv := λ a, by { ext, refl } }
 
 @[simp]
-lemma coe_maximal_ideal_equiv_apply (a : A.nonunits) :
-  (A.maximal_ideal_equiv a : K) = a := rfl
+lemma coe_nonunits_equiv_maximal_ideal_apply (a : A.nonunits) :
+  (A.nonunits_equiv_maximal_ideal a : K) = a := rfl
 
 @[simp]
-lemma coe_maximal_ideal_equiv_symm_apply (a : local_ring.maximal_ideal A) :
-  (A.maximal_ideal_equiv.symm a : K) = a := rfl
+lemma coe_nonunits_equiv_maximal_ideal_symm_apply (a : local_ring.maximal_ideal A) :
+  (A.nonunits_equiv_maximal_ideal.symm a : K) = a := rfl
 
 @[simp]
-lemma maximal_ideal_equiv_map_mul (a b : A.nonunits) :
-  A.maximal_ideal_equiv (a * b) = (A.maximal_ideal_equiv a : A) • A.maximal_ideal_equiv b := rfl
+lemma nonunits_equiv_maximal_ideal_map_mul (a b : A.nonunits) :
+  A.nonunits_equiv_maximal_ideal (a * b) =
+  (A.nonunits_equiv_maximal_ideal a : A) • A.nonunits_equiv_maximal_ideal b := rfl
 
 @[simp]
-lemma maximal_ideal_equiv_symm_map_smul (a b : local_ring.maximal_ideal A) :
-  A.maximal_ideal_equiv.symm ((a : A) • b) =
-  A.maximal_ideal_equiv.symm a * A.maximal_ideal_equiv.symm b := rfl
+lemma nonunits_equiv_maximal_ideal_symm_map_smul (a b : local_ring.maximal_ideal A) :
+  A.nonunits_equiv_maximal_ideal.symm ((a : A) • b) =
+  A.nonunits_equiv_maximal_ideal.symm a * A.nonunits_equiv_maximal_ideal.symm b := rfl
 
 end nonunits
 

From 8971c5223ef965c746e8a32756cadf7368ea2d54 Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Thu, 14 Jul 2022 10:31:48 +0000
Subject: [PATCH 08/15] Formatting

---
 .../valuation/valuation_subring.lean          | 36 +++++++++----------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 590a549fd85a3..2c8f4994b7e57 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -72,9 +72,9 @@ instance : valuation_ring A :=
     by_cases (b : K) = 0, { use 0, left, ext, simp [h] },
     by_cases (a : K) = 0, { use 0, right, ext, simp [h] },
     cases A.mem_or_inv_mem (a/b) with hh hh,
-    { use ⟨a/b,hh⟩, right, ext, field_simp, ring },
+    { use ⟨a/b, hh⟩, right, ext, field_simp, ring },
     { rw (show (a/b : K)⁻¹ = b/a, by field_simp) at hh,
-      use ⟨b/a,hh⟩, left, ext, field_simp, ring },
+      use ⟨b/a, hh⟩, left, ext, field_simp, ring },
   end }
 
 instance : algebra A K :=
@@ -84,16 +84,16 @@ show algebra A.to_subring K, by apply_instance
 lemma algebra_map_apply (a : A) : algebra_map A K a = a := rfl
 
 instance : is_fraction_ring A K :=
-{ map_units := λ ⟨y,hy⟩,
+{ map_units := λ ⟨y, hy⟩,
     (units.mk0 (y : K) (λ c, non_zero_divisors.ne_zero hy $ subtype.ext c)).is_unit,
   surj := λ z, begin
-    by_cases z = 0, { use (0,1), simp [h] },
+    by_cases z = 0, { use (0, 1), simp [h] },
     cases A.mem_or_inv_mem z with hh hh,
-    { use (⟨z,hh⟩,1), simp },
-    { refine ⟨⟨1,⟨⟨_,hh⟩,_⟩⟩, mul_inv_cancel h⟩,
+    { use (⟨z, hh⟩, 1), simp },
+    { refine ⟨⟨1, ⟨⟨_, hh⟩, _⟩⟩, mul_inv_cancel h⟩,
       exact mem_non_zero_divisors_iff_ne_zero.2 (λ c, h (inv_eq_zero.mp (congr_arg coe c))) },
   end,
-  eq_iff_exists := λ a b, ⟨ λ h, ⟨1, by { ext, simpa using h }⟩, λ ⟨c,h⟩,
+  eq_iff_exists := λ a b, ⟨ λ h, ⟨1, by { ext, simpa using h }⟩, λ ⟨c, h⟩,
     congr_arg coe ((mul_eq_mul_right_iff.1 h).resolve_right (non_zero_divisors.ne_zero c.2)) ⟩ }
 
 /-- The value group of the valuation associated to `A`. -/
@@ -106,13 +106,13 @@ def valuation : valuation K A.value_group := valuation_ring.valuation A K
 instance inhabited_value_group : inhabited A.value_group := ⟨A.valuation 0⟩
 
 lemma valuation_le_one (a : A) : A.valuation a ≤ 1 :=
-(valuation_ring.mem_integer_iff A K _).2 ⟨a,rfl⟩
+(valuation_ring.mem_integer_iff A K _).2 ⟨a, rfl⟩
 
 lemma mem_of_valuation_le_one (x : K) (h : A.valuation x ≤ 1) : x ∈ A :=
-let ⟨a,ha⟩ := (valuation_ring.mem_integer_iff A K x).1 h in ha ▸ a.2
+let ⟨a, ha⟩ := (valuation_ring.mem_integer_iff A K x).1 h in ha ▸ a.2
 
 lemma valuation_le_one_iff (x : K) : A.valuation x ≤ 1 ↔ x ∈ A :=
-⟨mem_of_valuation_le_one _ _, λ ha, A.valuation_le_one ⟨x,ha⟩⟩
+⟨mem_of_valuation_le_one _ _, λ ha, A.valuation_le_one ⟨x, ha⟩⟩
 
 lemma valuation_eq_iff (x y : K) : A.valuation x = A.valuation y ↔
   ∃ a : Aˣ, (a : K) * y = x := quotient.eq'
@@ -179,7 +179,7 @@ subring.subtype R.to_subring
 /-- The canonical map on value groups induced by a coarsening of valuation rings. -/
 def map_of_le (R S : valuation_subring K) (h : R ≤ S) :
   R.value_group →*₀ S.value_group :=
-{ to_fun := quotient.map' id $ λ x y ⟨u,hu⟩, ⟨units.map (R.inclusion S h).to_monoid_hom u, hu⟩,
+{ to_fun := quotient.map' id $ λ x y ⟨u, hu⟩, ⟨units.map (R.inclusion S h).to_monoid_hom u, hu⟩,
   map_zero' := rfl,
   map_one' := rfl,
   map_mul' := by { rintro ⟨⟩ ⟨⟩, refl } }
@@ -187,7 +187,7 @@ def map_of_le (R S : valuation_subring K) (h : R ≤ S) :
 @[mono]
 lemma monotone_map_of_le (R S : valuation_subring K) (h : R ≤ S) :
   monotone (R.map_of_le S h) :=
-by { rintros ⟨⟩ ⟨⟩ ⟨a,ha⟩, exact ⟨R.inclusion S h a, ha⟩ }
+by { rintros ⟨⟩ ⟨⟩ ⟨a, ha⟩, exact ⟨R.inclusion S h a, ha⟩ }
 
 @[simp]
 lemma map_of_le_comp_valuation (R S : valuation_subring K) (h : R ≤ S) :
@@ -209,7 +209,7 @@ def of_prime (A : valuation_subring K) (P : ideal A) [P.is_prime] :
   valuation_subring K :=
 of_le A (localization.subalgebra.of_field K P.prime_compl $
   le_non_zero_divisors_of_no_zero_divisors $ not_not_intro P.zero_mem).to_subring $
-  λ a ha, subalgebra.algebra_map_mem _ (⟨a,ha⟩ : A)
+  λ a ha, subalgebra.algebra_map_mem _ (⟨a, ha⟩ : A)
 
 instance of_prime_algebra (A : valuation_subring K) (P : ideal A) [P.is_prime] :
   algebra A (A.of_prime P) := subalgebra.algebra _
@@ -223,7 +223,7 @@ by apply localization.subalgebra.is_localization_of_field K
 
 lemma le_of_prime (A : valuation_subring K) (P : ideal A) [P.is_prime] :
   A ≤ of_prime A P :=
-λ a ha, subalgebra.algebra_map_mem _ (⟨a,ha⟩ : A)
+λ a ha, subalgebra.algebra_map_mem _ (⟨a, ha⟩ : A)
 
 lemma of_prime_valuation_eq_one_iff_mem_prime_compl
   (A : valuation_subring K)
@@ -243,7 +243,7 @@ lemma of_prime_ideal_of_le (R S : valuation_subring K) (h : R ≤ S) :
   of_prime R (ideal_of_le R S h) = S :=
 begin
   ext x, split,
-  { rintro ⟨a,r,hr,rfl⟩, apply mul_mem, { exact h a.2 },
+  { rintro ⟨a, r, hr, rfl⟩, apply mul_mem, { exact h a.2 },
     { rw [← valuation_le_one_iff, valuation.map_inv, ← inv_one, inv_le_inv₀],
       { exact not_lt.1 ((not_iff_not.2 $ valuation_lt_one_iff S _).1 hr) },
       { intro hh, erw [valuation.zero_iff, subring.coe_eq_zero_iff] at hh,
@@ -255,7 +255,7 @@ begin
     { use [1, x⁻¹, hr], split,
       { change (⟨x⁻¹, h hr⟩ : S) ∉ nonunits S,
         erw [mem_nonunits_iff, not_not],
-        apply is_unit_of_mul_eq_one _ (⟨x,hx⟩ : S),
+        apply is_unit_of_mul_eq_one _ (⟨x, hx⟩ : S),
         ext, field_simp },
       { field_simp } } },
 end
@@ -461,8 +461,8 @@ nonunits_injective.eq_iff.symm
 
 /-- `A.nonunits` agrees with the maximal ideal of `A`. -/
 def nonunits_equiv_maximal_ideal : A.nonunits ≃ local_ring.maximal_ideal A :=
-{ to_fun := λ a, ⟨⟨a,(A.valuation_le_one_iff _).1 (le_of_lt a.2)⟩,(A.valuation_lt_one_iff _).2 a.2⟩,
-  inv_fun := λ a, ⟨a,(A.valuation_lt_one_iff _).1 a.2⟩,
+{ to_fun := λ a, ⟨⟨a, (A.valuation_le_one_iff _).1 (le_of_lt a.2)⟩, (A.valuation_lt_one_iff _).2 a.2⟩,
+  inv_fun := λ a, ⟨a, (A.valuation_lt_one_iff _).1 a.2⟩,
   left_inv := λ a, by { ext, refl },
   right_inv := λ a, by { ext, refl } }
 

From 52fcc37e865266b1d185fbeeae63071ce789f858 Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Thu, 14 Jul 2022 10:54:57 +0000
Subject: [PATCH 09/15] Show `A.nonunits` agrees with the maximal ideal of `A`
 as an equality of subsets of `K`.

---
 .../valuation/valuation_subring.lean          | 49 +++++++++++--------
 1 file changed, 29 insertions(+), 20 deletions(-)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 2c8f4994b7e57..96b16481b9782 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -459,30 +459,39 @@ lemma eq_iff_nonunits {A B : valuation_subring K} :
   A = B ↔ A.nonunits = B.nonunits :=
 nonunits_injective.eq_iff.symm
 
-/-- `A.nonunits` agrees with the maximal ideal of `A`. -/
-def nonunits_equiv_maximal_ideal : A.nonunits ≃ local_ring.maximal_ideal A :=
-{ to_fun := λ a, ⟨⟨a, (A.valuation_le_one_iff _).1 (le_of_lt a.2)⟩, (A.valuation_lt_one_iff _).2 a.2⟩,
-  inv_fun := λ a, ⟨a, (A.valuation_lt_one_iff _).1 a.2⟩,
-  left_inv := λ a, by { ext, refl },
-  right_inv := λ a, by { ext, refl } }
+variables {A}
 
-@[simp]
-lemma coe_nonunits_equiv_maximal_ideal_apply (a : A.nonunits) :
-  (A.nonunits_equiv_maximal_ideal a : K) = a := rfl
+ /-- The elements of `A.nonunits` are those of the maximal ideal of `A` after coercion to `K`.
 
-@[simp]
-lemma coe_nonunits_equiv_maximal_ideal_symm_apply (a : local_ring.maximal_ideal A) :
-  (A.nonunits_equiv_maximal_ideal.symm a : K) = a := rfl
+See also `mem_nonunits_iff_exists_mem_maximal_ideal`, which gets rid of the coercion to `K`,
+at the expense of a more complicated right hand side.
+ -/
+theorem coe_mem_nonunits_iff {a : A} :
+  ((a : K) ∈ A.nonunits) ↔ a ∈ local_ring.maximal_ideal A :=
+by simp only [local_ring.mem_maximal_ideal, mem_nonunits_iff, valuation_lt_one_iff]
 
-@[simp]
-lemma nonunits_equiv_maximal_ideal_map_mul (a b : A.nonunits) :
-  A.nonunits_equiv_maximal_ideal (a * b) =
-  (A.nonunits_equiv_maximal_ideal a : A) • A.nonunits_equiv_maximal_ideal b := rfl
+lemma nonunits_subset : (A.nonunits : set K) ⊆ A :=
+λ a ha, (A.valuation_le_one_iff _).mp ((A.mem_nonunits_iff _).mp ha).le
 
-@[simp]
-lemma nonunits_equiv_maximal_ideal_symm_map_smul (a b : local_ring.maximal_ideal A) :
-  A.nonunits_equiv_maximal_ideal.symm ((a : A) • b) =
-  A.nonunits_equiv_maximal_ideal.symm a * A.nonunits_equiv_maximal_ideal.symm b := rfl
+ /-- The elements of `A.nonunits` are those of the maximal ideal of `A`.
+
+See also `coe_mem_nonunits_iff`, which has a simpler right hand side but requires the element
+to be in `A` already.
+ -/
+theorem mem_nonunits_iff_exists_mem_maximal_ideal {a : K} :
+  a ∈ A.nonunits ↔ ∃ ha, (⟨a, ha⟩ : A) ∈ local_ring.maximal_ideal A :=
+⟨λ h, ⟨nonunits_subset h, coe_mem_nonunits_iff.mp h⟩,
+ λ ⟨ha, h⟩, coe_mem_nonunits_iff.mpr h⟩
+
+ /-- `A.nonunits` agrees with the maximal ideal of `A`, after taking its image in `K`. -/
+theorem image_maximal_ideal : (coe : A → K) '' local_ring.maximal_ideal A = A.nonunits :=
+begin
+  ext a,
+  simp only [set.mem_image, set_like.mem_coe, mem_nonunits_iff_exists_mem_maximal_ideal],
+  split,
+  { rintros ⟨⟨a, ha⟩, h, rfl⟩, exact ⟨ha, h⟩ },
+  { rintros ⟨ha, h⟩, exact ⟨⟨a, ha⟩, h, rfl⟩ }
+end
 
 end nonunits
 

From 5b2c5699f501300cd16863b7aba106aecff2ae7f Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Thu, 14 Jul 2022 10:56:33 +0000
Subject: [PATCH 10/15] Make argument to `mem_nonunits_iff` implicit because
 it's on both sides of the `iff`

---
 src/ring_theory/valuation/valuation_subring.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 96b16481b9782..1a2e573feda6b 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -442,7 +442,7 @@ def nonunits : subsemigroup K :=
 { carrier := { x | A.valuation x < 1 },
   mul_mem' := λ a b ha hb, by { simpa using mul_lt_mul₀ ha hb } }
 
-lemma mem_nonunits_iff (x : K) : x ∈ A.nonunits ↔ A.valuation x < 1 := iff.refl _
+lemma mem_nonunits_iff {x : K} : x ∈ A.nonunits ↔ A.valuation x < 1 := iff.refl _
 
 lemma nonunits_injective :
   function.injective (nonunits : valuation_subring K → subsemigroup _) :=
@@ -471,7 +471,7 @@ theorem coe_mem_nonunits_iff {a : A} :
 by simp only [local_ring.mem_maximal_ideal, mem_nonunits_iff, valuation_lt_one_iff]
 
 lemma nonunits_subset : (A.nonunits : set K) ⊆ A :=
-λ a ha, (A.valuation_le_one_iff _).mp ((A.mem_nonunits_iff _).mp ha).le
+λ a ha, (A.valuation_le_one_iff _).mp (A.mem_nonunits_iff.mp ha).le
 
  /-- The elements of `A.nonunits` are those of the maximal ideal of `A`.
 

From 87ecfbaf693807367f94fc703487b1bc6211700f Mon Sep 17 00:00:00 2001
From: jackmckoen <104791831+jackmckoen@users.noreply.github.com>
Date: Fri, 15 Jul 2022 13:43:42 -0600
Subject: [PATCH 11/15] Apply suggestions from code review

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 src/ring_theory/valuation/basic.lean          | 10 ++++----
 .../valuation/valuation_subring.lean          | 25 ++++++++-----------
 2 files changed, 16 insertions(+), 19 deletions(-)

diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
index 992d82d6d943e..6ea92035a8aae 100644
--- a/src/ring_theory/valuation/basic.lean
+++ b/src/ring_theory/valuation/basic.lean
@@ -471,11 +471,11 @@ lemma is_equiv_tfae
   [linear_ordered_comm_group_with_zero Γ'₀]
   {K : Type*} [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
-  [ v.is_equiv v'
-  , ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1
-  , ∀ {x}, v x = 1 ↔ v' x = 1
-  , ∀ {x}, v x < 1 ↔ v' x < 1
-  , ∀ {x}, v (x-1) < 1 ↔ v' (x-1) < 1].tfae :=
+  [v.is_equiv v',
+   ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1,
+   ∀ {x}, v x = 1 ↔ v' x = 1,
+   ∀ {x}, v x < 1 ↔ v' x < 1,
+   ∀ {x}, v (x-1) < 1 ↔ v' (x-1) < 1].tfae :=
 begin
   tfae_have : 1 ↔ 2, { apply is_equiv_iff_val_le_one },
   tfae_have : 1 ↔ 3, { apply is_equiv_iff_val_eq_one },
diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 1a2e573feda6b..5f731790d1d3c 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -440,7 +440,7 @@ section nonunits
 /-- The nonunits of a valuation subring, as a subsemigroup of `K`-/
 def nonunits : subsemigroup K :=
 { carrier := { x | A.valuation x < 1 },
-  mul_mem' := λ a b ha hb, by { simpa using mul_lt_mul₀ ha hb } }
+  mul_mem' := λ a b ha hb, (mul_lt_mul₀ ha hb).trans_eq $ mul_one _ }
 
 lemma mem_nonunits_iff {x : K} : x ∈ A.nonunits ↔ A.valuation x < 1 := iff.refl _
 
@@ -450,14 +450,11 @@ lemma nonunits_injective :
   rw [← A.valuation_subring_valuation, ← B.valuation_subring_valuation,
     ← valuation.is_equiv_iff_valuation_subring, valuation.is_equiv_iff_val_lt_one],
   rw set_like.ext_iff at h,
-  intros x,
-  by_cases hx : x = 0, { simp only [hx, valuation.map_zero, zero_lt_one₀] },
-  exact h (units.mk0 x hx)
+  exact set_like.ext_iff.1 h
 end
 
-lemma eq_iff_nonunits {A B : valuation_subring K} :
-  A = B ↔ A.nonunits = B.nonunits :=
-nonunits_injective.eq_iff.symm
+lemma nonunits_inj {A B : valuation_subring K} : A.nonunits = B.nonunits ↔ A = B :=
+nonunits_injective.eq_iff
 
 variables {A}
 
@@ -466,13 +463,14 @@ variables {A}
 See also `mem_nonunits_iff_exists_mem_maximal_ideal`, which gets rid of the coercion to `K`,
 at the expense of a more complicated right hand side.
  -/
-theorem coe_mem_nonunits_iff {a : A} :
-  ((a : K) ∈ A.nonunits) ↔ a ∈ local_ring.maximal_ideal A :=
-by simp only [local_ring.mem_maximal_ideal, mem_nonunits_iff, valuation_lt_one_iff]
+theorem coe_mem_nonunits_iff {a : A} : (a : K) ∈ A.nonunits ↔ a ∈ local_ring.maximal_ideal A :=
+(valuation_lt_one_iff _ _).symm
 
-lemma nonunits_subset : (A.nonunits : set K) ⊆ A :=
+lemma nonunits_le : A.nonunits ≤ A.to_subring.to_submonoid.to_subsemigroup :=
 λ a ha, (A.valuation_le_one_iff _).mp (A.mem_nonunits_iff.mp ha).le
 
+lemma nonunits_subset : (A.nonunits : set K) ⊆ A := nonunits_le
+
  /-- The elements of `A.nonunits` are those of the maximal ideal of `A`.
 
 See also `coe_mem_nonunits_iff`, which has a simpler right hand side but requires the element
@@ -488,9 +486,8 @@ theorem image_maximal_ideal : (coe : A → K) '' local_ring.maximal_ideal A = A.
 begin
   ext a,
   simp only [set.mem_image, set_like.mem_coe, mem_nonunits_iff_exists_mem_maximal_ideal],
-  split,
-  { rintros ⟨⟨a, ha⟩, h, rfl⟩, exact ⟨ha, h⟩ },
-  { rintros ⟨ha, h⟩, exact ⟨⟨a, ha⟩, h, rfl⟩ }
+  erw subtype.exists,
+  simp_rw [subtype.coe_mk, exists_and_distrib_right, exists_eq_right],
 end
 
 end nonunits

From 0535212406b63052edb17e5507d5f789ca6880b4 Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Fri, 15 Jul 2022 14:28:35 -0600
Subject: [PATCH 12/15] add K as variable and small golf

---
 src/ring_theory/valuation/basic.lean | 48 +++++++++++++---------------
 1 file changed, 23 insertions(+), 25 deletions(-)

diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
index 6ea92035a8aae..8660e4a908569 100644
--- a/src/ring_theory/valuation/basic.lean
+++ b/src/ring_theory/valuation/basic.lean
@@ -67,7 +67,7 @@ noncomputable theory
 
 open function ideal
 
-variables {F R : Type*} -- This will be a ring, assumed commutative in some sections
+variables {K F R : Type*} -- This will be a ring, assumed commutative in some sections
 
 section
 variables (F R) (Γ₀ : Type*) [linear_ordered_comm_monoid_with_zero Γ₀] [ring R]
@@ -170,12 +170,12 @@ lemma ext_iff {v₁ v₂ : valuation R Γ₀} : v₁ = v₂ ↔ ∀ r, v₁ r =
 def to_preorder : preorder R := preorder.lift v
 
 /-- If `v` is a valuation on a division ring then `v(x) = 0` iff `x = 0`. -/
-@[simp] lemma zero_iff [nontrivial Γ₀] {K : Type*} [division_ring K]
-  (v : valuation K Γ₀) {x : K} : v x = 0 ↔ x = 0 :=
+@[simp] lemma zero_iff [nontrivial Γ₀] [division_ring K] (v : valuation K Γ₀) {x : K} :
+  v x = 0 ↔ x = 0 :=
 v.to_monoid_with_zero_hom.map_eq_zero
 
-lemma ne_zero_iff [nontrivial Γ₀] {K : Type*} [division_ring K]
-  (v : valuation K Γ₀) {x : K} : v x ≠ 0 ↔ x ≠ 0 :=
+lemma ne_zero_iff [nontrivial Γ₀] [division_ring K] (v : valuation K Γ₀) {x : K} :
+  v x ≠ 0 ↔ x ≠ 0 :=
 v.to_monoid_with_zero_hom.map_ne_zero
 
 theorem unit_map_eq (u : Rˣ) :
@@ -217,11 +217,11 @@ end monoid
 section group
 variables [linear_ordered_comm_group_with_zero Γ₀] {R} {Γ₀} (v : valuation R Γ₀) {x y z : R}
 
-@[simp] lemma map_inv {K : Type*} [division_ring K]
-  (v : valuation K Γ₀) {x : K} : v x⁻¹ = (v x)⁻¹ :=
+@[simp] lemma map_inv [division_ring K] (v : valuation K Γ₀) {x : K} :
+  v x⁻¹ = (v x)⁻¹ :=
 v.to_monoid_with_zero_hom.map_inv x
 
-@[simp] lemma map_zpow {K : Type*} [division_ring K] (v : valuation K Γ₀) {x : K} {n : ℤ} :
+@[simp] lemma map_zpow [division_ring K] (v : valuation K Γ₀) {x : K} {n : ℤ} :
   v (x^n) = (v x)^n :=
 v.to_monoid_with_zero_hom.map_zpow x n
 
@@ -293,12 +293,9 @@ begin
   simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h
 end
 
-lemma one_lt_val_iff
-  {K : Type*} [division_ring K] (v : valuation K Γ₀) {x : K} (h : x ≠ 0) :
+lemma one_lt_val_iff [division_ring K] (v : valuation K Γ₀) {x : K} (h : x ≠ 0) :
   1 < v x ↔ v x⁻¹ < 1 :=
-begin
-  simpa using (inv_lt_inv₀ (v.ne_zero_iff.2 h) one_ne_zero).symm,
-end
+by simpa using (inv_lt_inv₀ (v.ne_zero_iff.2 h) one_ne_zero).symm
 
 /-- The subgroup of elements whose valuation is less than a certain unit.-/
 def lt_add_subgroup (v : valuation R Γ₀) (γ : Γ₀ˣ) : add_subgroup R :=
@@ -365,7 +362,7 @@ lemma is_equiv_of_map_strict_mono [linear_ordered_comm_monoid_with_zero Γ₀]
 
 lemma is_equiv_of_val_le_one [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
+  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) (h : ∀ {x:K}, v x ≤ 1 ↔ v' x ≤ 1) :
   v.is_equiv v' :=
 begin
@@ -389,7 +386,7 @@ end
 lemma is_equiv_iff_val_le_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
+  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1 :=
 ⟨λ h x, by  simpa using h x 1, is_equiv_of_val_le_one _ _⟩
@@ -397,7 +394,7 @@ lemma is_equiv_iff_val_le_one
 lemma is_equiv_iff_val_eq_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
+  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1 :=
 begin
@@ -429,7 +426,7 @@ end
 lemma is_equiv_iff_val_lt_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
+  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1 :=
 begin
@@ -458,7 +455,7 @@ end
 lemma is_equiv_iff_val_sub_one_lt_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
+  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1 :=
 begin
@@ -469,7 +466,7 @@ end
 lemma is_equiv_tfae
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
+  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   [v.is_equiv v',
    ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1,
@@ -670,12 +667,13 @@ valuation.ext_iff
 def to_preorder : preorder R := preorder.lift v
 
 /-- If `v` is an additive valuation on a division ring then `v(x) = ⊤` iff `x = 0`. -/
-@[simp] lemma top_iff [nontrivial Γ₀] {K : Type*} [division_ring K]
-  (v : add_valuation K Γ₀) {x : K} : v x = ⊤ ↔ x = 0 :=
+@[simp] lemma top_iff [nontrivial Γ₀] [division_ring K] (v : add_valuation K Γ₀) {x : K} :
+  v x = ⊤ ↔ x = 0 :=
 v.zero_iff
 
-lemma ne_top_iff [nontrivial Γ₀] {K : Type*} [division_ring K]
-  (v : add_valuation K Γ₀) {x : K} : v x ≠ ⊤ ↔ x ≠ 0 := v.ne_zero_iff
+lemma ne_top_iff [nontrivial Γ₀] [division_ring K] (v : add_valuation K Γ₀) {x : K} :
+  v x ≠ ⊤ ↔ x ≠ 0 :=
+v.ne_zero_iff
 
 /-- A ring homomorphism `S → R` induces a map `add_valuation R Γ₀ → add_valuation S Γ₀`. -/
 def comap {S : Type*} [ring S] (f : S →+* R) (v : add_valuation R Γ₀) :
@@ -709,8 +707,8 @@ end monoid
 section group
 variables [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {x y z : R}
 
-@[simp] lemma map_inv {K : Type*} [division_ring K]
-  (v : add_valuation K Γ₀) {x : K} : v x⁻¹ = - (v x) :=
+@[simp] lemma map_inv [division_ring K] (v : add_valuation K Γ₀) {x : K} :
+  v x⁻¹ = - (v x) :=
 v.map_inv
 
 lemma map_units_inv (x : Rˣ) : v (x⁻¹ : Rˣ) = - (v x) :=

From 4861ac64876f9ecef0b8ef6a4e175ac7b51a1101 Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Fri, 15 Jul 2022 16:18:35 -0600
Subject: [PATCH 13/15] correction

---
 src/ring_theory/valuation/valuation_subring.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index 5f731790d1d3c..b8c9788a33dd2 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -449,8 +449,7 @@ lemma nonunits_injective :
 λ A B h, begin
   rw [← A.valuation_subring_valuation, ← B.valuation_subring_valuation,
     ← valuation.is_equiv_iff_valuation_subring, valuation.is_equiv_iff_val_lt_one],
-  rw set_like.ext_iff at h,
-  exact set_like.ext_iff.1 h
+  exact set_like.ext_iff.1 h,
 end
 
 lemma nonunits_inj {A B : valuation_subring K} : A.nonunits = B.nonunits ↔ A = B :=

From 167fda549cedd341c8b3b73d4f95a9fa852a4819 Mon Sep 17 00:00:00 2001
From: jackmckoen <104791831+jackmckoen@users.noreply.github.com>
Date: Sat, 16 Jul 2022 09:06:18 -0600
Subject: [PATCH 14/15] Update src/ring_theory/valuation/valuation_subring.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/ring_theory/valuation/valuation_subring.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index b8c9788a33dd2..db851af835777 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -437,7 +437,7 @@ end unit_group
 
 section nonunits
 
-/-- The nonunits of a valuation subring, as a subsemigroup of `K`-/
+/-- The nonunits of a valuation subring of `K`, as a subsemigroup of `K`-/
 def nonunits : subsemigroup K :=
 { carrier := { x | A.valuation x < 1 },
   mul_mem' := λ a b ha hb, (mul_lt_mul₀ ha hb).trans_eq $ mul_one _ }

From f48a73334c007df6a6d67965650f5e14a6c5b3bd Mon Sep 17 00:00:00 2001
From: jackmckoen <mckoen@ualberta.ca>
Date: Wed, 20 Jul 2022 14:03:23 -0600
Subject: [PATCH 15/15] add variable and order embedding

---
 src/ring_theory/valuation/basic.lean          | 24 +++++++------------
 .../valuation/valuation_subring.lean          | 21 +++++++++++++++-
 2 files changed, 29 insertions(+), 16 deletions(-)

diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
index 8660e4a908569..0174b62776a02 100644
--- a/src/ring_theory/valuation/basic.lean
+++ b/src/ring_theory/valuation/basic.lean
@@ -67,7 +67,7 @@ noncomputable theory
 
 open function ideal
 
-variables {K F R : Type*} -- This will be a ring, assumed commutative in some sections
+variables {K F R : Type*} [division_ring K]
 
 section
 variables (F R) (Γ₀ : Type*) [linear_ordered_comm_monoid_with_zero Γ₀] [ring R]
@@ -170,11 +170,11 @@ lemma ext_iff {v₁ v₂ : valuation R Γ₀} : v₁ = v₂ ↔ ∀ r, v₁ r =
 def to_preorder : preorder R := preorder.lift v
 
 /-- If `v` is a valuation on a division ring then `v(x) = 0` iff `x = 0`. -/
-@[simp] lemma zero_iff [nontrivial Γ₀] [division_ring K] (v : valuation K Γ₀) {x : K} :
+@[simp] lemma zero_iff [nontrivial Γ₀] (v : valuation K Γ₀) {x : K} :
   v x = 0 ↔ x = 0 :=
 v.to_monoid_with_zero_hom.map_eq_zero
 
-lemma ne_zero_iff [nontrivial Γ₀] [division_ring K] (v : valuation K Γ₀) {x : K} :
+lemma ne_zero_iff [nontrivial Γ₀] (v : valuation K Γ₀) {x : K} :
   v x ≠ 0 ↔ x ≠ 0 :=
 v.to_monoid_with_zero_hom.map_ne_zero
 
@@ -217,11 +217,11 @@ end monoid
 section group
 variables [linear_ordered_comm_group_with_zero Γ₀] {R} {Γ₀} (v : valuation R Γ₀) {x y z : R}
 
-@[simp] lemma map_inv [division_ring K] (v : valuation K Γ₀) {x : K} :
+@[simp] lemma map_inv (v : valuation K Γ₀) {x : K} :
   v x⁻¹ = (v x)⁻¹ :=
 v.to_monoid_with_zero_hom.map_inv x
 
-@[simp] lemma map_zpow [division_ring K] (v : valuation K Γ₀) {x : K} {n : ℤ} :
+@[simp] lemma map_zpow (v : valuation K Γ₀) {x : K} {n : ℤ} :
   v (x^n) = (v x)^n :=
 v.to_monoid_with_zero_hom.map_zpow x n
 
@@ -293,7 +293,7 @@ begin
   simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h
 end
 
-lemma one_lt_val_iff [division_ring K] (v : valuation K Γ₀) {x : K} (h : x ≠ 0) :
+lemma one_lt_val_iff (v : valuation K Γ₀) {x : K} (h : x ≠ 0) :
   1 < v x ↔ v x⁻¹ < 1 :=
 by simpa using (inv_lt_inv₀ (v.ne_zero_iff.2 h) one_ne_zero).symm
 
@@ -362,7 +362,6 @@ lemma is_equiv_of_map_strict_mono [linear_ordered_comm_monoid_with_zero Γ₀]
 
 lemma is_equiv_of_val_le_one [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) (h : ∀ {x:K}, v x ≤ 1 ↔ v' x ≤ 1) :
   v.is_equiv v' :=
 begin
@@ -386,7 +385,6 @@ end
 lemma is_equiv_iff_val_le_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1 :=
 ⟨λ h x, by  simpa using h x 1, is_equiv_of_val_le_one _ _⟩
@@ -394,7 +392,6 @@ lemma is_equiv_iff_val_le_one
 lemma is_equiv_iff_val_eq_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1 :=
 begin
@@ -426,7 +423,6 @@ end
 lemma is_equiv_iff_val_lt_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1 :=
 begin
@@ -455,7 +451,6 @@ end
 lemma is_equiv_iff_val_sub_one_lt_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1 :=
 begin
@@ -466,7 +461,6 @@ end
 lemma is_equiv_tfae
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   [v.is_equiv v',
    ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1,
@@ -667,11 +661,11 @@ valuation.ext_iff
 def to_preorder : preorder R := preorder.lift v
 
 /-- If `v` is an additive valuation on a division ring then `v(x) = ⊤` iff `x = 0`. -/
-@[simp] lemma top_iff [nontrivial Γ₀] [division_ring K] (v : add_valuation K Γ₀) {x : K} :
+@[simp] lemma top_iff [nontrivial Γ₀] (v : add_valuation K Γ₀) {x : K} :
   v x = ⊤ ↔ x = 0 :=
 v.zero_iff
 
-lemma ne_top_iff [nontrivial Γ₀] [division_ring K] (v : add_valuation K Γ₀) {x : K} :
+lemma ne_top_iff [nontrivial Γ₀] (v : add_valuation K Γ₀) {x : K} :
   v x ≠ ⊤ ↔ x ≠ 0 :=
 v.ne_zero_iff
 
@@ -707,7 +701,7 @@ end monoid
 section group
 variables [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {x y z : R}
 
-@[simp] lemma map_inv [division_ring K] (v : add_valuation K Γ₀) {x : K} :
+@[simp] lemma map_inv (v : add_valuation K Γ₀) {x : K} :
   v x⁻¹ = - (v x) :=
 v.map_inv
 
diff --git a/src/ring_theory/valuation/valuation_subring.lean b/src/ring_theory/valuation/valuation_subring.lean
index db851af835777..f26a3abd9eb69 100644
--- a/src/ring_theory/valuation/valuation_subring.lean
+++ b/src/ring_theory/valuation/valuation_subring.lean
@@ -407,7 +407,7 @@ lemma unit_group_le_unit_group {A B : valuation_subring K} :
   A.unit_group ≤ B.unit_group ↔ A ≤ B :=
 begin
   split,
-  { rintros h x hx,
+  { intros h x hx,
     rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx,
     by_cases h_1 : x = 0, { simp only [h_1, zero_mem] },
     by_cases h_2 : 1 + x = 0,
@@ -455,6 +455,25 @@ end
 lemma nonunits_inj {A B : valuation_subring K} : A.nonunits = B.nonunits ↔ A = B :=
 nonunits_injective.eq_iff
 
+lemma nonunits_le_nonunits {A B : valuation_subring K} :
+  B.nonunits ≤ A.nonunits ↔ A ≤ B :=
+begin
+  split,
+  { intros h x hx,
+    by_cases h_1 : x = 0, { simp only [h_1, zero_mem] },
+    rw [← valuation_le_one_iff, ← not_lt, valuation.one_lt_val_iff _ h_1] at hx ⊢,
+    by_contra h_2, from hx (h h_2) },
+  { intros h x hx,
+    by_contra h_1, from not_lt.2 (monotone_map_of_le _ _ h (not_lt.1 h_1)) hx }
+end
+
+/-- The map on valuation subrings to their nonunits is a dual order embedding. -/
+def nonunits_order_embedding :
+  valuation_subring K ↪o (subsemigroup K)ᵒᵈ :=
+{ to_fun := λ A, A.nonunits,
+  inj' := nonunits_injective,
+  map_rel_iff' := λ A B, nonunits_le_nonunits }
+
 variables {A}
 
  /-- The elements of `A.nonunits` are those of the maximal ideal of `A` after coercion to `K`.