feat(data/num,data/nat/cast,...): nat,num,int,rat.cast, list stuff

algebra/field.lean

@@ -15,6 +15,14 @@ variables [division_ring α] {a b : α}
 lemma division_ring.neg_inv (h : a ≠ 0) : - a⁻¹ = (- a)⁻¹ :=
 by rwa [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
 
+lemma inv_comm_of_comm {a b : α} (h : a ≠ 0) (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,
+  rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one,
+       ← mul_assoc, inv_mul_cancel, one_mul] at this; exact h
+end
+
 end division_ring
 
 section

algebra/group.lean

@@ -51,16 +51,22 @@ section group
   theorem mul_eq_one_iff_inv_eq : a * b = 1 ↔ a⁻¹ = b :=
   by rw [mul_eq_one_iff_eq_inv, eq_inv_iff_eq_inv, eq_comm]
 
-  @[simp] theorem eq_mul_inv_iff_mul_eq : a = b * c⁻¹ ↔ a * c = b :=
+  theorem eq_inv_iff_mul_eq_one : a = b⁻¹ ↔ a * b = 1 :=
+  mul_eq_one_iff_eq_inv.symm
+
+  theorem inv_eq_iff_mul_eq_one : a⁻¹ = b ↔ a * b = 1 :=
+  mul_eq_one_iff_inv_eq.symm
+
+  theorem eq_mul_inv_iff_mul_eq : a = b * c⁻¹ ↔ a * c = b :=
   ⟨λ h, by simp [h], λ h, by simp [h.symm]⟩
 
-  @[simp] theorem eq_inv_mul_iff_mul_eq : a = b⁻¹ * c ↔ b * a = c :=
+  theorem eq_inv_mul_iff_mul_eq : a = b⁻¹ * c ↔ b * a = c :=
   ⟨λ h, by simp [h], λ h, by simp [h.symm]⟩
 
-  @[simp] theorem inv_mul_eq_iff_eq_mul : a⁻¹ * b = c ↔ b = a * c :=
+  theorem inv_mul_eq_iff_eq_mul : a⁻¹ * b = c ↔ b = a * c :=
   ⟨λ h, by simp [h.symm], λ h, by simp [h]⟩
 
-  @[simp] theorem mul_inv_eq_iff_eq_mul : a * b⁻¹ = c ↔ a = c * b :=
+  theorem mul_inv_eq_iff_eq_mul : a * b⁻¹ = c ↔ a = c * b :=
   ⟨λ h, by simp [h.symm], λ h, by simp [h]⟩
 
   theorem mul_inv_eq_one {a b : α} : a * b⁻¹ = 1 ↔ a = b :=
@@ -107,6 +113,8 @@ run_cmd transport_multiplicative_to_additive [
   (`inv_eq_iff_inv_eq, `neg_eq_iff_neg_eq),
   (`mul_eq_one_iff_eq_inv, `add_eq_zero_iff_eq_neg),
   (`mul_eq_one_iff_inv_eq, `add_eq_zero_iff_neg_eq),
+  (`eq_inv_iff_mul_eq_one, `eq_neg_iff_add_eq_zero),
+  (`inv_eq_iff_mul_eq_one, `neg_eq_iff_add_eq_zero),
   (`eq_mul_inv_iff_mul_eq, `eq_add_neg_iff_add_eq),
   (`eq_inv_mul_iff_mul_eq, `eq_neg_add_iff_add_eq),
   (`inv_mul_eq_iff_eq_mul, `neg_add_eq_iff_eq_add),
@@ -136,11 +144,11 @@ section add_group
   theorem sub_ne_zero : a - b ≠ 0 ↔ a ≠ b :=
   not_congr sub_eq_zero
 
-  @[simp] theorem eq_sub_iff_add_eq : a = b - c ↔ a + c = b :=
-  by split; intro h; simp [h]
+  theorem eq_sub_iff_add_eq : a = b - c ↔ a + c = b :=
+  by split; intro h; simp [h, eq_add_neg_iff_add_eq]
 
   theorem sub_eq_iff_eq_add : a - b = c ↔ a = c + b :=
-  by split; intro h; simp * at *
+  by split; intro h; simp [*, add_neg_eq_iff_eq_add] at *
 
   theorem eq_iff_eq_of_sub_eq_sub {a b c d : α} (H : a - b = c - d) : a = b ↔ c = d :=
   by rw [← sub_eq_zero, H, sub_eq_zero]

algebra/group_power.lean

@@ -73,6 +73,9 @@ by rw [←pow_add, ←pow_add, add_comm]
 
 end monoid
 
+theorem nat.pow_eq_pow_nat (p q : ℕ) : nat.pow p q = pow_nat p q :=
+by induction q; [refl, simp [nat.pow_succ, pow_succ, *]]
+
 /- commutative monoid -/
 
 section comm_monoid

algebra/ordered_ring.lean

@@ -50,6 +50,9 @@ lemma le_mul_of_ge_one_left' {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ a *
 suffices 1 * b ≤ a * b, by rwa one_mul at this,
 mul_le_mul_of_nonneg_right h hb
 
+theorem mul_nonneg_iff_right_nonneg_of_pos {a b : α} (h : 0 < a) : 0 ≤ b * a ↔ 0 ≤ b :=
+⟨assume : 0 ≤ b * a, nonneg_of_mul_nonneg_right this h, assume : 0 ≤ b, mul_nonneg this $ le_of_lt h⟩
+
 /- remove when we have a linear arithmetic tactic -/
 lemma one_lt_two : 1 < (2 : α) :=
 calc (1:α) < 1 + 1 : lt_add_of_le_of_pos (le_refl 1) zero_lt_one

analysis/limits.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 A collection of limit properties.
 -/
 import algebra.big_operators algebra.group_power
-  analysis.metric_space analysis.of_nat analysis.topology.infinite_sum
+  analysis.metric_space analysis.topology.infinite_sum
 noncomputable theory
 open classical set finset function filter
 local attribute [instance] decidable_inhabited prop_decidable
@@ -70,25 +70,25 @@ lemma is_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} {r : ℝ} (hf : ∀n, 0
 
 end real
 
-lemma mul_add_one_le_pow {r : ℝ} (hr : 0 ≤ r) : ∀{n}, (of_nat n) * r + 1 ≤ (r + 1) ^ n
+lemma mul_add_one_le_pow {r : ℝ} (hr : 0 ≤ r) : ∀{n:ℕ}, (n:ℝ) * r + 1 ≤ (r + 1) ^ n
 | 0       := by simp; exact le_refl 1
 | (n + 1) :=
-  let h : of_nat n ≥ (0 : ℝ) := @zero_le_of_nat ℝ _ n in
-  calc of_nat (n + 1) * r + 1 ≤ (of_nat (n + 1) * r + 1) + r * r * of_nat n :
+  let h : (n:ℝ) ≥ 0 := nat.cast_nonneg n in
+  calc ↑(n + 1) * r + 1 ≤ ((n + 1) * r + 1) + r * r * n :
       le_add_of_le_of_nonneg (le_refl _) (mul_nonneg (mul_nonneg hr hr) h)
-    ... = (r + 1) * (of_nat n * r + 1) : by simp [mul_add, add_mul]
+    ... = (r + 1) * (n * r + 1) : by simp [mul_add, add_mul]
     ... ≤ (r + 1) * (r + 1) ^ n : mul_le_mul (le_refl _) mul_add_one_le_pow
       (add_nonneg (mul_nonneg h hr) zero_le_one) (add_nonneg hr zero_le_one)
 
 lemma tendsto_pow_at_top_at_top_of_gt_1 {r : ℝ} (h : r > 1) : tendsto (λn:ℕ, r ^ n) at_top at_top :=
 tendsto_infi $ assume p, tendsto_principal $
-  let ⟨n, hn⟩ := @exists_lt_of_nat (p / (r - 1)) in
-  have hn_nn : (0:ℝ) ≤ of_nat n, from (@zero_le_of_nat ℝ _ n),
+  let ⟨n, hn⟩ := @exists_lt_nat (p / (r - 1)) in
+  have hn_nn : (0:ℝ) ≤ n, from nat.cast_nonneg n,
   have r - 1 > 0, from sub_lt_iff.mp $ by simp; assumption,
   have p ≤ r ^ n,
     from calc p = (p / (r - 1)) * (r - 1) : (div_mul_cancel _ $ ne_of_gt this).symm
-      ... ≤ of_nat n * (r - 1) : mul_le_mul (le_of_lt hn) (le_refl _) (le_of_lt this) hn_nn
-      ... ≤ of_nat n * (r - 1) + 1 : le_add_of_le_of_nonneg (le_refl _) zero_le_one
+      ... ≤ n * (r - 1) : mul_le_mul (le_of_lt hn) (le_refl _) (le_of_lt this) hn_nn
+      ... ≤ n * (r - 1) + 1 : le_add_of_le_of_nonneg (le_refl _) zero_le_one
       ... ≤ ((r - 1) + 1) ^ n : mul_add_one_le_pow $ le_of_lt this
       ... ≤ r ^ n : by simp; exact le_refl _,
   show {n | p ≤ r ^ n} ∈ at_top.sets,

analysis/measure_theory/lebesgue_measure.lean

@@ -175,15 +175,10 @@ lebesgue_outer.to_measure $
     ... ≤ lebesgue_outer.caratheodory :
       measurable_space.generate_from_le $ by simp [lebesgue_outer_is_measurable_Iio] {contextual := tt}
 
-lemma tendsto_of_nat_at_top_at_top : tendsto (of_nat : ℕ → ℝ) at_top at_top :=
+lemma tendsto_of_nat_at_top_at_top : tendsto (coe : ℕ → ℝ) at_top at_top :=
 tendsto_infi $ assume r, tendsto_principal $
-  let ⟨q, hq⟩ := exists_lt_of_rat r in
-  show {n : ℕ | r ≤ of_nat n} ∈ at_top.sets,
-    from mem_at_top_iff.mpr ⟨rat.nat_ceil q, assume b (hb : rat.nat_ceil q ≤ b),
-      calc r ≤ of_rat q : le_of_lt hq
-        ... ≤ of_rat (rat.nat_ceil q) : of_rat_le_of_rat.mpr (rat.le_nat_ceil q)
-        ... = of_nat (rat.nat_ceil q) : by rw [rat_coe_eq_of_nat, real_of_rat_of_nat_eq_of_nat]
-        ... ≤ of_nat b : of_nat_le_of_nat hb⟩
+let ⟨n, hn⟩ := exists_lt_nat r in
+mem_at_top_iff.2 ⟨n, λ m h, le_trans (le_of_lt hn) (nat.cast_le.2 h)⟩
 
 lemma lebesgue_Ico {a b : ℝ} : lebesgue.measure (Ico a b) = of_real (b - a) :=
 match le_total a b with
@@ -203,22 +198,22 @@ lemma lebesgue_Ioo {a b : ℝ} : lebesgue.measure (Ioo a b) = of_real (b - a) :=
 by_cases (assume h : b ≤ a, by simp [h, -sub_eq_add_neg, ennreal.of_real_of_nonpos]) $
 assume : ¬ b ≤ a,
 have h : a < b, from not_le_iff.mp this,
-let s := λn:ℕ, a + (b - a) * (of_nat (n + 1))⁻¹ in
+let s := λn:ℕ, a + (b - a) * (↑(n + 1))⁻¹ in
 have tendsto s at_top (nhds (a + (b - a) * 0)),
   from tendsto_add tendsto_const_nhds $ tendsto_mul tendsto_const_nhds $ tendsto_compose
    (tendsto_comp_succ_at_top_iff.mpr tendsto_of_nat_at_top_at_top) tendsto_inverse_at_top_nhds_0,
 have hs : tendsto s at_top (nhds a), by simpa,
 have hsm : ∀i j, j ≤ i → s i ≤ s j,
   from assume i j hij,
-  have h₁ : ∀j:ℕ, (0:ℝ) < of_nat (j + 1),
-    from assume j, of_nat_pos $ add_pos_of_nonneg_of_pos (nat.zero_le j) zero_lt_one,
-  have h₂ : of_nat (j + 1) ≤ (of_nat (i + 1) : ℝ), from of_nat_le_of_nat $ add_le_add hij (le_refl _),
+  have h₁ : ∀j:ℕ, (0:ℝ) < (j + 1),
+    from assume j, nat.cast_pos.2 $ add_pos_of_nonneg_of_pos (nat.zero_le j) zero_lt_one,
+  have h₂ : (↑(j + 1) : ℝ) ≤ ↑(i + 1), from nat.cast_le.2 $ add_le_add hij (le_refl _),
   add_le_add (le_refl _) $
   mul_le_mul (le_refl _) (inv_le_inv _ _ (h₁ j) h₂) (le_of_lt $ inv_pos $ h₁ i) $
     by simp [le_sub_iff_add_le, -sub_eq_add_neg, le_of_lt h],
 have has : ∀i, a < s i,
   from assume i,
-  have (0:ℝ) < of_nat (i + 1), from of_nat_pos $ lt_add_of_le_of_pos (nat.zero_le _) zero_lt_one,
+  have (0:ℝ) < ↑(i + 1), from nat.cast_pos.2 $ lt_add_of_le_of_pos (nat.zero_le _) zero_lt_one,
   (lt_add_iff_pos_right _).mpr $ mul_pos
     (by simp [-sub_eq_add_neg, sub_lt_iff, (>), ‹a < b›]) (inv_pos this),
 have eq₁ : Ioo a b = (⋃n, Ico (s n) b),

analysis/metric_space.lean

@@ -96,7 +96,7 @@ instance : metric_space ℝ :=
 { real.uniform_space with
   dist := λx y, abs (x - y),
   dist_self := by simp [abs_zero],
-  eq_of_dist_eq_zero := by simp,
+  eq_of_dist_eq_zero := by simp [add_neg_eq_zero],
   dist_comm := assume x y, by rw [abs_sub],
   dist_triangle := assume x y z, abs_sub_le _ _ _,
   uniformity_dist := le_antisymm
@@ -134,7 +134,7 @@ begin
   exact (tendsto_map' $ tendsto_infi $ assume ε, tendsto_infi $ assume hε,
     let ε' : subtype {r : ℝ | r > 0} := ⟨ε / 2, div_pos_of_pos_of_pos hε two_pos⟩ in
     tendsto_infi' ε' $ tendsto_infi' ε' $ tendsto_principal_principal $
-    assume ⟨⟨p₁, p₂⟩, ⟨q₁, q₂⟩⟩, by simp; exact this hε),
+    assume ⟨⟨p₁, p₂⟩, ⟨q₁, q₂⟩⟩, by simpa using this hε),
 end
 
 theorem uniform_continuous_dist [uniform_space β] {f g : β → α}
@@ -185,26 +185,22 @@ assume y, assume ymem, lt_of_lt_of_le ymem h
 theorem nhds_eq_metric : nhds x = (⨅ε:{ε:ℝ // ε>0}, principal (open_ball x ε.val)) :=
 begin
   rw [nhds_eq_uniformity, uniformity_dist', lift'_infi],
-  apply congr_arg, apply funext, intro ε,
-  rw [lift'_principal],
-  simp [open_ball, dist_comm],
-  exact monotone_preimage,
-  exact ⟨⟨1, zero_lt_one⟩⟩,
-  exact assume a b, rfl
+  { apply congr_arg, apply funext, intro ε,
+    rw [lift'_principal],
+    { simp [open_ball, dist_comm] },
+    { exact monotone_preimage } },
+  { exact ⟨⟨1, zero_lt_one⟩⟩ },
+  { intros, refl }
 end
 
 theorem mem_nhds_sets_iff_metric : s ∈ (nhds x).sets ↔ ∃ε>0, open_ball x ε ⊆ s :=
 begin
   rw [nhds_eq_metric, infi_sets_eq],
-  simp,
-  exact assume ⟨x, hx⟩ ⟨y, hy⟩, ⟨⟨min x y, lt_min hx hy⟩,
-    begin
-      simp,
-      constructor,
-      exact open_ball_subset_open_ball_of_le (min_le_left _ _),
-      exact open_ball_subset_open_ball_of_le (min_le_right _ _)
-    end⟩,
-  exact ⟨⟨1, zero_lt_one⟩⟩,
+  { simp },
+  { intros y z, cases y with y hy, cases z with z hz,
+    refine ⟨⟨min y z, lt_min hy hz⟩, _⟩,
+    simp [open_ball_subset_open_ball_of_le, min_le_left, min_le_right] },
+  { exact ⟨⟨1, zero_lt_one⟩⟩ }
 end
 
 theorem is_open_metric : is_open s ↔ (∀x∈s, ∃ε>0, open_ball x ε ⊆ s) :=