refactor(library/init/meta/tactic): switch 'pose' and 'note'

library/init/algebra/ordered_group.lean

@@ -194,145 +194,145 @@ by rwa neg_zero at this
 
 lemma le_neg_of_le_neg {a b : α} (h : a ≤ -b) : b ≤ -a :=
 begin
-  pose h := neg_le_neg h,
+  note h := neg_le_neg h,
   rwa neg_neg at h
 end
 
 lemma neg_le_of_neg_le {a b : α} (h : -a ≤ b) : -b ≤ a :=
 begin
-  pose h := neg_le_neg h,
+  note h := neg_le_neg h,
   rwa neg_neg at h
 end
 
 lemma lt_neg_of_lt_neg {a b : α} (h : a < -b) : b < -a :=
 begin
-  pose h := neg_lt_neg h,
+  note h := neg_lt_neg h,
   rwa neg_neg at h
 end
 
 lemma neg_lt_of_neg_lt {a b : α} (h : -a < b) : -b < a :=
 begin
-  pose h := neg_lt_neg h,
+  note h := neg_lt_neg h,
   rwa neg_neg at h
 end
 
 lemma sub_nonneg_of_le {a b : α} (h : b ≤ a) : 0 ≤ a - b :=
 begin
-  pose h := add_le_add_right h (-b),
+  note h := add_le_add_right h (-b),
   rwa add_right_neg at h
 end
 
 lemma le_of_sub_nonneg {a b : α} (h : 0 ≤ a - b) : b ≤ a :=
 begin
-  pose h := add_le_add_right h b,
+  note h := add_le_add_right h b,
   rwa [sub_add_cancel, zero_add] at h
 end
 
 lemma sub_nonpos_of_le {a b : α} (h : a ≤ b) : a - b ≤ 0 :=
 begin
-  pose h := add_le_add_right h (-b),
+  note h := add_le_add_right h (-b),
   rwa add_right_neg at h
 end
 
 lemma le_of_sub_nonpos {a b : α} (h : a - b ≤ 0) : a ≤ b :=
 begin
-  pose h := add_le_add_right h b,
+  note h := add_le_add_right h b,
   rwa [sub_add_cancel, zero_add] at h
 end
 
 lemma sub_pos_of_lt {a b : α} (h : b < a) : 0 < a - b :=
 begin
-  pose h := add_lt_add_right h (-b),
+  note h := add_lt_add_right h (-b),
   rwa add_right_neg at h
 end
 
 lemma lt_of_sub_pos {a b : α} (h : 0 < a - b) : b < a :=
 begin
-  pose h := add_lt_add_right h b,
+  note h := add_lt_add_right h b,
   rwa [sub_add_cancel, zero_add] at h
 end
 
 lemma sub_neg_of_lt {a b : α} (h : a < b) : a - b < 0 :=
 begin
-  pose h := add_lt_add_right h (-b),
+  note h := add_lt_add_right h (-b),
   rwa add_right_neg at h
 end
 
 lemma lt_of_sub_neg {a b : α} (h : a - b < 0) : a < b :=
 begin
-  pose h := add_lt_add_right h b,
+  note h := add_lt_add_right h b,
   rwa [sub_add_cancel, zero_add] at h
 end
 
 lemma add_le_of_le_neg_add {a b c : α} (h : b ≤ -a + c) : a + b ≤ c :=
 begin
-  pose h := add_le_add_left h a,
+  note h := add_le_add_left h a,
   rwa add_neg_cancel_left at h
 end
 
 lemma le_neg_add_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ -a + c :=
 begin
-  pose h := add_le_add_left h (-a),
+  note h := add_le_add_left h (-a),
   rwa neg_add_cancel_left at h
 end
 
 lemma add_le_of_le_sub_left {a b c : α} (h : b ≤ c - a) : a + b ≤ c :=
 begin
-  pose h := add_le_add_left h a,
+  note h := add_le_add_left h a,
   rwa [-add_sub_assoc, add_comm a c, add_sub_cancel] at h
 end
 
 lemma le_sub_left_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ c - a :=
 begin
-  pose h := add_le_add_right h (-a),
+  note h := add_le_add_right h (-a),
   rwa [add_comm a b, add_neg_cancel_right] at h
 end
 
 lemma add_le_of_le_sub_right {a b c : α} (h : a ≤ c - b) : a + b ≤ c :=
 begin
-  pose h := add_le_add_right h b,
+  note h := add_le_add_right h b,
   rwa sub_add_cancel at h
 end
 
 lemma le_sub_right_of_add_le {a b c : α} (h : a + b ≤ c) : a ≤ c - b :=
 begin
-  pose h := add_le_add_right h (-b),
+  note h := add_le_add_right h (-b),
   rwa add_neg_cancel_right at h
 end
 
 lemma le_add_of_neg_add_le {a b c : α} (h : -b + a ≤ c) : a ≤ b + c :=
 begin
-  pose h := add_le_add_left h b,
+  note h := add_le_add_left h b,
   rwa add_neg_cancel_left at h
 end
 
 lemma neg_add_le_of_le_add {a b c : α} (h : a ≤ b + c) : -b + a ≤ c :=
 begin
-  pose h := add_le_add_left h (-b),
+  note h := add_le_add_left h (-b),
   rwa neg_add_cancel_left at h
 end
 
 lemma le_add_of_sub_left_le {a b c : α} (h : a - b ≤ c) : a ≤ b + c :=
 begin
-  pose h := add_le_add_right h b,
+  note h := add_le_add_right h b,
   rwa [sub_add_cancel, add_comm] at h
 end
 
 lemma sub_left_le_of_le_add {a b c : α} (h : a ≤ b + c) : a - b ≤ c :=
 begin
-  pose h := add_le_add_right h (-b),
+  note h := add_le_add_right h (-b),
   rwa [add_comm b c, add_neg_cancel_right] at h
 end
 
 lemma le_add_of_sub_right_le {a b c : α} (h : a - c ≤ b) : a ≤ b + c :=
 begin
-  pose h := add_le_add_right h c,
+  note h := add_le_add_right h c,
   rwa sub_add_cancel at h
 end
 
 lemma sub_right_le_of_le_add {a b c : α} (h : a ≤ b + c) : a - c ≤ b :=
 begin
-  pose h := add_le_add_right h (-c),
+  note h := add_le_add_right h (-c),
   rwa add_neg_cancel_right at h
 end
 
@@ -365,7 +365,7 @@ le_add_of_neg_add_le_left (add_le_of_le_sub_right h)
 
 lemma neg_le_sub_left_of_le_add {a b c : α} (h : c ≤ a + b) : -a ≤ b - c :=
 begin
-  pose h := le_neg_add_of_add_le (sub_left_le_of_le_add h),
+  note h := le_neg_add_of_add_le (sub_left_le_of_le_add h),
   rwa add_comm at h
 end
 
@@ -389,73 +389,73 @@ add_le_add hab (neg_le_neg hcd)
 
 lemma add_lt_of_lt_neg_add {a b c : α} (h : b < -a + c) : a + b < c :=
 begin
-  pose h := add_lt_add_left h a,
+  note h := add_lt_add_left h a,
   rwa add_neg_cancel_left at h
 end
 
 lemma lt_neg_add_of_add_lt {a b c : α} (h : a + b < c) : b < -a + c :=
 begin
-  pose h := add_lt_add_left h (-a),
+  note h := add_lt_add_left h (-a),
   rwa neg_add_cancel_left at h
 end
 
 lemma add_lt_of_lt_sub_left {a b c : α} (h : b < c - a) : a + b < c :=
 begin
-  pose h := add_lt_add_left h a,
+  note h := add_lt_add_left h a,
   rwa [-add_sub_assoc, add_comm a c, add_sub_cancel] at h
 end
 
 lemma lt_sub_left_of_add_lt {a b c : α} (h : a + b < c) : b < c - a :=
 begin
-  pose h := add_lt_add_right h (-a),
+  note h := add_lt_add_right h (-a),
   rwa [add_comm a b, add_neg_cancel_right] at h
 end
 
 lemma add_lt_of_lt_sub_right {a b c : α} (h : a < c - b) : a + b < c :=
 begin
-  pose h := add_lt_add_right h b,
+  note h := add_lt_add_right h b,
   rwa sub_add_cancel at h
 end
 
 lemma lt_sub_right_of_add_lt {a b c : α} (h : a + b < c) : a < c - b :=
 begin
-  pose h := add_lt_add_right h (-b),
+  note h := add_lt_add_right h (-b),
   rwa add_neg_cancel_right at h
 end
 
 lemma lt_add_of_neg_add_lt {a b c : α} (h : -b + a < c) : a < b + c :=
 begin
-  pose h := add_lt_add_left h b,
+  note h := add_lt_add_left h b,
   rwa add_neg_cancel_left at h
 end
 
 lemma neg_add_lt_of_lt_add {a b c : α} (h : a < b + c) : -b + a < c :=
 begin
-  pose h := add_lt_add_left h (-b),
+  note h := add_lt_add_left h (-b),
   rwa neg_add_cancel_left at h
 end
 
 lemma lt_add_of_sub_left_lt {a b c : α} (h : a - b < c) : a < b + c :=
 begin
-  pose h := add_lt_add_right h b,
+  note h := add_lt_add_right h b,
   rwa [sub_add_cancel, add_comm] at h
 end
 
 lemma sub_left_lt_of_lt_add {a b c : α} (h : a < b + c) : a - b < c :=
 begin
-  pose h := add_lt_add_right h (-b),
+  note h := add_lt_add_right h (-b),
   rwa [add_comm b c, add_neg_cancel_right] at h
 end
 
 lemma lt_add_of_sub_right_lt {a b c : α} (h : a - c < b) : a < b + c :=
 begin
-  pose h := add_lt_add_right h c,
+  note h := add_lt_add_right h c,
   rwa sub_add_cancel at h
 end
 
 lemma sub_right_lt_of_lt_add {a b c : α} (h : a < b + c) : a - c < b :=
 begin
-  pose h := add_lt_add_right h (-c),
+  note h := add_lt_add_right h (-c),
   rwa add_neg_cancel_right at h
 end
 
@@ -488,7 +488,7 @@ lt_add_of_neg_add_lt_left (add_lt_of_lt_sub_right h)
 
 lemma neg_lt_sub_left_of_lt_add {a b c : α} (h : c < a + b) : -a < b - c :=
 begin
-  pose h := lt_neg_add_of_add_lt (sub_left_lt_of_lt_add h),
+  note h := lt_neg_add_of_add_lt (sub_left_lt_of_lt_add h),
   rwa add_comm at h
 end
 

library/init/meta/tactic.lean

@@ -384,12 +384,12 @@ meta def step {α : Type u} (t : tactic α) : tactic unit :=
 t >>[tactic] cleanup
 
 /- Add (H : T := pr) to the current goal -/
-meta def note (n : name) (pr : expr) : tactic unit :=
+meta def pose (n : name) (pr : expr) : tactic unit :=
 do t ← infer_type pr,
    definev n t pr
 
 /- Add (H : T) to the current goal, given a proof (pr : T) -/
-meta def pose (n : name) (pr : expr) : tactic unit :=
+meta def note (n : name) (pr : expr) : tactic unit :=
 do t ← infer_type pr,
    assertv n t pr
 

tests/lean/run/assert_tac3.lean

@@ -41,7 +41,7 @@ end
 
 definition tst6 (a : nat) : a = a :=
 begin
-  note x := a,
+  pose x := a,
   trace_state,
   exact eq.refl x
 end