From fcc13150a755cc6e6f4fea81ca255a356ae8fae8 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 10 Oct 2019 20:02:51 +0200
Subject: [PATCH 1/9] gpow for group with zero

---
 src/for_mathlib/group_with_zero.lean | 130 +++++++++++++++++++++++++++
 1 file changed, 130 insertions(+)

diff --git a/src/for_mathlib/group_with_zero.lean b/src/for_mathlib/group_with_zero.lean
index f8cc4e66..c0cb1282 100644
--- a/src/for_mathlib/group_with_zero.lean
+++ b/src/for_mathlib/group_with_zero.lean
@@ -133,6 +133,10 @@ begin
   exact unit_ne_zero ((mk₀ a h.1) * (mk₀ b h.2))
 end
 
+instance : no_zero_divisors α :=
+{ eq_zero_or_eq_zero_of_mul_eq_zero := mul_eq_zero,
+  .. (‹_› : group_with_zero α) }
+
 @[simp] lemma mul_eq_zero_iff {a b : α} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
 ⟨mul_eq_zero a b, by rintro (H|H); simp [H]⟩
 
@@ -183,6 +187,132 @@ begin
       simp [with_zero.coe_inj, units.ext_iff, *] } }
 end
 
+theorem inv_comm_of_comm {a b : α} (H : a * b = b * a) : a⁻¹ * b = b * a⁻¹ :=
+begin
+  have : a⁻¹ * (b * a) * a⁻¹ = a⁻¹ * (a * b) * a⁻¹ :=
+    congr_arg (λ x:α, a⁻¹ * x * a⁻¹) H.symm,
+  by_cases h : a = 0, { rw [h, inv_zero', zero_mul, mul_zero] },
+  rwa [inv_mul_cancel_assoc_right _ _ h, mul_assoc, mul_inv_cancel_assoc_left _ _ h] at this,
+end
+
+section nat_pow
+
+@[simp] theorem inv_pow (a : α) (n : ℕ) : (a⁻¹)^n = (a^n)⁻¹ :=
+by induction n with n ih; [exact inv_one'.symm,
+  rw [pow_succ', pow_succ, ih, mul_inv_rev]]
+
+-- This should be done for [no_zero_divisors]
+lemma eq_zero_of_pow_eq_zero {a : α} {n : ℕ} (h : a^n = 0) : a = 0 :=
+begin
+  induction n with n ih,
+  { exfalso, rw pow_zero at h, exact one_ne_zero h },
+  rw [pow_succ, mul_eq_zero_iff] at h,
+  cases h; solve_by_elim
+end
+
+-- This should be done for [no_zero_divisors]
+lemma pow_ne_zero {a : α} {n : ℕ} (h : a ≠ 0) : a^n ≠ 0 :=
+assume H, h $ eq_zero_of_pow_eq_zero H
+
+theorem pow_sub (a : α) {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ :=
+have h1 : m - n + n = m, from nat.sub_add_cancel h,
+have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
+eq_mul_inv_of_mul_eq (pow_ne_zero ha) h2
+
+theorem pow_inv_comm (a : α) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m :=
+by rw inv_pow; exact inv_comm_of_comm (pow_mul_comm _ _ _)
+
+end nat_pow
+
+section int_pow
+open int
+
+/--
+The power operation in a group with zero.
+This extends `monoid.pow` to negative integers
+with the definition `a^(-n) = (a^n)⁻¹`.
+-/
+def gpow (a : α) : ℤ → α
+| (of_nat n) := a^n
+| -[1+n]     := (a^(nat.succ n))⁻¹
+
+@[priority 10] instance : has_pow α ℤ := ⟨gpow⟩
+
+@[simp] theorem gpow_coe_nat (a : α) (n : ℕ) : a ^ (n:ℤ) = a ^ n := rfl
+
+@[simp] theorem gpow_of_nat (a : α) (n : ℕ) : a ^ of_nat n = a ^ n := rfl
+
+@[simp] theorem gpow_neg_succ (a : α) (n : ℕ) : a ^ -[1+n] = (a ^ n.succ)⁻¹ := rfl
+
+local attribute [ematch] le_of_lt
+open nat
+
+@[simp] theorem gpow_zero (a : α) : a ^ (0:ℤ) = 1 := rfl
+
+@[simp] theorem gpow_one (a : α) : a ^ (1:ℤ) = a := mul_one _
+
+@[simp] theorem one_gpow : ∀ (n : ℤ), (1 : α) ^ n = 1
+| (n : ℕ) := one_pow _
+| -[1+ n] := show _⁻¹=(1:α), by rw [_root_.one_pow, inv_one']
+
+@[simp] theorem gpow_neg (a : α) : ∀ (n : ℤ), a ^ -n = (a ^ n)⁻¹
+| (n+1:ℕ) := rfl
+| 0       := inv_one'.symm
+| -[1+ n] := (inv_inv'' _).symm
+
+theorem gpow_neg_one (x : α) : x ^ (-1:ℤ) = x⁻¹ := congr_arg has_inv.inv $ pow_one x
+
+theorem inv_gpow (a : α) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
+| (n : ℕ) := inv_pow a n
+| -[1+ n] := congr_arg has_inv.inv $ inv_pow a (n+1)
+
+private lemma gpow_add_aux (a : α) (h : a ≠ 0) (m n : nat) :
+  a ^ ((of_nat m) + -[1+n]) = a ^ of_nat m * a ^ -[1+n] :=
+or.elim (nat.lt_or_ge m (nat.succ n))
+ (assume h1 : m < succ n,
+  have h2 : m ≤ n, from le_of_lt_succ h1,
+  suffices a ^ -[1+ n-m] = a ^ of_nat m * a ^ -[1+n],
+    by rwa [of_nat_add_neg_succ_of_nat_of_lt h1],
+  show (a ^ nat.succ (n - m))⁻¹ = a ^ of_nat m * a ^ -[1+n],
+  by rw [← succ_sub h2, pow_sub _ h (le_of_lt h1), mul_inv_rev, inv_inv'']; refl)
+ (assume : m ≥ succ n,
+  suffices a ^ (of_nat (m - succ n)) = (a ^ (of_nat m)) * (a ^ -[1+ n]),
+    by rw [of_nat_add_neg_succ_of_nat_of_ge]; assumption,
+  suffices a ^ (m - succ n) = a ^ m * (a ^ n.succ)⁻¹, from this,
+  by rw pow_sub; assumption)
+
+theorem gpow_add (a : α) (h : a ≠ 0) : ∀ (i j : ℤ), a ^ (i + j) = a ^ i * a ^ j
+| (of_nat m) (of_nat n) := pow_add _ _ _
+| (of_nat m) -[1+n]     := gpow_add_aux _ h _ _
+| -[1+m]     (of_nat n) := by rw [add_comm, gpow_add_aux _ h,
+  gpow_neg_succ, gpow_of_nat, ← inv_pow, ← pow_inv_comm]
+| -[1+m]     -[1+n]     :=
+  suffices (a ^ (m + succ (succ n)))⁻¹ = (a ^ m.succ)⁻¹ * (a ^ n.succ)⁻¹, from this,
+  by rw [← succ_add_eq_succ_add, add_comm, _root_.pow_add, mul_inv_rev]
+
+theorem gpow_add_one (a : α) (h : a ≠ 0) (i : ℤ) : a ^ (i + 1) = a ^ i * a :=
+by rw [gpow_add _ h, gpow_one]
+
+theorem gpow_one_add (a : α) (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i :=
+by rw [gpow_add _ h, gpow_one]
+
+theorem gpow_mul_comm (a : α) (h : a ≠ 0) (i j : ℤ) : a ^ i * a ^ j = a ^ j * a ^ i :=
+by rw [← gpow_add _ h, ← gpow_add _ h, add_comm]
+
+theorem gpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
+| (m : ℕ) (n : ℕ) := pow_mul _ _ _
+| (m : ℕ) -[1+ n] := (gpow_neg _ (m * succ n)).trans $
+  show (a ^ (m * succ n))⁻¹ = _, by rw pow_mul; refl
+| -[1+ m] (n : ℕ) := (gpow_neg _ (succ m * n)).trans $
+  show (a ^ (m.succ * n))⁻¹ = _, by rw [pow_mul, ← inv_pow]; refl
+| -[1+ m] -[1+ n] := (pow_mul a (succ m) (succ n)).trans $
+  show _ = (_⁻¹^_)⁻¹, by rw [inv_pow, inv_inv'']
+
+theorem gpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m :=
+by rw [mul_comm, gpow_mul]
+
+end int_pow
+
 end group_with_zero
 
 /-- A type `α` is a commutative “group with zero”

From 27201ec294eb6f3a97b127e63ed8257b61f308d5 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 10 Oct 2019 21:00:42 +0200
Subject: [PATCH 2/9] Fix build

---
 src/continuous_valuations.lean | 2 +-
 src/examples/padics.lean       | 3 ++-
 src/valuation/basic.lean       | 5 +++--
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/continuous_valuations.lean b/src/continuous_valuations.lean
index a54619fa..8c6e72df 100644
--- a/src/continuous_valuations.lean
+++ b/src/continuous_valuations.lean
@@ -116,7 +116,7 @@ begin
     split; intro hx,
     { cases hv x with H H, {assumption},
       { exfalso, rw H at hx, exact lt_irrefl _ hx }, },
-    { rw hx, apply lt_of_le_of_ne linear_ordered_structure.zero_le zero_ne_one } },
+    { rw hx, apply lt_of_le_of_ne linear_ordered_structure.zero_le, exact zero_ne_one } },
   { resetI, intro g, exact is_open_discrete _ }
 end
 
diff --git a/src/examples/padics.lean b/src/examples/padics.lean
index 03d0a9d6..5b21aee5 100644
--- a/src/examples/padics.lean
+++ b/src/examples/padics.lean
@@ -282,8 +282,9 @@ def padic.Spa_unique : unique (Spa $ padic.Huber_pair p) :=
         contrapose! h,
         obtain ⟨y, hy⟩ : ∃ y : ℤ_[p], x⁻¹ = y,
         { refine ⟨⟨x⁻¹, _⟩, rfl⟩, rw norm_inv, apply inv_le_one, apply le_of_lt, exact h },
-        refine (linear_ordered_structure.inv_lt_inv _ one_ne_zero).mp _,
+        refine (linear_ordered_structure.inv_lt_inv _ _).mp _,
         { rw valuation.ne_zero_iff, contrapose! hx, use [0, hx] },
+        { exact one_ne_zero },
         { rw [inv_one', ← valuation.map_inv, hy],
           refine lt_of_le_of_ne (v.map_plus y) _,
           assume H,
diff --git a/src/valuation/basic.lean b/src/valuation/basic.lean
index 030a71d4..6a2a367a 100644
--- a/src/valuation/basic.lean
+++ b/src/valuation/basic.lean
@@ -315,11 +315,12 @@ begin
   { contrapose! h, cases h with h₁ h₂,
     by_cases hx : v x ≤ 1,
     { refine ⟨x⁻¹, _⟩,
-      rw [v.map_inv', ← linear_ordered_structure.inv_lt_inv _ one_ne_zero,
+      rw [v.map_inv', ← linear_ordered_structure.inv_lt_inv _ _,
         inv_inv'', inv_one'],
       { exact lt_of_le_of_ne hx h₂ },
       { exact inv_ne_zero' _ h₁ },
-      { rwa v.ne_zero_iff at h₁ } },
+      { exact one_ne_zero },
+      { rwa v.ne_zero_iff at h₁, } },
     { push_neg at hx, exact ⟨_, hx⟩ } }
 end
 

From a7a2dc66f6699e202b99f0524736ca8eeee8eb3c Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 10 Oct 2019 23:14:33 +0200
Subject: [PATCH 3/9] Start on the height of nnreal

---
 .../linear_ordered_comm_group_with_zero.lean  | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/valuation/linear_ordered_comm_group_with_zero.lean b/src/valuation/linear_ordered_comm_group_with_zero.lean
index cc034876..cbc26c06 100644
--- a/src/valuation/linear_ordered_comm_group_with_zero.lean
+++ b/src/valuation/linear_ordered_comm_group_with_zero.lean
@@ -200,6 +200,7 @@ end
 end linear_ordered_structure
 
 namespace nnreal
+open linear_ordered_structure
 
 /-- The nonnegative real numbers form a linearly ordered commutative group with zero.-/
 noncomputable instance : linear_ordered_comm_group_with_zero nnreal :=
@@ -212,4 +213,25 @@ noncomputable instance : linear_ordered_comm_group_with_zero nnreal :=
   .. (infer_instance : linear_order nnreal),
   .. (infer_instance : comm_semiring nnreal) }
 
+--move this
+lemma cardinal.eq_one_iff_nonempty_subsingleton {α : Type*} :
+  cardinal.mk α = 1 ↔ (nonempty α ∧ subsingleton α) :=
+begin
+  symmetry,
+  rw [← cardinal.ne_zero_iff_nonempty, ← cardinal.le_one_iff_subsingleton],
+  rw [eq_iff_le_not_lt, ← cardinal.succ_zero, cardinal.lt_succ, cardinal.le_zero, and_comm],
+end
+
+lemma height : height (units nnreal) = 1 :=
+begin
+  refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, _⟩,
+  { constructor, any_goals { intros, exact set.mem_univ _ },
+    have h2 : (2:nnreal) ≠ 0 := by norm_num,
+    let two : units nnreal := ⟨2,2⁻¹, mul_inv_cancel' _ h2, inv_mul_cancel' _ h2⟩,
+    refine ⟨1, two, set.mem_univ _, set.mem_univ _, _⟩,
+    sorry
+    },
+    sorry
+end
+
 end nnreal

From fc708642feec96a98146b9c3410fc85c7309eb8b Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 10 Oct 2019 23:14:50 +0200
Subject: [PATCH 4/9] Start on discrete valuations

---
 src/valuation/discrete.lean | 61 +++++++++++++++++++++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 src/valuation/discrete.lean

diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean
new file mode 100644
index 00000000..1d15db43
--- /dev/null
+++ b/src/valuation/discrete.lean
@@ -0,0 +1,61 @@
+import valuation.basic
+
+/-!
+# Discrete valuations
+
+We define discrete valuations
+-/
+
+universe variables u u₀ u₁
+
+namespace valuation
+variables {R : Type u} [ring R]
+variables {Γ₀   : Type u₀} [linear_ordered_comm_group_with_zero Γ₀]
+variables {Γ₀'  : Type u₁} [linear_ordered_comm_group_with_zero Γ₀']
+variables (v : valuation R Γ₀) {v' : valuation R Γ₀'}
+
+def is_discrete : Prop :=
+∃ r : R, ∀ s : R, v s ≠ 0 → ∃ n : ℤ, v s = (v r)^n
+
+def is_non_discrete : Prop := (¬ v.is_trivial) ∧ (¬ v.is_discrete)
+
+namespace is_equiv
+variable {v}
+
+lemma is_discrete (h : v.is_equiv v') :
+  v.is_discrete ↔ v'.is_discrete :=
+begin
+  apply exists_congr, intro r,
+  apply forall_congr, intro s,
+  apply imp_congr_ctx h.ne_zero, intro hs,
+  apply exists_congr, intro n,
+  sorry
+end
+
+-- move this
+lemma eq_zero (h : v.is_equiv v') {r : R} :
+  v r = 0 ↔ v' r = 0 :=
+by { rw [← v.map_zero, ← v'.map_zero], exact h.val_eq }
+
+-- move this
+lemma eq_one (h : v.is_equiv v') {r : R} :
+  v r = 1 ↔ v' r = 1 :=
+by { rw [← v.map_one, ← v'.map_one], exact h.val_eq }
+
+-- move this
+lemma is_trivial (h : v.is_equiv v') :
+  v.is_trivial ↔ v'.is_trivial :=
+begin
+  apply forall_congr, intro r,
+  exact or_congr h.eq_zero h.eq_one,
+end
+
+lemma is_non_discrete (h : v.is_equiv v') :
+  v.is_non_discrete ↔ v'.is_non_discrete :=
+and_congr
+  (not_iff_not_of_iff h.is_trivial)
+  (not_iff_not_of_iff h.is_discrete)
+
+end is_equiv
+
+end valuation

From 3b2e8e381c464c33a63c1296b2529fa4eedf67c9 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Fri, 11 Oct 2019 11:23:27 +0200
Subject: [PATCH 5/9] We almost know that nnreal has height one

---
 .../linear_ordered_comm_group_with_zero.lean  | 78 +++++++++++++++++--
 1 file changed, 73 insertions(+), 5 deletions(-)

diff --git a/src/valuation/linear_ordered_comm_group_with_zero.lean b/src/valuation/linear_ordered_comm_group_with_zero.lean
index cbc26c06..0e42005d 100644
--- a/src/valuation/linear_ordered_comm_group_with_zero.lean
+++ b/src/valuation/linear_ordered_comm_group_with_zero.lean
@@ -222,16 +222,84 @@ begin
   rw [eq_iff_le_not_lt, ← cardinal.succ_zero, cardinal.lt_succ, cardinal.le_zero, and_comm],
 end
 
+-- move this
+lemma exists_one_lt {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] :
+  ∃ a : α, a ∈ S ∧ 1 < a :=
+begin
+  choose x y hx hy hxy using h.exists_ne,
+  rcases lt_trichotomy 1 x with Hx|rfl|Hx,
+  { use [x, hx, Hx] },
+  { rcases lt_trichotomy 1 y with Hy|rfl|Hy,
+    { use [y, hy, Hy] },
+    { contradiction },
+    { refine ⟨y⁻¹, is_convex.inv_mem hy, _⟩,
+      simpa using mul_lt_right y⁻¹ Hy, } },
+  { refine ⟨x⁻¹, is_convex.inv_mem hx, _⟩,
+    simpa using mul_lt_right x⁻¹ Hx, }
+end
+
+-- move this
+lemma exists_lt_one {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] :
+  ∃ a : α, a ∈ S ∧ a < 1 :=
+begin
+  rcases exists_one_lt S with ⟨x, H1, H2⟩,
+  use [x⁻¹, is_convex.inv_mem H1],
+  simpa using mul_lt_right x⁻¹ H2,
+end
+
+open_locale classical
+
+-- move this
+lemma is_convex.mem_of_between' {α : Type*} [linear_ordered_comm_group α]
+  (S : set α) [h : is_proper_convex S]
+  {a b c : α} (ha : a ∈ S) (hc : c ∈ S) (hab : a ≤ b) (hbc : b ≤ c) :
+  b ∈ S :=
+begin
+  cases le_total b 1 with hb hb,
+  { exact is_convex.mem_of_between hab hb ha },
+  rw ← _root_.inv_inv b,
+  apply is_convex.inv_mem,
+  apply @is_convex.mem_of_between α _ S _ c⁻¹ _ _ _ (is_convex.inv_mem hc),
+  { contrapose! hbc, have := mul_lt_right (b*c) hbc,
+    rwa [inv_mul_cancel_left, mul_left_comm, mul_left_inv, mul_one] at this },
+  { contrapose! hb, simpa using mul_lt_right b hb, }
+end
+
+-- move this
+lemma is_convex.pow_mem {α : Type*} [linear_ordered_comm_group α]
+  (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) (n : ℕ) :
+  a^n ∈ S :=
+begin
+  induction n with n ih, { rw pow_zero, exact is_convex.one_mem S },
+  rw pow_succ, exact is_convex.mul_mem ha ih,
+end
+
+-- move this
+lemma is_convex.gpow_mem {α : Type*} [linear_ordered_comm_group α]
+  (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) :
+  ∀ (n : ℤ), a^n ∈ S
+| (int.of_nat n) := by { rw [gpow_of_nat], exact is_convex.pow_mem S ha n }
+| -[1+n] := by { apply is_convex.inv_mem, exact is_convex.pow_mem S ha _ }
+
 lemma height : height (units nnreal) = 1 :=
 begin
-  refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, _⟩,
+  refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, ⟨_⟩⟩,
   { constructor, any_goals { intros, exact set.mem_univ _ },
     have h2 : (2:nnreal) ≠ 0 := by norm_num,
-    let two : units nnreal := ⟨2,2⁻¹, mul_inv_cancel' _ h2, inv_mul_cancel' _ h2⟩,
+    let two : units nnreal := group_with_zero.mk₀ 2 (by norm_num),
     refine ⟨1, two, set.mem_univ _, set.mem_univ _, _⟩,
-    sorry
-    },
-    sorry
+    rw [ne.def, units.ext_iff], show (1:nnreal) ≠ 2, by norm_num, },
+  { suffices key : ∀ S : set (units nnreal), is_proper_convex S → S = set.univ,
+    { intros S T, rw [subtype.ext, key S.1 S.2, key T.1 T.2], },
+    intros S hS, resetI,
+    rw set.eq_univ_iff_forall, intro y,
+    cases le_total 1 y with Hy Hy,
+    { rcases exists_one_lt S with ⟨x, hx, Hx⟩,
+      obtain ⟨n, hn⟩ : ∃ (n : ℕ), y ≤ x^n := sorry,
+      exact is_convex.mem_of_between' S (is_convex.one_mem S) (is_convex.pow_mem S hx _) Hy hn, },
+    { rcases exists_lt_one S with ⟨x, hx, Hx⟩,
+      obtain ⟨n, hn⟩ : ∃ (n : ℕ), x^n ≤ y := sorry,
+      exact is_convex.mem_of_between hn Hy (is_convex.pow_mem S hx _) } }
 end
 
 end nnreal

From 55f355a86e0fdc2615148d43611b34da8459be67 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Fri, 11 Oct 2019 13:43:39 +0200
Subject: [PATCH 6/9] Move things around a bit

---
 src/for_mathlib/nnreal.lean                   | 104 +++++++++++++++++
 .../linear_ordered_comm_group_with_zero.lean  | 105 ------------------
 2 files changed, 104 insertions(+), 105 deletions(-)

diff --git a/src/for_mathlib/nnreal.lean b/src/for_mathlib/nnreal.lean
index a0ab5126..f4f9a410 100644
--- a/src/for_mathlib/nnreal.lean
+++ b/src/for_mathlib/nnreal.lean
@@ -1,6 +1,8 @@
 import data.real.nnreal
 import analysis.complex.exponential
 
+import valuation.linear_ordered_comm_group_with_zero
+
 namespace nnreal
 
 @[simp] lemma coe_max (x y : nnreal) : ((max x y : nnreal) : ℝ) = max (x : ℝ) (y : ℝ) :=
@@ -30,4 +32,106 @@ by rw [← real.rpow_one a, ← nat.cast_one, rpow_nat_cast, real.rpow_nat_cast,
 lemma rpow_le_rpow {a b : nnreal} (h : a ≤ b) (hx : 0 ≤ x) : a^x ≤ b^x :=
 show (a^x : ℝ) ≤ b^x, from real.rpow_le_rpow a.2 h hx
 
+open linear_ordered_structure
+
+/-- The nonnegative real numbers form a linearly ordered commutative group with zero.-/
+noncomputable instance : linear_ordered_comm_group_with_zero nnreal :=
+{ inv_zero := by simp,
+  zero_le' := zero_le,
+  mul_le_mul_left := λ a b h c, mul_le_mul (le_refl _) h (zero_le _) (zero_le _),
+  mul_inv_cancel := λ a h, mul_inv_cancel h,
+  .. (infer_instance : zero_ne_one_class nnreal),
+  .. (infer_instance : has_inv nnreal),
+  .. (infer_instance : linear_order nnreal),
+  .. (infer_instance : comm_semiring nnreal) }
+
+--move this
+lemma cardinal.eq_one_iff_nonempty_subsingleton {α : Type*} :
+  cardinal.mk α = 1 ↔ (nonempty α ∧ subsingleton α) :=
+begin
+  symmetry,
+  rw [← cardinal.ne_zero_iff_nonempty, ← cardinal.le_one_iff_subsingleton],
+  rw [eq_iff_le_not_lt, ← cardinal.succ_zero, cardinal.lt_succ, cardinal.le_zero, and_comm],
+end
+
+-- move this
+lemma exists_one_lt {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] :
+  ∃ a : α, a ∈ S ∧ 1 < a :=
+begin
+  choose x y hx hy hxy using h.exists_ne,
+  rcases lt_trichotomy 1 x with Hx|rfl|Hx,
+  { use [x, hx, Hx] },
+  { rcases lt_trichotomy 1 y with Hy|rfl|Hy,
+    { use [y, hy, Hy] },
+    { contradiction },
+    { refine ⟨y⁻¹, is_convex.inv_mem hy, _⟩,
+      simpa using mul_lt_right y⁻¹ Hy, } },
+  { refine ⟨x⁻¹, is_convex.inv_mem hx, _⟩,
+    simpa using mul_lt_right x⁻¹ Hx, }
+end
+
+-- move this
+lemma exists_lt_one {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] :
+  ∃ a : α, a ∈ S ∧ a < 1 :=
+begin
+  rcases exists_one_lt S with ⟨x, H1, H2⟩,
+  use [x⁻¹, is_convex.inv_mem H1],
+  simpa using mul_lt_right x⁻¹ H2,
+end
+
+open_locale classical
+
+-- move this
+lemma is_convex.mem_of_between' {α : Type*} [linear_ordered_comm_group α]
+  (S : set α) [h : is_proper_convex S]
+  {a b c : α} (ha : a ∈ S) (hc : c ∈ S) (hab : a ≤ b) (hbc : b ≤ c) :
+  b ∈ S :=
+begin
+  cases le_total b 1 with hb hb,
+  { exact is_convex.mem_of_between hab hb ha },
+  rw ← _root_.inv_inv b,
+  apply is_convex.inv_mem,
+  apply @is_convex.mem_of_between α _ S _ c⁻¹ _ _ _ (is_convex.inv_mem hc),
+  { contrapose! hbc, have := mul_lt_right (b*c) hbc,
+    rwa [inv_mul_cancel_left, mul_left_comm, mul_left_inv, mul_one] at this },
+  { contrapose! hb, simpa using mul_lt_right b hb, }
+end
+
+-- move this
+lemma is_convex.pow_mem {α : Type*} [linear_ordered_comm_group α]
+  (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) (n : ℕ) :
+  a^n ∈ S :=
+begin
+  induction n with n ih, { rw pow_zero, exact is_convex.one_mem S },
+  rw pow_succ, exact is_convex.mul_mem ha ih,
+end
+
+-- move this
+lemma is_convex.gpow_mem {α : Type*} [linear_ordered_comm_group α]
+  (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) :
+  ∀ (n : ℤ), a^n ∈ S
+| (int.of_nat n) := by { rw [gpow_of_nat], exact is_convex.pow_mem S ha n }
+| -[1+n] := by { apply is_convex.inv_mem, exact is_convex.pow_mem S ha _ }
+
+lemma height : height (units nnreal) = 1 :=
+begin
+  refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, ⟨_⟩⟩,
+  { constructor, any_goals { intros, exact set.mem_univ _ },
+    have h2 : (2:nnreal) ≠ 0 := by norm_num,
+    let two : units nnreal := group_with_zero.mk₀ 2 (by norm_num),
+    refine ⟨1, two, set.mem_univ _, set.mem_univ _, _⟩,
+    rw [ne.def, units.ext_iff], show (1:nnreal) ≠ 2, by norm_num, },
+  { suffices key : ∀ S : set (units nnreal), is_proper_convex S → S = set.univ,
+    { intros S T, rw [subtype.ext, key S.1 S.2, key T.1 T.2], },
+    intros S hS, resetI,
+    rw set.eq_univ_iff_forall, intro y,
+    cases le_total 1 y with Hy Hy,
+    { rcases exists_one_lt S with ⟨x, hx, Hx⟩,
+      obtain ⟨n, hn⟩ : ∃ (n : ℕ), y ≤ x^n := sorry,
+      exact is_convex.mem_of_between' S (is_convex.one_mem S) (is_convex.pow_mem S hx _) Hy hn, },
+    { rcases exists_lt_one S with ⟨x, hx, Hx⟩,
+      obtain ⟨n, hn⟩ : ∃ (n : ℕ), x^n ≤ y := sorry,
+      exact is_convex.mem_of_between hn Hy (is_convex.pow_mem S hx _) } }
+end
+
 end nnreal
diff --git a/src/valuation/linear_ordered_comm_group_with_zero.lean b/src/valuation/linear_ordered_comm_group_with_zero.lean
index 0e42005d..bc7f18c7 100644
--- a/src/valuation/linear_ordered_comm_group_with_zero.lean
+++ b/src/valuation/linear_ordered_comm_group_with_zero.lean
@@ -198,108 +198,3 @@ begin
 end
 
 end linear_ordered_structure
-
-namespace nnreal
-open linear_ordered_structure
-
-/-- The nonnegative real numbers form a linearly ordered commutative group with zero.-/
-noncomputable instance : linear_ordered_comm_group_with_zero nnreal :=
-{ inv_zero := by simp,
-  zero_le' := zero_le,
-  mul_le_mul_left := λ a b h c, mul_le_mul (le_refl _) h (zero_le _) (zero_le _),
-  mul_inv_cancel := λ a h, mul_inv_cancel h,
-  .. (infer_instance : zero_ne_one_class nnreal),
-  .. (infer_instance : has_inv nnreal),
-  .. (infer_instance : linear_order nnreal),
-  .. (infer_instance : comm_semiring nnreal) }
-
---move this
-lemma cardinal.eq_one_iff_nonempty_subsingleton {α : Type*} :
-  cardinal.mk α = 1 ↔ (nonempty α ∧ subsingleton α) :=
-begin
-  symmetry,
-  rw [← cardinal.ne_zero_iff_nonempty, ← cardinal.le_one_iff_subsingleton],
-  rw [eq_iff_le_not_lt, ← cardinal.succ_zero, cardinal.lt_succ, cardinal.le_zero, and_comm],
-end
-
--- move this
-lemma exists_one_lt {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] :
-  ∃ a : α, a ∈ S ∧ 1 < a :=
-begin
-  choose x y hx hy hxy using h.exists_ne,
-  rcases lt_trichotomy 1 x with Hx|rfl|Hx,
-  { use [x, hx, Hx] },
-  { rcases lt_trichotomy 1 y with Hy|rfl|Hy,
-    { use [y, hy, Hy] },
-    { contradiction },
-    { refine ⟨y⁻¹, is_convex.inv_mem hy, _⟩,
-      simpa using mul_lt_right y⁻¹ Hy, } },
-  { refine ⟨x⁻¹, is_convex.inv_mem hx, _⟩,
-    simpa using mul_lt_right x⁻¹ Hx, }
-end
-
--- move this
-lemma exists_lt_one {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] :
-  ∃ a : α, a ∈ S ∧ a < 1 :=
-begin
-  rcases exists_one_lt S with ⟨x, H1, H2⟩,
-  use [x⁻¹, is_convex.inv_mem H1],
-  simpa using mul_lt_right x⁻¹ H2,
-end
-
-open_locale classical
-
--- move this
-lemma is_convex.mem_of_between' {α : Type*} [linear_ordered_comm_group α]
-  (S : set α) [h : is_proper_convex S]
-  {a b c : α} (ha : a ∈ S) (hc : c ∈ S) (hab : a ≤ b) (hbc : b ≤ c) :
-  b ∈ S :=
-begin
-  cases le_total b 1 with hb hb,
-  { exact is_convex.mem_of_between hab hb ha },
-  rw ← _root_.inv_inv b,
-  apply is_convex.inv_mem,
-  apply @is_convex.mem_of_between α _ S _ c⁻¹ _ _ _ (is_convex.inv_mem hc),
-  { contrapose! hbc, have := mul_lt_right (b*c) hbc,
-    rwa [inv_mul_cancel_left, mul_left_comm, mul_left_inv, mul_one] at this },
-  { contrapose! hb, simpa using mul_lt_right b hb, }
-end
-
--- move this
-lemma is_convex.pow_mem {α : Type*} [linear_ordered_comm_group α]
-  (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) (n : ℕ) :
-  a^n ∈ S :=
-begin
-  induction n with n ih, { rw pow_zero, exact is_convex.one_mem S },
-  rw pow_succ, exact is_convex.mul_mem ha ih,
-end
-
--- move this
-lemma is_convex.gpow_mem {α : Type*} [linear_ordered_comm_group α]
-  (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) :
-  ∀ (n : ℤ), a^n ∈ S
-| (int.of_nat n) := by { rw [gpow_of_nat], exact is_convex.pow_mem S ha n }
-| -[1+n] := by { apply is_convex.inv_mem, exact is_convex.pow_mem S ha _ }
-
-lemma height : height (units nnreal) = 1 :=
-begin
-  refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, ⟨_⟩⟩,
-  { constructor, any_goals { intros, exact set.mem_univ _ },
-    have h2 : (2:nnreal) ≠ 0 := by norm_num,
-    let two : units nnreal := group_with_zero.mk₀ 2 (by norm_num),
-    refine ⟨1, two, set.mem_univ _, set.mem_univ _, _⟩,
-    rw [ne.def, units.ext_iff], show (1:nnreal) ≠ 2, by norm_num, },
-  { suffices key : ∀ S : set (units nnreal), is_proper_convex S → S = set.univ,
-    { intros S T, rw [subtype.ext, key S.1 S.2, key T.1 T.2], },
-    intros S hS, resetI,
-    rw set.eq_univ_iff_forall, intro y,
-    cases le_total 1 y with Hy Hy,
-    { rcases exists_one_lt S with ⟨x, hx, Hx⟩,
-      obtain ⟨n, hn⟩ : ∃ (n : ℕ), y ≤ x^n := sorry,
-      exact is_convex.mem_of_between' S (is_convex.one_mem S) (is_convex.pow_mem S hx _) Hy hn, },
-    { rcases exists_lt_one S with ⟨x, hx, Hx⟩,
-      obtain ⟨n, hn⟩ : ∃ (n : ℕ), x^n ≤ y := sorry,
-      exact is_convex.mem_of_between hn Hy (is_convex.pow_mem S hx _) } }
-end
-
-end nnreal

From 16e718a02f7dd4e9f2a09e288e96933f23772fa4 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Fri, 11 Oct 2019 14:12:50 +0200
Subject: [PATCH 7/9] Make the nondiscrete life easier

---
 src/valuation/discrete.lean | 51 ++++++++++++++++++++++++++-----------
 1 file changed, 36 insertions(+), 15 deletions(-)

diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean
index 1d15db43..b8ef1a6b 100644
--- a/src/valuation/discrete.lean
+++ b/src/valuation/discrete.lean
@@ -8,30 +8,23 @@ We define discrete valuations
 
 universe variables u u₀ u₁
 
+open_locale classical
+
 namespace valuation
 variables {R : Type u} [ring R]
 variables {Γ₀   : Type u₀} [linear_ordered_comm_group_with_zero Γ₀]
 variables {Γ₀'  : Type u₁} [linear_ordered_comm_group_with_zero Γ₀']
 variables (v : valuation R Γ₀) {v' : valuation R Γ₀'}
 
+def is_non_discrete : Prop :=
+∀ r : R, v r < 1 → ∃ s : R, v r < v s ∧ v s < 1
+
 def is_discrete : Prop :=
 ∃ r : R, ∀ s : R, v s ≠ 0 → ∃ n : ℤ, v s = (v r)^n
 
-def is_non_discrete : Prop := (¬ v.is_trivial) ∧ (¬ v.is_discrete)
-
 namespace is_equiv
 variable {v}
 
-lemma is_discrete (h : v.is_equiv v') :
-  v.is_discrete ↔ v'.is_discrete :=
-begin
-  apply exists_congr, intro r,
-  apply forall_congr, intro s,
-  apply imp_congr_ctx h.ne_zero, intro hs,
-  apply exists_congr, intro n,
-  sorry
-end
-
 -- move this
 lemma eq_zero (h : v.is_equiv v') {r : R} :
   v r = 0 ↔ v' r = 0 :=
@@ -42,6 +35,16 @@ lemma eq_one (h : v.is_equiv v') {r : R} :
   v r = 1 ↔ v' r = 1 :=
 by { rw [← v.map_one, ← v'.map_one], exact h.val_eq }
 
+-- move this
+lemma lt_iff (h : v.is_equiv v') {r s : R} :
+  v r < v s ↔ v' r < v' s :=
+by { have := not_iff_not_of_iff (h s r), push_neg at this, exact this }
+
+-- move this
+lemma lt_one (h : v.is_equiv v') {r : R} :
+  v r < 1 ↔ v' r < 1 :=
+by { rw [← v.map_one, ← v'.map_one], exact h.lt_iff }
+
 -- move this
 lemma is_trivial (h : v.is_equiv v') :
   v.is_trivial ↔ v'.is_trivial :=
@@ -52,9 +55,27 @@ end
 
 lemma is_non_discrete (h : v.is_equiv v') :
   v.is_non_discrete ↔ v'.is_non_discrete :=
-and_congr
-  (not_iff_not_of_iff h.is_trivial)
-  (not_iff_not_of_iff h.is_discrete)
+begin
+  apply forall_congr, intro r,
+  apply imp_congr_ctx h.lt_one, intro hr,
+  apply exists_congr, intro s,
+  rw [h.lt_iff, h.lt_one]
+end
+
+-- This is not so trivial. But we don't need it atm.
+-- lemma is_discrete (h : v.is_equiv v') :
+--   v.is_discrete ↔ v'.is_discrete :=
+-- begin
+--   apply exists_congr, intro r,
+--   apply forall_congr, intro s,
+--   apply imp_congr_ctx h.ne_zero, intro hs,
+--   apply exists_congr, intro n,
+--   sorry
+-- end
+
+-- lemma trichotomy :
+--   v.is_trivial ∨ v.is_discrete ∨ v.is_non_discrete :=
+-- sorry
 
 end is_equiv
 

From d4981344443dc3cfab4518a40bc9792f69edc00b Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Fri, 11 Oct 2019 15:10:12 +0200
Subject: [PATCH 8/9] Move some lemmas in the proper place

---
 src/valuation/basic.lean    | 23 +++++++++++++++++++++++
 src/valuation/discrete.lean | 32 ++------------------------------
 2 files changed, 25 insertions(+), 30 deletions(-)

diff --git a/src/valuation/basic.lean b/src/valuation/basic.lean
index 6a2a367a..54ce5bc6 100644
--- a/src/valuation/basic.lean
+++ b/src/valuation/basic.lean
@@ -247,6 +247,22 @@ begin
   rwa [v₁.map_zero, v₂.map_zero] at this,
 end
 
+lemma eq_zero (h : v₁.is_equiv v₂) {r : R} :
+  v₁ r = 0 ↔ v₂ r = 0 :=
+by { rw [← v₁.map_zero, ← v₂.map_zero], exact h.val_eq }
+
+lemma eq_one (h : v₁.is_equiv v₂) {r : R} :
+  v₁ r = 1 ↔ v₂ r = 1 :=
+by { rw [← v₁.map_one, ← v₂.map_one], exact h.val_eq }
+
+lemma lt_iff (h : v₁.is_equiv v₂) {r s : R} :
+  v₁ r < v₁ s ↔ v₂ r < v₂ s :=
+by { have := not_iff_not_of_iff (h s r), push_neg at this, exact this }
+
+lemma lt_one (h : v₁.is_equiv v₂) {r : R} :
+  v₁ r < 1 ↔ v₂ r < 1 :=
+by { rw [← v₁.map_one, ← v₂.map_one], exact h.lt_iff }
+
 end is_equiv -- end of namespace
 
 lemma is_equiv_of_map_strict_mono [ring R] {v : valuation R Γ₀}
@@ -324,6 +340,13 @@ begin
     { push_neg at hx, exact ⟨_, hx⟩ } }
 end
 
+lemma is_equiv.is_trivial {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} (h : v₁.is_equiv v₂) :
+  v₁.is_trivial ↔ v₂.is_trivial :=
+begin
+  apply forall_congr, intro r,
+  exact or_congr h.eq_zero h.eq_one,
+end
+
 end trivial -- end of section
 
 section supp
diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean
index b8ef1a6b..b83d0ed9 100644
--- a/src/valuation/discrete.lean
+++ b/src/valuation/discrete.lean
@@ -13,8 +13,8 @@ open_locale classical
 namespace valuation
 variables {R : Type u} [ring R]
 variables {Γ₀   : Type u₀} [linear_ordered_comm_group_with_zero Γ₀]
-variables {Γ₀'  : Type u₁} [linear_ordered_comm_group_with_zero Γ₀']
-variables (v : valuation R Γ₀) {v' : valuation R Γ₀'}
+variables {Γ'₀  : Type u₁} [linear_ordered_comm_group_with_zero Γ'₀]
+variables (v : valuation R Γ₀) {v' : valuation R Γ'₀}
 
 def is_non_discrete : Prop :=
 ∀ r : R, v r < 1 → ∃ s : R, v r < v s ∧ v s < 1
@@ -25,34 +25,6 @@ def is_discrete : Prop :=
 namespace is_equiv
 variable {v}
 
--- move this
-lemma eq_zero (h : v.is_equiv v') {r : R} :
-  v r = 0 ↔ v' r = 0 :=
-by { rw [← v.map_zero, ← v'.map_zero], exact h.val_eq }
-
--- move this
-lemma eq_one (h : v.is_equiv v') {r : R} :
-  v r = 1 ↔ v' r = 1 :=
-by { rw [← v.map_one, ← v'.map_one], exact h.val_eq }
-
--- move this
-lemma lt_iff (h : v.is_equiv v') {r s : R} :
-  v r < v s ↔ v' r < v' s :=
-by { have := not_iff_not_of_iff (h s r), push_neg at this, exact this }
-
--- move this
-lemma lt_one (h : v.is_equiv v') {r : R} :
-  v r < 1 ↔ v' r < 1 :=
-by { rw [← v.map_one, ← v'.map_one], exact h.lt_iff }
-
--- move this
-lemma is_trivial (h : v.is_equiv v') :
-  v.is_trivial ↔ v'.is_trivial :=
-begin
-  apply forall_congr, intro r,
-  exact or_congr h.eq_zero h.eq_one,
-end
-
 lemma is_non_discrete (h : v.is_equiv v') :
   v.is_non_discrete ↔ v'.is_non_discrete :=
 begin

From 4a96399b856663b5440599a56bc9ff276d5fa1d5 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Fri, 11 Oct 2019 15:15:12 +0200
Subject: [PATCH 9/9] Add docstrings to definitons

---
 src/valuation/discrete.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean
index b83d0ed9..e570c2da 100644
--- a/src/valuation/discrete.lean
+++ b/src/valuation/discrete.lean
@@ -16,9 +16,13 @@ variables {Γ₀   : Type u₀} [linear_ordered_comm_group_with_zero Γ₀]
 variables {Γ'₀  : Type u₁} [linear_ordered_comm_group_with_zero Γ'₀]
 variables (v : valuation R Γ₀) {v' : valuation R Γ'₀}
 
+/-- A valuation on a ring R is nondiscrete if for every element of R with value x < 1,
+there is another element of R whose value lies between x and 1. -/
 def is_non_discrete : Prop :=
 ∀ r : R, v r < 1 → ∃ s : R, v r < v s ∧ v s < 1
 
+/-- A valuation on a ring R is discrete if there is an element x of the value monoid
+such that the valuation of every element of R is either 0 or an integer power of x. -/
 def is_discrete : Prop :=
 ∃ r : R, ∀ s : R, v s ≠ 0 → ∃ n : ℤ, v s = (v r)^n
 
@@ -45,10 +49,10 @@ end
 --   sorry
 -- end
 
+end is_equiv
+
 -- lemma trichotomy :
 --   v.is_trivial ∨ v.is_discrete ∨ v.is_non_discrete :=
 -- sorry
 
-end is_equiv
-
 end valuation