refactor(data/nat/basic): use function equality for iterate lemmas (#2748)

Author: urkud

src/algebra/group_power.lean

@@ -419,7 +419,7 @@ variable (f : R →+* R)
 
 lemma coe_pow : ∀ n : ℕ, ⇑(f^n) = (f^[n])
 | 0 := rfl
-| (n+1) := by { simp only [nat.iterate_succ', pow_succ', coe_mul, coe_pow n], refl }
+| (n+1) := by { simp only [nat.iterate_succ, pow_succ', coe_mul, coe_pow n] }
 
 lemma iterate_map_pow (a) (n m : ℕ) : f^[n] (a^m) = (f^[n] a)^m :=
 f.to_monoid_hom.iterate_map_pow a n m

src/analysis/calculus/deriv.lean

@@ -1527,8 +1527,9 @@ lemma iter_deriv_pow' {k : ℕ} :
   deriv^[k] (λx:𝕜, x^n) = λ x, ((finset.range k).prod (λ i, n - i):ℕ) * x^(n-k) :=
 begin
   induction k with k ihk,
-  { simp only [one_mul, finset.prod_range_zero, nat.iterate_zero, nat.sub_zero, nat.cast_one] },
-  { simp only [nat.iterate_succ', ihk, finset.prod_range_succ],
+  { simp only [one_mul, finset.prod_range_zero, nat.iterate_zero_apply, nat.sub_zero,
+      nat.cast_one] },
+  { simp only [nat.iterate_succ_apply', ihk, finset.prod_range_succ],
     ext x,
     rw [((has_deriv_at_pow (n - k) x).const_mul _).deriv, nat.cast_mul, mul_left_comm, mul_assoc,
       nat.succ_eq_add_one, nat.sub_sub] }
@@ -1630,7 +1631,7 @@ lemma iter_deriv_fpow {k : ℕ} (hx : x ≠ 0) :
   deriv^[k] (λx:𝕜, x^m) x = ((finset.range k).prod (λ i, m - i):ℤ) * x^(m-k) :=
 begin
   induction k with k ihk generalizing x hx,
-  { simp only [one_mul, finset.prod_range_zero, nat.iterate_zero, int.coe_nat_zero, sub_zero,
+  { simp only [one_mul, finset.prod_range_zero, nat.iterate_zero_apply, int.coe_nat_zero, sub_zero,
       int.cast_one] },
   { rw [nat.iterate_succ', finset.prod_range_succ, int.cast_mul, mul_assoc, mul_left_comm, int.coe_nat_succ,
       ← sub_sub, ← ((has_deriv_at_fpow _ hx).const_mul _).deriv],

src/analysis/normed_space/banach.lean

@@ -131,7 +131,8 @@ begin
   have hnle : ∀n:ℕ, ∥(h^[n]) y∥ ≤ (1/2)^n * ∥y∥,
   { assume n,
     induction n with n IH,
-    { simp only [one_div_eq_inv, nat.nat_zero_eq_zero, one_mul, nat.iterate_zero, pow_zero] },
+    { simp only [one_div_eq_inv, nat.nat_zero_eq_zero, one_mul, nat.iterate_zero_apply,
+        pow_zero] },
     { rw [nat.iterate_succ'],
       apply le_trans (hle _) _,
       rw [pow_succ, mul_assoc],

src/analysis/special_functions/exp_log.lean

@@ -65,7 +65,7 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 
 @[simp] lemma iter_deriv_exp : ∀ n : ℕ, (deriv^[n] exp) = exp
 | 0 := rfl
-| (n+1) := by rw [nat.iterate_succ, deriv_exp, iter_deriv_exp n]
+| (n+1) := by rw [nat.iterate_succ_apply, deriv_exp, iter_deriv_exp n]
 
 lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous
@@ -128,7 +128,7 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 
 @[simp] lemma iter_deriv_exp : ∀ n : ℕ, (deriv^[n] exp) = exp
 | 0 := rfl
-| (n+1) := by rw [nat.iterate_succ, deriv_exp, iter_deriv_exp n]
+| (n+1) := by rw [nat.iterate_succ_apply, deriv_exp, iter_deriv_exp n]
 
 lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous

src/computability/turing_machine.lean

@@ -555,10 +555,10 @@ by rintro ⟨⟩; refl
   ((tape.move dir.right)^[n] (tape.mk' L (R.modify_nth f n))) :=
 begin
   induction n with n IH generalizing L R,
-  { simp only [list_blank.nth_zero, list_blank.modify_nth, nat.iterate_zero],
+  { simp only [list_blank.nth_zero, list_blank.modify_nth, nat.iterate_zero_apply],
     rw [← tape.write_mk', list_blank.cons_head_tail] },
   simp only [list_blank.head_cons, list_blank.nth_succ, list_blank.modify_nth,
-    tape.move_right_mk', list_blank.tail_cons, nat.iterate_succ, IH]
+    tape.move_right_mk', list_blank.tail_cons, nat.iterate_succ_apply, IH]
 end
 
 theorem tape.map_move {Γ Γ'} [inhabited Γ] [inhabited Γ']
@@ -1418,7 +1418,7 @@ begin
     step_aux (stmt.move d^[i] q) v T =
     step_aux q v (tape.move d^[i] T), from this n,
   intro, induction i with i IH generalizing T, {refl},
-  rw [nat.iterate_succ', step_aux, IH, ← nat.iterate_succ]
+  rw [nat.iterate_succ', step_aux, IH, nat.iterate_succ]
 end
 
 theorem supports_stmt_move {S d q} :
@@ -1493,7 +1493,7 @@ begin
       using this (list.reverse_reverse _).symm },
   intros, induction l₁ with b l₁ IH generalizing l₂,
   { cases e, refl },
-  simp only [list.length, list.cons_append, nat.iterate_succ],
+  simp only [list.length, list.cons_append, nat.iterate_succ_apply],
   convert IH e,
   simp only [list_blank.tail_cons, list_blank.append, tape.move_left_mk', list_blank.head_cons]
 end
@@ -1507,7 +1507,7 @@ begin
     simp only [tr_tape'_move_left, list_blank.cons_head_tail,
       list_blank.head_cons, list_blank.tail_cons] },
   intros, induction i with i IH, {refl},
-  rw [nat.iterate_succ, nat.iterate_succ', tape.move_left_right, IH]
+  rw [nat.iterate_succ_apply, nat.iterate_succ_apply', tape.move_left_right, IH]
 end
 
 theorem step_aux_write (q v a b L R) :
@@ -2215,7 +2215,7 @@ begin
   case TM2to1.st_act.pop : f {
     cases e : S k,
     { simp only [tape.mk'_head, list_blank.head_cons, tape.move_left_mk',
-        list.length, tape.write_mk', list.head', nat.iterate_zero, list.tail_nil],
+        list.length, tape.write_mk', list.head', nat.iterate_zero_apply, list.tail_nil],
       rw [← e, function.update_eq_self], exact ⟨L, hL, by rw [add_bottom_head_fst, cond]⟩ },
     { refine ⟨_, λ k', _, by rw [
         list.length_cons, tape.move_right_n_head, tape.mk'_nth_nat, add_bottom_nth_succ_fst,

src/data/nat/basic.lean

@@ -977,19 +977,29 @@ by unfold bodd div2; cases bodd_div2 n; refl
 section
 variables {α : Sort*} (op : α → α)
 
-@[simp] theorem iterate_zero (a : α) : op^[0] a = a := rfl
+@[simp] theorem iterate_zero : op^[0] = id := rfl
 
-@[simp] theorem iterate_succ (n : ℕ) (a : α) : op^[succ n] a = (op^[n]) (op a) := rfl
+theorem iterate_zero_apply (x : α) : op^[0] x = x := rfl
 
-theorem iterate_add : ∀ (m n : ℕ) (a : α), op^[m + n] a = (op^[m]) (op^[n] a)
-| m 0 a := rfl
-| m (succ n) a := iterate_add m n _
+@[simp] theorem iterate_succ (n : ℕ) : op^[succ n] = (op^[n]) ∘ op := rfl
+
+theorem iterate_succ_apply (n : ℕ) (x : α) : op^[succ n] x = (op^[n]) (op x) := rfl
+
+theorem iterate_add : ∀ (m n : ℕ), op^[m + n] = (op^[m]) ∘ (op^[n])
+| m 0 := rfl
+| m (succ n) := by rw [iterate_succ, iterate_succ, iterate_add]
+
+theorem iterate_add_apply (m n : ℕ) (x : α) : op^[m + n] x = (op^[m] (op^[n] x)) :=
+by rw iterate_add
 
 @[simp] theorem iterate_one : op^[1] = op := funext $ λ a, rfl
 
-theorem iterate_succ' (n : ℕ) (a : α) : op^[succ n] a = op (op^[n] a) :=
+theorem iterate_succ' (n : ℕ) : op^[succ n] = op ∘ (op^[n]) :=
 by rw [← one_add, iterate_add, iterate_one]
 
+theorem iterate_succ_apply' (n : ℕ) (x : α) : op^[succ n] x = op (op^[n] x) :=
+by rw [iterate_succ']
+
 lemma iterate_mul (m : ℕ) : ∀ n, op^[m * n] = (op^[m]^[n])
 | 0 := by { ext a, simp only [mul_zero, iterate_zero] }
 | (n + 1) := by { ext x, simp only [mul_add, mul_one, iterate_one, iterate_add, iterate_mul n] }
@@ -1003,21 +1013,21 @@ theorem iterate_ind {α : Type u} (f : α → α) {p : (α → α) → Prop} (hf
 
 theorem iterate₀ {α : Type u} {op : α → α} {x : α} (H : op x = x) {n : ℕ} :
   op^[n] x = x :=
-by induction n; [simp only [iterate_zero], simp only [iterate_succ', H, *]]
+by induction n; [simp only [iterate_zero_apply], simp only [iterate_succ_apply', H, *]]
 
 theorem iterate₁ {α : Type u} {β : Type v} {op : α → α} {op' : β → β} {op'' : α → β}
   (H : ∀ x, op' (op'' x) = op'' (op x)) {n : ℕ} {x : α} :
   op'^[n] (op'' x) = op'' (op^[n] x) :=
-by induction n; [simp only [iterate_zero], simp only [iterate_succ', H, *]]
+by induction n; [simp only [iterate_zero_apply], simp only [iterate_succ_apply', H, *]]
 
 theorem iterate₂ {α : Type u} {op : α → α} {op' : α → α → α}
   (H : ∀ x y, op (op' x y) = op' (op x) (op y)) {n : ℕ} {x y : α} :
   op^[n] (op' x y) = op' (op^[n] x) (op^[n] y) :=
-by induction n; [simp only [iterate_zero], simp only [iterate_succ', H, *]]
+by induction n; [simp only [iterate_zero_apply], simp only [iterate_succ_apply', H, *]]
 
 theorem iterate_cancel {α : Type u} {op op' : α → α} (H : ∀ x, op (op' x) = x) {n : ℕ} {x : α} :
   op^[n] (op'^[n] x) = x :=
-by induction n; [refl, rwa [iterate_succ, iterate_succ', H]]
+by induction n; [refl, rwa [iterate_succ_apply, iterate_succ_apply', H]]
 
 end
 

src/field_theory/perfect_closure.lean

@@ -126,15 +126,15 @@ private lemma mul_aux_left (x1 x2 y : ℕ × K) (H : r K p x1 x2) :
   mk K p (x1.1 + y.1, ((frobenius K p)^[y.1] x1.2) * ((frobenius K p)^[x1.1] y.2)) =
   mk K p (x2.1 + y.1, ((frobenius K p)^[y.1] x2.2) * ((frobenius K p)^[x2.1] y.2)) :=
 match x1, x2, H with
-| _, _, r.intro n x := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
+| _, _, r.intro n x := quot.sound $ by rw [← nat.iterate_succ_apply, nat.iterate_succ',
     nat.iterate_succ', ← frobenius_mul, nat.succ_add]; apply r.intro
 end
 
 private lemma mul_aux_right (x y1 y2 : ℕ × K) (H : r K p y1 y2) :
   mk K p (x.1 + y1.1, ((frobenius K p)^[y1.1] x.2) * ((frobenius K p)^[x.1] y1.2)) =
   mk K p (x.1 + y2.1, ((frobenius K p)^[y2.1] x.2) * ((frobenius K p)^[x.1] y2.2)) :=
 match y1, y2, H with
-| _, _, r.intro n y := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
+| _, _, r.intro n y := quot.sound $ by rw [← nat.iterate_succ_apply, nat.iterate_succ',
     nat.iterate_succ', ← frobenius_mul]; apply r.intro
 end
 
@@ -153,12 +153,12 @@ instance : comm_monoid (perfect_closure K p) :=
 { mul_assoc := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
     quot.induction_on g $ λ ⟨s, z⟩, congr_arg (quot.mk _) $
     by simp only [add_assoc, mul_assoc, nat.iterate₂ (frobenius_mul _),
-      ← nat.iterate_add, add_comm, add_left_comm],
+      ← nat.iterate_add_apply, add_comm, add_left_comm],
   one := mk K p (0, 1),
   one_mul := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
-    by simp only [nat.iterate₀ (frobenius_one _), nat.iterate_zero, one_mul, zero_add]),
+    by simp only [nat.iterate₀ (frobenius_one _), nat.iterate_zero_apply, one_mul, zero_add]),
   mul_one := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
-    by simp only [nat.iterate₀ (frobenius_one _), nat.iterate_zero, mul_one, add_zero]),
+    by simp only [nat.iterate₀ (frobenius_one _), nat.iterate_zero_apply, mul_one, add_zero]),
   mul_comm := λ e f, quot.induction_on e (λ ⟨m, x⟩, quot.induction_on f (λ ⟨n, y⟩,
     congr_arg (quot.mk _) $ by simp only [add_comm, mul_comm])),
   .. (infer_instance : has_mul (perfect_closure K p)) }
@@ -171,15 +171,15 @@ private lemma add_aux_left (x1 x2 y : ℕ × K) (H : r K p x1 x2) :
   mk K p (x1.1 + y.1, ((frobenius K p)^[y.1] x1.2) + ((frobenius K p)^[x1.1] y.2)) =
   mk K p (x2.1 + y.1, ((frobenius K p)^[y.1] x2.2) + ((frobenius K p)^[x2.1] y.2)) :=
 match x1, x2, H with
-| _, _, r.intro n x := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
+| _, _, r.intro n x := quot.sound $ by rw [← nat.iterate_succ_apply, nat.iterate_succ',
     nat.iterate_succ', ← frobenius_add, nat.succ_add]; apply r.intro
 end
 
 private lemma add_aux_right (x y1 y2 : ℕ × K) (H : r K p y1 y2) :
   mk K p (x.1 + y1.1, ((frobenius K p)^[y1.1] x.2) + ((frobenius K p)^[x.1] y1.2)) =
   mk K p (x.1 + y2.1, ((frobenius K p)^[y2.1] x.2) + ((frobenius K p)^[x.1] y2.2)) :=
 match y1, y2, H with
-| _, _, r.intro n y := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
+| _, _, r.intro n y := quot.sound $ by rw [← nat.iterate_succ_apply, nat.iterate_succ',
     nat.iterate_succ', ← frobenius_add]; apply r.intro
 end
 
@@ -210,19 +210,19 @@ have := r.intro n (0:K); rwa [frobenius_zero K p] at this
 
 theorem r.sound (m n : ℕ) (x y : K) (H : frobenius K p^[m] x = y) :
   mk K p (n, x) = mk K p (m + n, y) :=
-by subst H; induction m with m ih; [simp only [zero_add, nat.iterate_zero],
+by subst H; induction m with m ih; [simp only [zero_add, nat.iterate_zero_apply],
   rw [ih, nat.succ_add, nat.iterate_succ']]; apply quot.sound; apply r.intro
 
 instance : comm_ring (perfect_closure K p) :=
 { add_assoc := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
     quot.induction_on g $ λ ⟨s, z⟩, congr_arg (quot.mk _) $
     by simp only [add_assoc, nat.iterate₂ (frobenius_add K p),
-      (nat.iterate_add _ _ _ _).symm, add_comm, add_left_comm],
+      ← nat.iterate_add_apply, add_comm, add_left_comm],
   zero := 0,
   zero_add := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
-    by simp only [nat.iterate₀ (frobenius_zero K p), nat.iterate_zero, zero_add]),
+    by simp only [nat.iterate₀ (frobenius_zero K p), nat.iterate_zero_apply, zero_add]),
   add_zero := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
-    by simp only [nat.iterate₀ (frobenius_zero K p), nat.iterate_zero, add_zero]),
+    by simp only [nat.iterate₀ (frobenius_zero K p), nat.iterate_zero_apply, add_zero]),
   add_left_neg := λ e, quot.induction_on e (λ ⟨n, x⟩,
     by simp only [quot_mk_eq_mk, neg_mk, mk_add_mk,
       nat.iterate₁ (frobenius_neg K p), add_left_neg, mk_zero]),
@@ -232,12 +232,12 @@ instance : comm_ring (perfect_closure K p) :=
     quot.induction_on g $ λ ⟨s, z⟩, show quot.mk _ _ = quot.mk _ _,
     by simp only [add_assoc, add_comm, add_left_comm]; apply r.sound;
     simp only [nat.iterate₂ (frobenius_mul p), nat.iterate₂ (frobenius_add K p),
-      (nat.iterate_add _ _ _ _).symm, mul_add, add_comm, add_left_comm],
+      ← nat.iterate_add_apply, mul_add, add_comm, add_left_comm],
   right_distrib := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
     quot.induction_on g $ λ ⟨s, z⟩, show quot.mk _ _ = quot.mk _ _,
     by simp only [add_assoc, add_comm _ s, add_left_comm _ s]; apply r.sound;
     simp only [nat.iterate₂ (frobenius_mul p), nat.iterate₂ (frobenius_add K p),
-      (nat.iterate_add _ _ _ _).symm, add_mul, add_comm, add_left_comm],
+      ← nat.iterate_add_apply, add_mul, add_comm, add_left_comm],
   .. (infer_instance : has_add (perfect_closure K p)),
   .. (infer_instance : has_neg (perfect_closure K p)),
   .. (infer_instance : comm_monoid (perfect_closure K p)) }
@@ -259,9 +259,9 @@ begin
     { cases ih1 with z1 ih1,
       cases ih2 with z2 ih2,
       existsi z2+(y.1+z1),
-      rw [← add_assoc, nat.iterate_add, ih1],
-      rw [← nat.iterate_add, add_comm, nat.iterate_add, ih2],
-      rw [← nat.iterate_add],
+      rw [← add_assoc, nat.iterate_add_apply, ih1],
+      rw [← nat.iterate_add_apply, add_comm, nat.iterate_add_apply, ih2],
+      rw [← nat.iterate_add_apply],
       simp only [add_comm, add_left_comm] } },
   intro H,
   cases x with m x,
@@ -349,7 +349,7 @@ instance : field (perfect_closure K p) :=
   mul_inv_cancel := λ e, induction_on e $ λ ⟨m, x⟩ H,
     have _ := mt (eq_iff _ _ _ _).2 H, (eq_iff _ _ _ _).2
       (by simp only [(frobenius _ _).iterate_map_one, (frobenius K p).iterate_map_zero,
-        nat.iterate_zero, ← (frobenius _ p).iterate_map_mul] at this ⊢;
+        nat.iterate_zero_apply, ← (frobenius _ p).iterate_map_mul] at this ⊢;
         rw [mul_inv_cancel this, (frobenius _ _).iterate_map_one]),
   inv_zero := congr_arg (quot.mk (r K p)) (by rw [inv_zero]),
   .. (infer_instance : has_inv (perfect_closure K p)),
@@ -369,7 +369,7 @@ theorem eq_pth_root (x : ℕ × K) :
 begin
   rcases x with ⟨m, x⟩,
   induction m with m ih, {refl},
-  rw [nat.iterate_succ', ← ih]; refl
+  rw [nat.iterate_succ_apply', ← ih]; refl
 end
 
 /-- Given a field `K` of characteristic `p` and a perfect field `L` of the same characteristic,
@@ -382,19 +382,19 @@ begin
     refine_struct { .. },
     field to_fun { refine λ e, lift_on e (λ x, pth_root L p^[x.1] (f x.2)) _,
       rintro a b ⟨n⟩,
-      simp only [f.map_frobenius, nat.iterate_succ, pth_root_frobenius] },
+      simp only [f.map_frobenius, nat.iterate_succ, (∘), pth_root_frobenius] },
     field map_one' { exact f.map_one },
     field map_zero' { exact f.map_zero },
     field map_mul' { rintro ⟨x⟩ ⟨y⟩,
       simp only [quot_mk_eq_mk, lift_on_mk, mk_mul_mk, ring_hom.map_iterate_frobenius,
         ring_hom.iterate_map_mul, ring_hom.map_mul],
-      rw [nat.iterate_add, nat.iterate_cancel, add_comm, nat.iterate_add, nat.iterate_cancel];
-        exact pth_root_frobenius },
+      rw [nat.iterate_add_apply, nat.iterate_cancel, add_comm, nat.iterate_add_apply,
+        nat.iterate_cancel]; exact pth_root_frobenius },
     field map_add' { rintro ⟨x⟩ ⟨y⟩,
       simp only [quot_mk_eq_mk, lift_on_mk, mk_add_mk, ring_hom.map_iterate_frobenius,
         ring_hom.iterate_map_add, ring_hom.map_add],
-      rw [nat.iterate_add, nat.iterate_cancel, add_comm x.1, nat.iterate_add, nat.iterate_cancel];
-        exact pth_root_frobenius } },
+      rw [nat.iterate_add_apply, nat.iterate_cancel, add_comm x.1, nat.iterate_add_apply,
+        nat.iterate_cancel]; exact pth_root_frobenius } },
   field inv_fun { exact λ f, f.comp (of K p) },
   field left_inv { intro f, ext x, refl },
   field right_inv { intro f, ext ⟨x⟩,

src/topology/metric_space/contracting.lean

@@ -21,6 +21,9 @@ of convergence, and some properties of the map sending a contracting map to its
   in `emetric.ball x ∞`;
 * `fixed_point` : the unique fixed point of a contracting map on a complete nonempty metric space.
 
+## Tags
+
+contracting map, fixed point, Banach fixed point theorem
 -/
 
 open_locale nnreal topological_space classical
@@ -35,8 +38,8 @@ lemma fixed_point_of_tendsto_iterate [topological_space α] [t2_space α] {f : 
   f x = x :=
 begin
   rcases hx with ⟨x₀, hx⟩,
-  refine tendsto_nhds_unique at_top_ne_bot _ hx,
-  rw [← tendsto_add_at_top_iff_nat 1, funext (assume n, nat.iterate_succ' f n x₀)],
+  refine tendsto_nhds_unique at_top_ne_bot ((tendsto_add_at_top_iff_nat 1).1 _) hx,
+  simp only [nat.iterate_succ' f],
   exact tendsto.comp hf hx
 end