style(library/data): clean up proofs in pnat and real

library/data/pnat.lean

@@ -284,4 +284,35 @@ theorem inv_pceil_div (a b : ℚ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻
     ((div_div_eq_mul_div (ne_of_gt Hb) (ne_of_gt Ha))⁻¹ ▸
       !rat.one_mul⁻¹ ▸ !ubound_ge)
 
+theorem sep_by_inv {a b : ℚ} (H : a > b) : ∃ N : ℕ+, a > (b + N⁻¹ + N⁻¹) :=
+  begin
+    apply exists.elim (find_midpoint H),
+    intro c Hc,
+    existsi (pceil ((1 + 1 + 1) / c)),
+    apply rat.lt.trans,
+    rotate 1,
+    apply and.left Hc,
+    rewrite rat.add.assoc,
+    apply rat.add_lt_add_left,
+    rewrite -(@rat.add_halves c) at {3},
+    apply rat.add_lt_add,
+    repeat (apply rat.lt_of_le_of_lt;
+    apply inv_pceil_div;
+    apply dec_trivial;
+    apply and.right Hc;
+    apply div_lt_div_of_pos_of_lt_of_pos;
+    repeat (apply two_pos);
+    apply and.right Hc)
+  end
+
+theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0 ≤ a :=
+  rat.le_of_not_gt (suppose a < 0,
+    have H2 : 0 < -a, from neg_pos_of_neg this,
+   (rat.not_lt_of_ge !H) (iff.mp !lt_neg_iff_lt_neg (calc
+       (pceil (of_num 2 / -a))⁻¹ ≤ -a / of_num 2
+          : !inv_pceil_div dec_trivial H2
+                             ... < -a / 1
+          : div_lt_div_of_pos_of_lt_of_pos dec_trivial dec_trivial H2
+                             ... = -a : div_one)))
+
 end pnat

library/data/real/basic.lean

@@ -15,28 +15,11 @@ open -[coercions] rat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
 ----------------------------------------------------------------------------------------------------
+-- small helper lemmas
 
--------------------------------------
+theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
--- theorems to add to (ordered) field and/or rat
+        p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ :=
-
+  by rewrite [rat.mul.assoc, rat.right_distrib, *inv_mul_eq_mul_inv]
--- this can move to pnat
-theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c ∧ c > 0 :=
-  exists.intro ((a - b) / (1 + 1))
-    (and.intro (assert H2 : a + a > (b + b) + (a - b), from calc
-      a + a > b + a : rat.add_lt_add_right H
-      ... = b + a + b - b : rat.add_sub_cancel
-      ... = b + b + a - b : rat.add.right_comm
-      ... = (b + b) + (a - b) : add_sub,
-     assert H3 : (a + a) / (1 + 1) > ((b + b) + (a - b)) / (1 + 1),
-       from div_lt_div_of_lt_of_pos H2 dec_trivial,
-     by rewrite [div_two at H3, -div_add_div_same at H3, div_two at H3]; exact H3)
-    (pos_div_of_pos_of_pos (iff.mpr !sub_pos_iff_lt H) dec_trivial))
-
-theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) :=
-  calc
-     a + b - (c + d) = a + b - c - d   : sub_add_eq_sub_sub
-                 ... = a - c + b - d   : sub_add_eq_add_sub
-                 ... = a - c + (b - d) : add_sub
 
 theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) (H : n ≥ pceil (q / ε)) :
         q * n⁻¹ ≤ ε :=
@@ -48,13 +31,6 @@ theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0)
     repeat assumption
   end
 
--------------------------------------
--- small helper lemmas
-
-theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
-        p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ :=
-  by rewrite [rat.mul.assoc, rat.right_distrib, *inv_mul_eq_mul_inv]
-
 theorem find_thirds (a b : ℚ) (H : b > 0) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b :=
   let n := pceil (of_nat 4 / b) in
   have of_nat 3 * n⁻¹ < b, from calc
@@ -152,7 +128,6 @@ infix `≡` := equiv
 
 theorem equiv.refl (s : seq) : s ≡ s :=
   begin
-    rewrite ↑equiv,
     intros,
     rewrite [rat.sub_self, abs_zero],
     apply add_invs_nonneg
@@ -160,7 +135,6 @@ theorem equiv.refl (s : seq) : s ≡ s :=
 
 theorem equiv.symm (s t : seq) (H : s ≡ t) : t ≡ s :=
   begin
-    rewrite ↑equiv at *,
     intros,
     rewrite [-abs_neg, neg_sub],
     exact H n
@@ -169,7 +143,6 @@ theorem equiv.symm (s t : seq) (H : s ≡ t) : t ≡ s :=
 theorem bdd_of_eq {s t : seq} (H : s ≡ t) :
         ∀ j : ℕ+, ∀ n : ℕ+, n ≥ 2 * j → abs (s n - t n) ≤ j⁻¹ :=
   begin
-    rewrite ↑equiv at *,
     intros [j, n, Hn],
     apply rat.le.trans,
     apply H n,
@@ -182,12 +155,10 @@ theorem bdd_of_eq {s t : seq} (H : s ≡ t) :
 theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t)
         (H : ∀ j : ℕ+, ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ j⁻¹) : s ≡ t :=
   begin
-    rewrite ↑equiv,
     intros,
     have Hj : (∀ j : ℕ+, abs (s n - t n) ≤ n⁻¹ + n⁻¹ + j⁻¹ + j⁻¹ + j⁻¹), begin
       intros,
-      apply exists.elim (H j),
+      cases H j with [Nj, HNj],
-      intros [Nj, HNj],
       rewrite [-(rat.sub_add_cancel (s n) (s (max j Nj))), rat.add.assoc (s n + -s (max j Nj)),
               ↑regular at *],
       apply rat.le.trans,
@@ -219,21 +190,19 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t)
          rat.add_le_add_left Hms
        ... = n⁻¹ + n⁻¹ + j⁻¹ + j⁻¹ + j⁻¹ : by rewrite *rat.add.assoc)
     end,
-    apply (squeeze Hj)
+    apply squeeze Hj
   end
 
 theorem eq_of_bdd_var {s t : seq} (Hs : regular s) (Ht : regular t)
         (H : ∀ ε : ℚ, ε > 0 → ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ ε) : s ≡ t :=
   begin
     apply eq_of_bdd,
-    apply Hs,
+    repeat assumption,
-    apply Ht,
     intros,
     apply H j⁻¹,
     apply inv_pos
   end
 
-set_option pp.beta false
 theorem pnat_bound {ε : ℚ} (Hε : ε > 0) : ∃ p : ℕ+, p⁻¹ ≤ ε :=
   begin
     existsi (pceil (1 / ε)),
@@ -247,13 +216,11 @@ theorem bdd_of_eq_var {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡
         ∀ ε : ℚ, ε > 0 → ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ ε :=
   begin
     intro ε Hε,
-    apply (exists.elim (pnat_bound Hε)),
+    cases pnat_bound Hε with [N, HN],
-    intro N HN,
-    let Bd' := bdd_of_eq Heq N,
     existsi 2 * N,
     intro n Hn,
     apply rat.le.trans,
-    apply Bd' n Hn,
+    apply bdd_of_eq Heq N n Hn,
     assumption
   end
 
@@ -500,36 +467,24 @@ theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu
     (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) + (Kq s) * (Kq t) * (b⁻¹ + d⁻¹) + (Kq s) * (Kq u) * (a⁻¹ + d⁻¹) :=
   begin
     apply add_le_add_three,
-    repeat apply rat.mul_le_mul,
+    repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
-    apply Kq_bound Ht,
+           apply abs_nonneg),
-    apply Kq_bound Hu,
-    apply abs_nonneg,
-    apply Kq_bound_nonneg Ht,
     apply Hs,
     apply abs_nonneg,
     apply rat.mul_nonneg,
-    apply Kq_bound_nonneg Ht,
+    repeat (apply Kq_bound_nonneg | assumption),
-    apply Kq_bound_nonneg Hu,
     repeat apply rat.mul_le_mul,
-    apply Kq_bound Hs,
+    repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
-    apply Kq_bound Ht,
+           apply abs_nonneg),
-    apply abs_nonneg,
-    apply Kq_bound_nonneg Hs,
     apply Hu,
     apply abs_nonneg,
     apply rat.mul_nonneg,
-    apply Kq_bound_nonneg Hs,
+    repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
-    apply Kq_bound_nonneg Ht,
+           apply abs_nonneg),
-    repeat apply rat.mul_le_mul,
-    apply Kq_bound Hs,
-    apply Kq_bound Hu,
-    apply abs_nonneg,
-    apply Kq_bound_nonneg Hs,
     apply Ht,
     apply abs_nonneg,
     apply rat.mul_nonneg,
-    apply Kq_bound_nonneg Hs,
+    repeat (apply Kq_bound_nonneg; assumption)
-    apply Kq_bound_nonneg Hu
   end
 
 theorem s_mul_assoc {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) :
@@ -543,8 +498,7 @@ theorem s_mul_assoc {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regula
     apply reg_mul_reg Hs,
     apply reg_mul_reg Ht Hu,
     intros,
-    fapply exists.intro,
+    apply exists.intro,
-    rotate 1,
     intros,
     rewrite [↑smul, *DK_rewrite, *TK_rewrite, -*pnat.mul.assoc, -*rat.mul.assoc],
     apply rat.le.trans,
@@ -622,13 +576,7 @@ theorem neg_s_cancel (s : seq) (H : regular s) : sadd s (sneg s) ≡ zero :=
     rotate 3,
     apply s_add_comm,
     apply s_neg_cancel s H,
-    apply reg_add_reg,
+    repeat (apply reg_add_reg | apply reg_neg_reg | assumption),
-    apply H,
-    apply reg_neg_reg,
-    apply H,
-    apply reg_add_reg,
-    apply reg_neg_reg,
-    repeat apply H,
     apply zero_is_reg
   end
 
@@ -757,8 +705,7 @@ theorem mul_zero_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Htz :
     intro ε Hε,
     let Bd := bdd_of_eq_var Ht zero_is_reg Htz (ε / (Kq s))
                             (pos_div_of_pos_of_pos Hε (Kq_bound_pos Hs)),
-    apply exists.elim Bd,
+    cases Bd with [N, HN],
-    intro N HN,
     existsi N,
     intro n Hn,
     rewrite [↑equiv at Htz, ↑zero at *, rat.sub_zero, ↑smul, abs_mul],
@@ -832,18 +779,15 @@ theorem s_sub_cancel (s : seq) : sadd s (sneg s) ≡ zero :=
 theorem diff_equiv_zero_of_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (H : s ≡ t) :
         sadd s (sneg t) ≡ zero :=
   begin
-    let Hnt := reg_neg_reg Ht,
-    let Hsnt := reg_add_reg Hs Hnt,
-    let Htnt := reg_add_reg Ht Hnt,
     apply equiv.trans,
     rotate 4,
     apply s_sub_cancel t,
     rotate 2,
     apply zero_is_reg,
     apply add_well_defined,
-    repeat assumption,
+    repeat (assumption | apply reg_neg_reg),
     apply equiv.refl,
-    repeat assumption
+    repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
   end
 
 theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
@@ -917,7 +861,6 @@ theorem one_is_reg : regular one :=
 
 theorem s_one_mul {s : seq} (H : regular s) : smul one s ≡ s :=
   begin
-    rewrite ↑equiv,
     intros,
     rewrite [↑smul, ↑one, rat.one_mul],
     apply rat.le.trans,
@@ -1158,9 +1101,7 @@ definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (s.r_const a)
 theorem of_rat_add (a b : ℚ) : of_rat a + of_rat b = of_rat (a + b) :=
    quot.sound (s.r_add_consts a b)
 
-theorem of_rat_neg (a : ℚ) : -of_rat a = of_rat (-a) := quot.sound (s.r_neg_const a)
+theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a := eq.symm (quot.sound (s.r_neg_const a))
-
---theorem of_rat_sub (a b : ℚ) : of_rat a + - of_rat b = of_rat (a - b) := !of_rat_add
 
 theorem of_rat_mul (a b : ℚ) : of_rat a * of_rat b = of_rat (a * b) :=
   quot.sound (s.r_mul_consts a b)

library/data/real/complete.lean

@@ -44,10 +44,8 @@ theorem rat_approx {s : seq} (H : regular s) :
   begin
     intro m,
     rewrite ↑s_le,
-    apply exists.elim (rat_approx_l1 H m),
+    cases rat_approx_l1 H m with [q, Hq],
-    intro q Hq,
+    cases Hq with [N, HN],
-    apply exists.elim Hq,
-    intro N HN,
     existsi q,
     apply nonneg_of_bdd_within,
     repeat (apply reg_add_reg | apply reg_neg_reg | apply abs_reg_of_reg | apply const_reg
@@ -106,10 +104,7 @@ theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) :
   end
 
 theorem abs_const (a : ℚ) : const (abs a) ≡ s_abs (const a) :=
-  begin
+  by apply equiv.refl
-    rewrite [↑s_abs, ↑const],
-    apply equiv.refl
-  end
 
 theorem r_abs_const (a : ℚ) : requiv (r_const (abs a) ) (r_abs (r_const a)) := abs_const a
 
@@ -123,12 +118,10 @@ theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_a
     let Hz' := s_nonneg_of_ge_zero Hs Hz,
     existsi 2 * j,
     intro n Hn,
-    apply or.elim (em (s n ≥ 0)),
+    cases em (s n ≥ 0) with [Hpos, Hneg],
-    intro Hpos,
     rewrite [rat.abs_of_nonneg Hpos, sub_self, abs_zero],
     apply rat.le_of_lt,
     apply inv_pos,
-    intro Hneg,
     let Hneg' := lt_of_not_ge Hneg,
     have Hsn : -s n - s n > 0, from add_pos (neg_pos_of_neg Hneg') (neg_pos_of_neg Hneg'),
     rewrite [rat.abs_of_neg Hneg', rat.abs_of_pos Hsn],
@@ -160,8 +153,7 @@ theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) :
     end,
     existsi 2 * j,
     intro n Hn,
-    apply or.elim (em (s n ≥ 0)),
+    cases em (s n ≥ 0) with [Hpos, Hneg],
-    intro Hpos,
     have Hsn : s n + s n ≥ 0, from add_nonneg Hpos Hpos,
     rewrite [rat.abs_of_nonneg Hpos, ↑sneg, rat.sub_neg_eq_add, rat.abs_of_nonneg Hsn],
     rewrite [↑nonneg at Hz', ↑sneg at Hz'],
@@ -173,7 +165,6 @@ theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) :
     repeat (apply inv_ge_of_le; apply Hn),
     rewrite pnat.add_halves,
     apply rat.le.refl,
-    intro Hneg,
     let Hneg' := lt_of_not_ge Hneg,
     rewrite [rat.abs_of_neg Hneg', ↑sneg, rat.sub_neg_eq_add, rat.neg_add_eq_sub, rat.sub_self,
                 abs_zero],
@@ -219,11 +210,8 @@ theorem re_abs_is_abs : re_abs = real.abs := funext
   (begin
     intro x,
     apply eq.symm,
-    let Hor := em (zero ≤ x),
+    cases em (zero ≤ x) with [Hor1, Hor2],
-    apply or.elim Hor,
-    intro Hor1,
     rewrite [abs_of_nonneg Hor1, r_abs_nonneg Hor1],
-    intro Hor2,
     have Hor2' : x ≤ zero, from le_of_lt (lt_of_not_ge Hor2),
     rewrite [abs_of_neg (lt_of_not_ge Hor2), r_abs_nonpos Hor2']
   end)
@@ -320,23 +308,17 @@ theorem lim_seq_reg : s.regular lim_seq :=
     rewrite [abs_const, -of_rat_sub, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
     apply real.le.trans,
     apply abs_add_three,
-    let Hor := em (M (2 * m) ≥ M (2 * n)),
+    cases em (M (2 * m) ≥ M (2 * n)) with [Hor1, Hor2],
-    apply or.elim Hor,
-    intro Hor1,
     apply lim_seq_reg_helper Hor1,
-    intro Hor2,
     let Hor2' := pnat.le_of_lt (pnat.lt_of_not_le Hor2),
-    rewrite [real.abs_sub (X (Nb M n)), abs_sub (X (Nb M m)), abs_sub, -- ???
+    rewrite [real.abs_sub (X (Nb M n)), abs_sub (X (Nb M m)), abs_sub,
              rat.add.comm, add_comm_three],
     apply lim_seq_reg_helper Hor2'
   end
 
 theorem lim_seq_spec (k : ℕ+) :
         s.s_le (s.s_abs (s.sadd lim_seq (s.sneg (s.const (lim_seq k))))) (s.const k⁻¹) :=
-  begin
+  by apply s.const_bound; apply lim_seq_reg
-    apply s.const_bound,
-    apply lim_seq_reg
-  end
 
 noncomputable definition r_lim_seq : s.reg_seq :=
   s.reg_seq.mk lim_seq lim_seq_reg
@@ -449,7 +431,7 @@ theorem archimedean' (x : ℝ) : ∃ z : ℤ, x ≥ of_rat (of_int z) :=
   begin
     cases archimedean (-x) with [z, Hz],
     existsi -z,
-    rewrite [of_int_neg, -of_rat_neg], -- change the direction of of_rat_neg
+    rewrite [of_int_neg, of_rat_neg],
     apply iff.mp !neg_le_iff_neg_le Hz
   end
 
@@ -457,7 +439,7 @@ theorem archimedean_strict' (x : ℝ) : ∃ z : ℤ, x > of_rat (of_int z) :=
   begin
     cases archimedean_strict (-x) with [z, Hz],
     existsi -z,
-    rewrite [of_int_neg, -of_rat_neg],
+    rewrite [of_int_neg, of_rat_neg],
     apply iff.mp !neg_lt_iff_neg_lt Hz
   end
 
@@ -570,7 +552,7 @@ theorem floor_largest {x : ℝ} {z : ℤ} (Hz : z > floor x) : x < of_rat (of_in
 
 theorem ceil_spec (x : ℝ) : of_rat (of_int (ceil x)) ≥ x :=
   begin
-    rewrite [↑ceil, of_int_neg, -of_rat_neg],
+    rewrite [↑ceil, of_int_neg, of_rat_neg],
     apply iff.mp !le_neg_iff_le_neg,
     apply floor_spec
   end
@@ -579,7 +561,7 @@ theorem ceil_smallest {x : ℝ} {z : ℤ} (Hz : z < ceil x) : x > of_rat (of_int
   begin
     rewrite ↑ceil at Hz,
     let Hz' := floor_largest (iff.mp !int.lt_neg_iff_lt_neg Hz),
-    rewrite [of_int_neg at Hz', -of_rat_neg at Hz'],
+    rewrite [of_int_neg at Hz', of_rat_neg at Hz'],
     apply lt_of_neg_lt_neg Hz'
   end
 

library/data/real/division.lean

@@ -23,22 +23,6 @@ namespace s
 -----------------------------
 -- helper lemmas
 
-theorem neg_add_rewrite {a b : ℚ} : a + -b = -(b + -a) :=
-  by rewrite[neg_add_rev,neg_neg]
-
-theorem abs_abs_sub_abs_le_abs_sub (a b : ℚ) : abs (abs a - abs b) ≤ abs (a - b) :=
-  begin
-    apply rat.nonneg_le_nonneg_of_squares_le,
-    repeat apply abs_nonneg,
-    rewrite [*abs_sub_square, *abs_abs, *abs_mul_self],
-    apply sub_le_sub_left,
-    rewrite *rat.mul.assoc,
-    apply rat.mul_le_mul_of_nonneg_left,
-    rewrite -abs_mul,
-    apply le_abs_self,
-    apply trivial
-  end
-
 theorem and_of_not_or {a b : Prop} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b :=
   and.intro (assume H', H (or.inl H')) (assume H', H (or.inr H'))
 
@@ -49,7 +33,6 @@ definition s_abs (s : seq) : seq := λ n, abs (s n)
 
 theorem abs_reg_of_reg {s : seq} (Hs : regular s) : regular (s_abs s) :=
   begin
-    rewrite ↑regular at *,
     intros,
     apply rat.le.trans,
     apply abs_abs_sub_abs_le_abs_sub,
@@ -70,9 +53,7 @@ theorem abs_pos_of_nonzero {s : seq} (Hs : regular s) (Hnz : sep s zero) :
       apply s_zero_add,
       repeat (assumption | apply reg_add_reg | apply reg_neg_reg | apply zero_is_reg)
     end,
-    let H'' := bdd_away_of_pos (reg_neg_reg Hs) H',
+    cases bdd_away_of_pos (reg_neg_reg Hs) H' with [N, HN],
-    apply exists.elim H'',
-    intro N HN,
     existsi N,
     intro m Hm,
     apply rat.le.trans,
@@ -82,8 +63,7 @@ theorem abs_pos_of_nonzero {s : seq} (Hs : regular s) (Hnz : sep s zero) :
     intro Hnz2,
     let H' := pos_of_pos_equiv (reg_add_reg Hs (reg_neg_reg zero_is_reg)) (s_add_zero s Hs) Hnz2,
     let H'' := bdd_away_of_pos Hs H',
-    apply exists.elim H'',
+    cases H'' with [N, HN],
-    intro N HN,
     existsi N,
     intro m Hm,
     apply rat.le.trans,
@@ -93,9 +73,7 @@ theorem abs_pos_of_nonzero {s : seq} (Hs : regular s) (Hnz : sep s zero) :
 
 theorem sep_zero_of_pos {s : seq} (Hs : regular s) (Hpos : pos s) : sep s zero :=
   begin
-    rewrite ↑sep,
     apply or.inr,
-    rewrite ↑s_lt,
     apply pos_of_pos_equiv,
     rotate 2,
     apply Hpos,
@@ -211,14 +189,11 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
     have Hspm : s ((ps Hs Hsep) * (ps Hs Hsep) * m) ≠ 0, from
       s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * m ≥ ps Hs Hsep, by
         rewrite pnat.mul.assoc; apply pnat.mul_le_mul_right),
-    apply @decidable.cases_on (m < (ps Hs Hsep)) _ _,
+    cases em (m < ps Hs Hsep) with [Hmlt, Hmlt],
-      intro Hmlt,
+      cases em (n < ps Hs Hsep) with [Hnlt, Hnlt],
-      apply @decidable.cases_on (n < (ps Hs Hsep)) _ _,
-        intro Hnlt,
         rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt), (s_inv_of_sep_lt_p Hs Hsep Hnlt)],
         rewrite [sub_self, abs_zero],
         apply add_invs_nonneg,
-       intro Hnlt,
        rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt),
                 (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt))],
        rewrite [(div_sub_div Hsp Hspn), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
@@ -240,9 +215,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
        apply inv_ge_of_le,
        apply pnat.le_of_lt,
        apply Hmlt,
-      intro Hmlt,
+      cases em (n < ps Hs Hsep) with [Hnlt, Hnlt],
-      apply @decidable.cases_on (n < (ps Hs Hsep)) _ _,
-        intro Hnlt,
         rewrite [(s_inv_of_sep_lt_p Hs Hsep Hnlt),
                  (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt))],
         rewrite [(div_sub_div Hspm Hsp), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
@@ -264,7 +237,6 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
         apply inv_ge_of_le,
         apply pnat.le_of_lt,
         apply Hnlt,
-      intro Hnlt,
       rewrite [(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)),
               (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt))],
       rewrite [(div_sub_div Hspm Hspn), div_eq_mul_one_div, abs_mul, *one_mul, *mul_one],
@@ -517,7 +489,7 @@ theorem s_le_of_not_lt {s t : seq} (Hle : ¬ s_lt s t) : s_le t s :=
     let Hle' := iff.mp forall_iff_not_exists Hle,
     intro n,
     let Hn := neg_le_neg (rat.le_of_not_gt (Hle' n)),
-    rewrite [↑sadd, ↑sneg, neg_add_rewrite],
+    rewrite [↑sadd, ↑sneg, add_neg_eq_neg_add_rev],
     apply Hn
   end
 

library/data/real/order.lean

@@ -19,45 +19,6 @@ notation 2 := subtype.tag (of_num 2) dec_trivial
 
 ----------------------------------------------------------------------------------------------------
 
--- this could be moved to pnat, but it uses find_midpoint which still has sorries in real.basic
-theorem sep_by_inv {a b : ℚ} (H : a > b) : ∃ N : ℕ+, a > (b + N⁻¹ + N⁻¹) :=
-  begin
-    apply exists.elim (find_midpoint H),
-    intro c Hc,
-    existsi (pceil ((1 + 1 + 1) / c)),
-    apply rat.lt.trans,
-    rotate 1,
-    apply and.left Hc,
-    rewrite rat.add.assoc,
-    apply rat.add_lt_add_left,
-    rewrite -(@rat.add_halves c) at {3},
-    apply rat.add_lt_add,
-    repeat (apply lt_of_le_of_lt;
-    apply inv_pceil_div;
-    apply dec_trivial;
-    apply and.right Hc;
-    apply div_lt_div_of_pos_of_lt_of_pos;
-    repeat (apply dec_trivial);
-    apply and.right Hc)
-  end
-
-theorem helper_1 {a : ℚ} (H : a > 0) : -a + -a ≤ -a :=
-  !neg_add ▸ neg_le_neg (le_add_of_nonneg_left (le_of_lt H))
-
-theorem rewrite_helper8 (a b c : ℚ) : a - b = c - b + (a - c) :=
-  by rewrite[add_sub,rat.sub_add_cancel] ⬝ !rat.add.comm
-
-theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0 ≤ a :=
-  rat.le_of_not_gt (suppose a < 0,
-    have H2 : 0 < -a, from neg_pos_of_neg this,
-   (rat.not_lt_of_ge !H) (iff.mp !lt_neg_iff_lt_neg (calc
-       (pceil (of_num 2 / -a))⁻¹ ≤ -a / of_num 2
-          : !inv_pceil_div dec_trivial H2
-                             ... < -a / 1
-          : div_lt_div_of_pos_of_lt_of_pos dec_trivial dec_trivial H2
-                             ... = -a : div_one)))
-
----------
 namespace s
 definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n)
 
@@ -66,11 +27,8 @@ definition nonneg (s : seq) := ∀ n : ℕ+, -(n⁻¹) ≤ s n
 theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
         ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹ :=
   begin
-    apply exists.elim H,
+    cases H with [n, Hn],
-    intro n Hn,
+    cases sep_by_inv Hn with [N, HN],
-    let Em := sep_by_inv Hn,
-    apply exists.elim Em,
-    intro N HN,
     existsi N,
     intro m Hm,
     have Habs : abs (s m - s n) ≥ s n - s m, by rewrite abs_sub; apply le_abs_self,
@@ -94,9 +52,7 @@ theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
 
 theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹) : pos s :=
   begin
-    rewrite ↑pos,
+    cases H with [N, HN],
-    apply exists.elim H,
-    intro N HN,
     existsi (N + pone),
     apply lt_of_lt_of_le,
     apply inv_add_lt_left,
@@ -111,7 +67,6 @@ theorem bdd_within_of_nonneg {s : seq} (Hs : regular s) (H : nonneg s) :
     intros,
     existsi n,
     intro m Hm,
-    rewrite ↑nonneg at H,
     apply le.trans,
     apply neg_le_neg,
     apply inv_ge_of_le,
@@ -126,10 +81,7 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
     intro k,
     apply squeeze_2,
     intro ε Hε,
-    apply exists.elim (H (pceil ((1 + 1) / ε))),
+    cases H (pceil ((1 + 1) / ε)) with [N, HN],
-    intro N HN,
-    let HN' := HN (max (pceil ((1+1)/ε)) N),
-    let HN'' := HN' (!max_right),
     apply le.trans,
     rotate 1,
     apply ge_sub_of_abs_sub_le_left,
@@ -141,7 +93,7 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
     rotate 1,
     apply rat.add_le_add,
     rotate 1,
-    apply HN'',
+    apply HN (max (pceil ((1+1)/ε)) N) !max_right,
     rotate_right 1,
     apply neg_le_neg,
     apply inv_ge_of_le,
@@ -161,9 +113,7 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
 
 theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos s) : pos t :=
   begin
-    rewrite [↑pos at *],
+    cases (bdd_away_of_pos Hs Hp) with [N, HN],
-    apply exists.elim (bdd_away_of_pos Hs Hp),
-    intro N HN,
     existsi 2 * 2 * N,
     apply lt_of_lt_of_le,
     rotate 1,
@@ -172,7 +122,7 @@ theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos
     have Hs4 : N⁻¹ ≤ s (2 * 2 * N), from HN _ (!mul_le_mul_left),
     apply lt_of_lt_of_le,
     rotate 1,
-    apply iff.mpr (rat.add_le_add_right_iff _ _ _),
+    apply iff.mpr !rat.add_le_add_right_iff,
     apply Hs4,
     rewrite [*pnat.mul.assoc, pnat.add_halves, -(add_halves N), rat.add_sub_cancel],
     apply inv_two_mul_lt_inv
@@ -185,9 +135,7 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
     apply nonneg_of_bdd_within,
     apply Ht,
     intros,
-    let Bd := (bdd_within_of_nonneg Hs Hp) (2 * 2 * n),
+    cases bdd_within_of_nonneg Hs Hp (2 * 2 * n) with [Ns, HNs],
-    apply exists.elim Bd,
-    intro Ns HNs,
     existsi max Ns (2 * 2 * n),
     intro m Hm,
     apply le.trans,
@@ -226,7 +174,6 @@ definition s_lt (a b : seq) := pos (sadd b (sneg a))
 
 theorem zero_nonneg : nonneg zero :=
   begin
-    rewrite ↑[nonneg, zero],
     intros,
     apply neg_nonpos_of_nonneg,
     apply le_of_lt,
@@ -257,9 +204,7 @@ theorem s_nonneg_of_pos {s : seq} (Hs : regular s) (H : pos s) : nonneg s :=
     apply nonneg_of_bdd_within,
     apply Hs,
     intros,
-    let Bt := bdd_away_of_pos Hs H,
+    cases bdd_away_of_pos Hs H with [N, HN],
-    apply exists.elim Bt,
-    intro N HN,
     existsi N,
     intro m Hm,
     apply le.trans,
@@ -354,7 +299,6 @@ theorem s_add_lt_add_left {s t : seq} (Hs : regular s) (Ht : regular t) (Hst : s
 
 theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) : nonneg (sadd s t) :=
   begin
-    rewrite [↑nonneg at *, ↑sadd],
     intros,
     rewrite [-pnat.add_halves, neg_add],
     apply add_le_add,
@@ -418,14 +362,14 @@ theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s
     apply le_of_neg_le_neg,
     rewrite [2 neg_add, neg_neg],
     apply rat.le.trans,
-    apply helper_1,
+    apply rat.neg_add_neg_le_neg_of_pos,
     apply inv_pos,
     rewrite add.comm,
     apply Lst,
     apply le_of_neg_le_neg,
     rewrite [neg_add, neg_neg],
     apply rat.le.trans,
-    apply helper_1,
+    apply rat.neg_add_neg_le_neg_of_pos,
     apply inv_pos,
     apply Lts,
     repeat assumption
@@ -438,10 +382,8 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
         s_le s t ∧ sep s t :=
   begin
     apply and.intro,
-    rewrite [↑s_lt at *, ↑pos at *, ↑s_le, ↑nonneg],
     intros,
-    apply exists.elim Lst,
+    cases Lst with [N, HN],
-    intro N HN,
     let Rns := reg_neg_reg Hs,
     let Rtns := reg_add_reg Ht Rns,
     let Habs := ge_sub_of_abs_sub_le_right (Rtns N n),
@@ -455,7 +397,6 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
                        apply HN
                      end
       ... = -n⁻¹ : by rewrite zero_sub),
-    rewrite ↑sep,
     exact or.inl Lst
   end
 
@@ -463,16 +404,13 @@ theorem lt_of_le_and_sep {s t : seq} (Hs : regular s) (Ht : regular t) (H : s_le
         s_lt s t :=
   begin
     let Le := and.left H,
-    let Hsep := and.right H,
+    cases and.right H with [P, Hlt],
-    rewrite [↑sep at Hsep],
+    exact P,
-    apply or.elim Hsep,
-    intro P, exact P,
-    intro Hlt,
     rewrite [↑s_le at Le, ↑nonneg at Le, ↑s_lt at Hlt, ↑pos at Hlt],
     apply exists.elim Hlt,
     intro N HN,
     let LeN := Le N,
-    let HN' := (iff.mpr (neg_lt_neg_iff_lt _ _)) HN,
+    let HN' := (iff.mpr !neg_lt_neg_iff_lt) HN,
     rewrite [↑sadd at HN', ↑sneg at HN', neg_add at HN', neg_neg at HN', add.comm at HN'],
     let HN'' := not_le_of_gt HN',
     apply absurd LeN HN''
@@ -545,10 +483,8 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
         (Hpt : pos t) : pos (smul s t) :=
   begin
     rewrite [↑pos at *],
-    apply exists.elim (bdd_away_of_pos Hs Hps),
+    cases bdd_away_of_pos Hs Hps with [Ns, HNs],
-    intros Ns HNs,
+    cases bdd_away_of_pos Ht Hpt with [Nt, HNt],
-    apply exists.elim (bdd_away_of_pos Ht Hpt),
-    intros Nt HNt,
     existsi 2 * max Ns Nt * max Ns Nt,
     rewrite ↑smul,
     apply lt_of_lt_of_le,
@@ -726,8 +662,6 @@ theorem s_mul_ge_zero_of_ge_zero {s t : seq} (Hs : regular s) (Ht : regular t)
     apply reg_mul_reg Hs Ht
   end
 
-
-
 theorem not_lt_self (s : seq) : ¬ s_lt s s :=
   begin
     intro Hlt,
@@ -743,7 +677,7 @@ theorem not_sep_self (s : seq) : ¬ s ≢ s :=
   begin
     intro Hsep,
     rewrite ↑sep at Hsep,
-    let Hsep' := (iff.mp (!or_self)) Hsep,
+    let Hsep' := (iff.mp !or_self) Hsep,
     apply absurd Hsep' (!not_lt_self)
   end
 
@@ -843,13 +777,11 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
     let Runt := reg_add_reg Hu (reg_neg_reg Ht),
     have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
       intro m,
-      rewrite [↑sadd, ↑sneg, -rewrite_helper8]
+      rewrite [↑sadd, ↑sneg, -sub_eq_sub_add_sub]
     end,
     rewrite [↑s_lt at *, ↑s_le at *],
-    apply exists.elim (bdd_away_of_pos Rtns Hst),
+    cases bdd_away_of_pos Rtns Hst with [Nt, HNt],
-    intro Nt HNt,
+    cases bdd_within_of_nonneg Runt Htu (2 * Nt) with [Nu, HNu],
-    apply exists.elim (bdd_within_of_nonneg Runt Htu (2 * Nt)),
-    intro Nu HNu,
     apply pos_of_bdd_away,
     existsi max (2 * Nt) Nu,
     intro n Hn,
@@ -883,13 +815,11 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
     let Runt := reg_add_reg Hu (reg_neg_reg Ht),
     have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
       intro m,
-      rewrite [↑sadd, ↑sneg, -rewrite_helper8]
+      rewrite [↑sadd, ↑sneg, -sub_eq_sub_add_sub]
     end,
     rewrite [↑s_lt at *, ↑s_le at *],
-    apply exists.elim (bdd_away_of_pos Runt Htu),
+    cases bdd_away_of_pos Runt Htu with [Nu, HNu],
-    intro Nu HNu,
+    cases bdd_within_of_nonneg Rtns Hst (2 * Nu) with [Nt, HNt],
-    apply exists.elim (bdd_within_of_nonneg Rtns Hst (2 * Nu)),
-    intro Nt HNt,
     apply pos_of_bdd_away,
     existsi max (2 * Nu) Nt,
     intro n Hn,
@@ -918,19 +848,11 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
 
 theorem le_of_le_reprs {s t : seq} (Hs : regular s) (Ht : regular t)
         (Hle : ∀ n : ℕ+, s_le s (const (t n))) : s_le s t :=
-  begin
+  by intro m; apply Hle (2 * m) m
-    rewrite [↑s_le, ↑nonneg],
-    intro m,
-    apply Hle (2 * m) m
-  end
 
 theorem le_of_reprs_le {s t : seq} (Hs : regular s) (Ht : regular t)
         (Hle : ∀ n : ℕ+, s_le (const (t n)) s) : s_le t s :=
-  begin
+  by intro m; apply Hle (2 * m) m
-    rewrite [↑s_le, ↑nonneg],
-    intro m,
-    apply Hle (2 * m) m
-  end
 
 -----------------------------
 -- of_rat theorems