chore(library/init/*): a few small improvements

library/init/algebra/field.lean

@@ -86,9 +86,17 @@ assume : 1 / a = 0,
 have 0 = (1:α), from eq.symm (by rw [← mul_one_div_cancel h, this, mul_zero]),
 absurd this zero_ne_one
 
+lemma ne_zero_of_one_div_ne_zero {a : α} (h : 1 / a ≠ 0) : a ≠ 0 :=
+assume ha : a = 0, begin rw [ha, div_zero] at h, contradiction end
+
 lemma inv_ne_zero {a : α} (h : a ≠ 0) : a⁻¹ ≠ 0 :=
 by rw inv_eq_one_div; exact one_div_ne_zero h
 
+lemma eq_zero_of_one_div_eq_zero {a : α} (h : 1 / a = 0) : a = 0 :=
+classical.by_cases
+  (assume ha, ha)
+  (assume ha, false.elim ((one_div_ne_zero ha) h))
+
 lemma one_inv_eq : 1⁻¹ = (1:α) :=
 calc 1⁻¹ = 1 * 1⁻¹ : by rw [one_mul]
      ... = (1:α)   : by simp
@@ -101,7 +109,7 @@ by simp
 lemma zero_div (a : α) : 0 / a = 0 :=
 by simp
 
--- note: integral domain has a "mul_ne_zero". α commutative division ring is an integral
+-- note: integral domain has a "mul_ne_zero". a commutative division ring is an integral
 -- domain, but let's not define that class for now.
 lemma division_ring.mul_ne_zero {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=
 assume : a * b = 0,
@@ -169,7 +177,7 @@ match classical.em (a = 0) with
 | or.inr h := eq.symm (eq_one_div_of_mul_eq_one_left (mul_one_div_cancel h))
 end
 
-lemma inv_inv' {a : α} : a⁻¹⁻¹ = a :=
+lemma inv_inv' (a : α) : a⁻¹⁻¹ = a :=
 by rw [inv_eq_one_div, inv_eq_one_div, one_div_one_div]
 
 lemma eq_of_one_div_eq_one_div {a b : α} (h : 1 / a = 1 / b) : a = b :=
@@ -185,12 +193,26 @@ lemma one_div_div (a b : α) : 1 / (a / b) = b / a :=
 by rw [one_div_eq_inv, division_def, mul_inv',
        inv_inv', division_def]
 
+lemma div_helper {a : α} (b : α) (h : a ≠ 0) : (1 / (a * b)) * a = 1 / b :=
+by simp only [division_def, mul_inv', one_mul, mul_assoc, inv_mul_cancel h, mul_one]
+
 lemma mul_div_cancel (a : α) {b : α} (hb : b ≠ 0) : a * b / b = a :=
 by simp [hb]
 
 lemma div_mul_cancel (a : α) {b : α} (hb : b ≠ 0) : a / b * b = a :=
 by simp [hb]
 
+lemma div_div_eq_mul_div (a b c : α) :
+      a / (b / c) = (a * c) / b :=
+by rw [div_eq_mul_one_div, one_div_div, ← mul_div_assoc]
+
+lemma div_mul_left {a b : α} (hb : b ≠ 0) : b / (a * b) = 1 / a :=
+by simp only [division_def, mul_inv', ← mul_assoc, mul_inv_cancel hb]
+
+lemma mul_div_mul_right (a : α) (b : α) {c : α} (hc : c ≠ 0) :
+      (a * c) / (b * c) = a / b :=
+by rw [mul_div_assoc, div_mul_left hc, ← mul_div_assoc, mul_one]
+
 lemma div_add_div_same (a b c : α) : a / c + b / c = (a + b) / c :=
 eq.symm $ right_distrib a b (c⁻¹)
 
@@ -236,6 +258,12 @@ have (a + b / c) * c = a * c + b, by rw [right_distrib, (div_mul_cancel _ hc)],
 lemma mul_mul_div (a : α) {c : α} (hc : c ≠ 0) : a = a * c * (1 / c) :=
 by simp [hc]
 
+lemma eq_of_mul_eq_mul_of_nonzero_left {a b c : α} (h : a ≠ 0) (h₂ : a * b = a * c) : b = c :=
+by rw [← one_mul b, ← inv_mul_cancel h, mul_assoc, h₂, ← mul_assoc, inv_mul_cancel h, one_mul]
+
+lemma eq_of_mul_eq_mul_of_nonzero_right {a b c : α} (h : c ≠ 0) (h2 : a * c = b * c) : a = b :=
+by rw [← mul_one a, ← mul_inv_cancel h, ← mul_assoc, h2, mul_assoc, mul_inv_cancel h, mul_one]
+
 end division_ring
 
 class field (α : Type u) extends comm_ring α, has_inv α, zero_ne_one_class α :=
@@ -254,13 +282,7 @@ lemma one_div_mul_one_div (a b : α) : (1 / a) * (1 / b) =  1 / (a * b) :=
 by rw [division_ring.one_div_mul_one_div, mul_comm b]
 
 lemma div_mul_right {a : α} (b : α) (ha : a ≠ 0) : a / (a * b) = 1 / b :=
-eq.symm (calc
-    1 / b = a * ((1 / a) * (1 / b)) : by rw [← mul_assoc, mul_one_div_cancel ha, one_mul]
-      ... = a * (1 / (b * a))       : by rw division_ring.one_div_mul_one_div
-      ... = a * (a * b)⁻¹           : by rw [inv_eq_one_div, mul_comm a b])
-
-lemma div_mul_left {a b : α} (hb : b ≠ 0) : b / (a * b) = 1 / a :=
-by rw [mul_comm a, div_mul_right _ hb]
+by rw [mul_comm, div_mul_left ha]
 
 lemma mul_div_cancel_left {a : α} (b : α) (ha : a ≠ 0) : a * b / a = b :=
 by rw [mul_comm a, (mul_div_cancel _ ha)]
@@ -282,10 +304,6 @@ lemma mul_div_mul_left (a b : α) {c : α} (hc : c ≠ 0) :
       (c * a) / (c * b) = a / b :=
 by rw [← div_mul_div, div_self hc, one_mul]
 
-lemma mul_div_mul_right (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) :
-      (a * c) / (b * c) = a / b :=
-by rw [mul_comm a, mul_comm b, mul_div_mul_left _ _ hc]
-
 lemma div_mul_eq_mul_div (a b c : α) : (b / c) * a = (b * a) / c :=
 by simp [division_def]
 
@@ -296,7 +314,7 @@ by rw [div_mul_eq_mul_div, ← one_mul c, ← div_mul_div,
 
 lemma div_add_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) :
       (a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) :=
-by rw [← mul_div_mul_right _ hb hd, ← mul_div_mul_left c d hb, div_add_div_same]
+by rw [← mul_div_mul_right _ b hd, ← mul_div_mul_left c d hb, div_add_div_same]
 
 lemma div_sub_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) :
       (a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) :=
@@ -311,10 +329,6 @@ lemma mul_eq_mul_of_div_eq_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0
 by rw [← mul_one (a*d), mul_assoc, mul_comm d, ← mul_assoc, ← div_self hb,
        ← div_mul_eq_mul_div_comm, h, div_mul_eq_mul_div, div_mul_cancel _ hd]
 
-lemma div_div_eq_mul_div (a b c : α) :
-      a / (b / c) = (a * c) / b :=
-by rw [div_eq_mul_one_div, one_div_div, ← mul_div_assoc]
-
 lemma div_div_eq_div_mul (a b c : α) :
       (a / b) / c = a / (b * c) :=
 by rw [div_eq_mul_one_div, div_mul_div, mul_one]
@@ -328,21 +342,4 @@ lemma div_mul_eq_div_mul_one_div (a b c : α) :
       a / (b * c) = (a / b) * (1 / c) :=
 by rw [← div_div_eq_div_mul, ← div_eq_mul_one_div]
 
-lemma eq_of_mul_eq_mul_of_nonzero_left {a b c : α} (h : a ≠ 0) (h₂ : a * b = a * c) : b = c :=
-by rw [← one_mul b, ← div_self h, div_mul_eq_mul_div, h₂, mul_div_cancel_left _ h]
-
-lemma eq_of_mul_eq_mul_of_nonzero_right {a b c : α} (h : c ≠ 0) (h2 : a * c = b * c) : a = b :=
-by rw [← mul_one a, ← div_self h, ← mul_div_assoc, h2, mul_div_cancel _ h]
-
-lemma ne_zero_of_one_div_ne_zero {a : α} (h : 1 / a ≠ 0) : a ≠ 0 :=
-assume ha : a = 0, begin rw [ha, div_zero] at h, contradiction end
-
-lemma eq_zero_of_one_div_eq_zero {a : α} (h : 1 / a = 0) : a = 0 :=
-classical.by_cases
-  (assume ha, ha)
-  (assume ha, false.elim ((one_div_ne_zero ha) h))
-
-lemma div_helper {a : α} (b : α) (h : a ≠ 0) : (1 / (a * b)) * a = 1 / b :=
-by rw [div_mul_eq_mul_div, one_mul, div_mul_right _ h]
-
 end field

library/init/algebra/ordered_field.lean

@@ -30,9 +30,15 @@ calc  a * 0 = 0           : by rw mul_zero
 lemma one_div_pos_of_pos {a : α} (h : 0 < a) : 0 < 1 / a :=
 lt_of_mul_lt_mul_left (mul_zero_lt_mul_inv_of_pos h) (le_of_lt h)
 
+lemma pos_of_one_div_pos {a : α} (h : 0 < 1 / a) : 0 < a :=
+one_div_one_div a ▸ one_div_pos_of_pos h
+
 lemma one_div_neg_of_neg {a : α} (h : a < 0) : 1 / a < 0 :=
 gt_of_mul_lt_mul_neg_left (mul_zero_lt_mul_inv_of_neg h) (le_of_lt h)
 
+lemma neg_of_one_div_neg {a : α} (h : 1 / a < 0) : a < 0 :=
+one_div_one_div a ▸ one_div_neg_of_neg h
+
 lemma le_mul_of_ge_one_right {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ b * a :=
 suffices b * 1 ≤ b * a, by rwa mul_one at this,
 mul_le_mul_of_nonneg_left h hb
@@ -267,19 +273,8 @@ begin
   exact mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc))
 end
 
-lemma two_pos : (2:α) > 0 :=
-begin unfold bit0, exact add_pos zero_lt_one zero_lt_one end
-
-lemma two_ne_zero : (2:α) ≠ 0 :=
-ne.symm (ne_of_lt two_pos)
-
 lemma add_halves (a : α) : a / 2 + a / 2 = a :=
-calc
-   a / 2 + a / 2 = (a + a) / 2 : by rw div_add_div_same
-    ... = (a * 1 + a * 1) / 2   : by rw mul_one
-    ... = (a * (1 + 1)) / 2     : by rw left_distrib
-    ... = (a * 2) / 2           : by rw one_add_one_eq_two
-    ... = a                     : by rw [@mul_div_cancel α _ _ _ two_ne_zero]
+by { rw [div_add_div_same, ← two_mul, mul_div_cancel_left], exact two_ne_zero }
 
 lemma sub_self_div_two (a : α) : a - a / 2 = a / 2 :=
 suffices a / 2 + a / 2 - a / 2 = a / 2, by rwa add_halves at this,
@@ -302,17 +297,6 @@ eq.symm
   (iff.mpr (eq_div_iff_mul_eq _ _ (ne_of_gt (add_pos (@zero_lt_one α _) zero_lt_one)))
            (begin unfold bit0, rw [left_distrib, mul_one] end))
 
-lemma two_gt_one : (2:α) > 1 :=
-calc (2:α) = 1+1 : one_add_one_eq_two
-     ...   > 1+0 : add_lt_add_left zero_lt_one _
-     ...   = 1   : add_zero 1
-
-lemma two_ge_one : (2:α) ≥ 1 :=
-le_of_lt two_gt_one
-
-lemma four_pos : (4:α) > 0 :=
-add_pos two_pos two_pos
-
 lemma mul_le_mul_of_mul_div_le {a b c d : α} (h : a * (b / c) ≤ d) (hc : c > 0) : b * a ≤ d * c :=
 begin
   rw [← mul_div_assoc] at h, rw [mul_comm b],
@@ -442,31 +426,6 @@ begin
   apply one_div_lt_one_div_of_lt; assumption,
 end
 
-end linear_ordered_field
-
-class discrete_linear_ordered_field (α : Type u) extends linear_ordered_field α,
-      decidable_linear_ordered_comm_ring α
-
-section discrete_linear_ordered_field
-variables {α : Type u}
-
-variables [discrete_linear_ordered_field α]
-
-lemma pos_of_one_div_pos {a : α} (h : 0 < 1 / a) : 0 < a :=
- have h1 : 0 < 1 / (1 / a), from one_div_pos_of_pos h,
- have h2 : 1 / a ≠ 0, from
-   (assume h3 : 1 / a = 0,
-    have h4 : 1 / (1 / a) = 0, from eq.symm h3 ▸ div_zero 1,
-    absurd h4 (ne.symm (ne_of_lt h1))),
- (one_div_one_div a) ▸ h1
-
-lemma neg_of_one_div_neg {a : α} (h : 1 / a < 0) : a < 0 :=
-have h1 : 0 < - (1 / a), from neg_pos_of_neg h,
-have ha : a ≠ 0, from ne_zero_of_one_div_ne_zero (ne_of_lt h),
-have h2 : 0 < 1 / (-a), from eq.symm (one_div_neg_eq_neg_one_div a) ▸ h1,
-have h3 : 0 < -a, from pos_of_one_div_pos h2,
-neg_of_neg_pos h3
-
 lemma div_mul_le_div_mul_of_div_le_div_pos' {a b c d e : α} (h : a / b ≤ c / d)
           (he : e > 0) : a / (b * e) ≤ c / (d * e) :=
 begin
@@ -476,4 +435,7 @@ begin
   apply one_div_pos_of_pos he
 end
 
-end discrete_linear_ordered_field
+end linear_ordered_field
+
+class discrete_linear_ordered_field (α : Type u) extends linear_ordered_field α,
+      decidable_linear_ordered_comm_ring α

library/init/algebra/ordered_ring.lean

@@ -98,6 +98,22 @@ linear_ordered_semiring.zero_lt_one α
 lemma zero_le_one : 0 ≤ (1:α) :=
 le_of_lt zero_lt_one
 
+lemma two_pos : 0 < (2:α) := add_pos zero_lt_one zero_lt_one
+
+lemma two_ne_zero : (2:α) ≠ 0 :=
+ne.symm (ne_of_lt two_pos)
+
+lemma two_gt_one : (2:α) > 1 :=
+calc (2:α) = 1+1 : one_add_one_eq_two
+     ...   > 1+0 : add_lt_add_left zero_lt_one _
+     ...   = 1   : add_zero 1
+
+lemma two_ge_one : (2:α) ≥ 1 :=
+le_of_lt two_gt_one
+
+lemma four_pos : (4:α) > 0 :=
+add_pos two_pos two_pos
+
 lemma lt_of_mul_lt_mul_left {a b c : α} (h : c * a < c * b) (hc : c ≥ 0) : a < b :=
 lt_of_not_ge
   (assume h1 : b ≤ a,

library/init/data/prod.lean

@@ -43,5 +43,5 @@ rfl
 end
 
 def {u₁ u₂ v₁ v₂} prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
-  (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
-| (a, b) := (f a, g b)
+  (f : α₁ → α₂) (g : β₁ → β₂) (x : α₁ × β₁) : α₂ × β₂ :=
+(f x.1, g x.2)

library/init/function.lean

@@ -130,7 +130,7 @@ variables {α : Type u₁} {β : Type u₂} {φ : Type u₃}
 λ f a b, f (a, b)
 
 @[inline] def uncurry : (α → β → φ) → α × β → φ :=
-λ f ⟨a, b⟩, f a b
+λ f a, f a.1 a.2
 
 @[simp] lemma curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
 rfl

library/init/logic.lean

@@ -770,18 +770,14 @@ end
 class inhabited (α : Sort u) :=
 (default : α)
 
-def default (α : Sort u) [inhabited α] : α :=
-inhabited.default α
+export inhabited (default)
 
 @[inline, irreducible] def arbitrary (α : Sort u) [inhabited α] : α :=
 default α
 
 instance prop.inhabited : inhabited Prop :=
 ⟨true⟩
 
-instance fun.inhabited (α : Sort u) {β : Sort v} [h : inhabited β] : inhabited (α → β) :=
-inhabited.rec_on h (λ b, ⟨λ a, b⟩)
-
 instance pi.inhabited (α : Sort u) {β : α → Sort v} [Π x, inhabited (β x)] : inhabited (Π x, β x) :=
 ⟨λ a, default (β a)⟩