chore: bump to nightly-2022-03-01 (#216)

Author: gebner

Mathlib/Data/List/Basic.lean

@@ -529,14 +529,14 @@ theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β}
 
 /-! ### repeat -/
 
-theorem repeat_succ (a : α) n : repeat a (n+1) = a :: repeat a n := rfl
+theorem repeat'_succ (a : α) n : repeat' a (n+1) = a :: repeat' a n := rfl
 
-theorem mem_repeat {a b : α} : ∀ {n}, b ∈ repeat a n ↔ n ≠ 0 ∧ b = a
+theorem mem_repeat' {a b : α} : ∀ {n}, b ∈ repeat' a n ↔ n ≠ 0 ∧ b = a
 | 0 => by simp
-| n+1 => by simp [mem_repeat]
+| n+1 => by simp [mem_repeat']
 
-theorem eq_of_mem_repeat {a b : α} {n} (h : b ∈ repeat a n) : b = a :=
-  (mem_repeat.1 h).2
+theorem eq_of_mem_repeat' {a b : α} {n} (h : b ∈ repeat' a n) : b = a :=
+  (mem_repeat'.1 h).2
 
 /-! ### getLast -/
 
@@ -671,12 +671,12 @@ theorem get_append_right_aux {l₁ l₂ : List α} {n : ℕ}
   rw [length_append] at h₂
   exact Nat.sub_lt_left_of_lt_add h₁ h₂
 
-theorem get_append_right {l₁ l₂ : List α} {n : ℕ} (h₁ : l₁.length ≤ n) (h₂) :
+theorem get_append_right' {l₁ l₂ : List α} {n : ℕ} (h₁ : l₁.length ≤ n) (h₂) :
     (l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, id <| get_append_right_aux h₁ h₂⟩ :=
 Option.some.inj $ by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁]
 
-@[simp] theorem get_repeat (a : α) {n : ℕ} (m : Fin _) : (List.repeat a n).get m = a :=
-  eq_of_mem_repeat (get_mem _ _ _)
+@[simp] theorem get_repeat' (a : α) {n : ℕ} (m : Fin _) : (List.repeat' a n).get m = a :=
+  eq_of_mem_repeat' (get_mem _ _ _)
 
 theorem get?_append {l₁ l₂ : List α} {n : ℕ} (hn : n < l₁.length) :
   (l₁ ++ l₂).get? n = l₁.get? n := by
@@ -1236,21 +1236,21 @@ List.decidablePairwise
 /-- pad `l : List α` with repeated occurrences of `a : α` until it's of length `n`.
   If `l` is initially larger than `n`, just return `l`. -/
 def leftpad (n : ℕ) (a : α) (l : List α) : List α :=
-repeat a (n - length l) ++ l
+repeat' a (n - length l) ++ l
 
 /-- The length of the List returned by `List.leftpad n a l` is equal
   to the larger of `n` and `l.length` -/
 theorem leftpad_length (n : ℕ) (a : α) (l : List α) : (leftpad n a l).length = max n l.length :=
-by simp only [leftpad, length_append, length_repeat, Nat.sub_add_eq_max]
+by simp only [leftpad, length_append, length_repeat', Nat.sub_add_eq_max]
 
-theorem leftpad_prefix [DecidableEq α] (n : ℕ) (a : α) (l : List α) : isPrefix (repeat a (n - length l)) (leftpad n a l) :=
+theorem leftpad_prefix [DecidableEq α] (n : ℕ) (a : α) (l : List α) : isPrefix (repeat' a (n - length l)) (leftpad n a l) :=
 by
   simp only [isPrefix, leftpad]
   exact Exists.intro l rfl
 
 theorem leftpad_suffix [DecidableEq α] (n : ℕ) (a : α) (l : List α) : isSuffix l (leftpad n a l) :=
 by
   simp only [isSuffix, leftpad]
-  exact Exists.intro (repeat a (n - length l)) rfl
+  exact Exists.intro (repeat' a (n - length l)) rfl
 
 end List

Mathlib/Data/Nat/Basic.lean

@@ -39,10 +39,6 @@ protected lemma not_le {n m : ℕ} : ¬ n ≤ m ↔ m < n :=
 protected lemma lt_or_eq_of_le {n m : ℕ} (h : n ≤ m) : n < m ∨ n = m :=
 (Nat.lt_or_ge _ _).imp_right (Nat.le_antisymm h)
 
-lemma eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : 0 < m) (H : n * m = k * m) : n = k :=
-by rw [Nat.mul_comm n m, Nat.mul_comm k m] at H
-   exact Nat.eq_of_mul_eq_mul_left Hm H
-
 theorem le_zero_iff {i : ℕ} : i ≤ 0 ↔ i = 0 :=
   ⟨Nat.eq_zero_of_le_zero, λ h => h ▸ le_refl i⟩
 

Mathlib/Data/String/Defs.lean

@@ -7,7 +7,7 @@ namespace String
 def leftpad (n : Nat) (c : Char) (s : String) : String :=
 ⟨List.leftpad n c s.data⟩
 
-def repeat (c : Char) (n : Nat) : String := ⟨List.repeat c n⟩
+def repeat' (c : Char) (n : Nat) : String := ⟨List.repeat' c n⟩
 
 def isPrefix : String -> String -> Prop
 | ⟨d1⟩, ⟨d2⟩ => List.isPrefix d1 d2

Mathlib/Data/String/Lemmas.lean

@@ -12,8 +12,8 @@ lemma congr_append : ∀ (a b : String), a ++ b = String.mk (a.data ++ b.data)
   simp only [String.length]
   exact List.length_append as bs
 
-@[simp] lemma length_repeat (c : Char) (n : ℕ) : (repeat c n).length = n :=
-by simp only [String.length, String.repeat, List.length_repeat]
+@[simp] lemma length_repeat' (c : Char) (n : ℕ) : (repeat' c n).length = n :=
+by simp only [String.length, String.repeat', List.length_repeat']
 
 lemma length_eq_list_length (l : List Char) : (String.mk l).length = l.length :=
 by simp only [String.length]
@@ -23,10 +23,10 @@ by simp only [String.length]
 @[simp] lemma leftpad_length (n : ℕ) (c : Char) : ∀ (s : String), (leftpad n c s).length = max n s.length
 | ⟨s⟩ => by simp only [leftpad, String.length, List.leftpad_length]
 
-lemma leftpad_prefix (n : ℕ) (c : Char) : ∀ s, isPrefix (repeat c (n - length s)) (leftpad n c s)
-| ⟨l⟩ => by simp only [isPrefix, repeat, leftpad, String.length, List.leftpad_prefix]
+lemma leftpad_prefix (n : ℕ) (c : Char) : ∀ s, isPrefix (repeat' c (n - length s)) (leftpad n c s)
+| ⟨l⟩ => by simp only [isPrefix, repeat', leftpad, String.length, List.leftpad_prefix]
 
 lemma leftpad_suffix (n : ℕ) (c : Char) : ∀ s, isSuffix s (leftpad n c s)
-| ⟨l⟩ => by simp only [isSuffix, repeat, leftpad, String.length, List.leftpad_suffix]
+| ⟨l⟩ => by simp only [isSuffix, repeat', leftpad, String.length, List.leftpad_suffix]
 
 end String

Mathlib/Init/Data/List/Basic.lean

@@ -131,9 +131,9 @@ protected def inter [DecidableEq α] (l₁ l₂ : List α) : List α :=
 
 instance [DecidableEq α] : Inter (List α) := ⟨List.inter⟩
 
-@[simp] def repeat (a : α) : Nat → List α
+@[simp] def repeat' (a : α) : Nat → List α
 | 0 => []
-| succ n => a :: repeat a n
+| succ n => a :: repeat' a n
 
 def last! [Inhabited α] : List α → α
 | [] => panic! "empty list"

Mathlib/Init/Data/List/Lemmas.lean

@@ -10,7 +10,7 @@ namespace List
 
 open Nat
 
-@[simp] theorem length_repeat (a : α) (n : Nat) : length (repeat a n) = n := by
+@[simp] theorem length_repeat' (a : α) (n : Nat) : length (repeat' a n) = n := by
   induction n <;> simp_all
 
 @[simp] theorem length_tail (l : List α) : length (tail l) = length l - 1 := by cases l <;> rfl

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -60,15 +60,6 @@ lemma pred_lt_pred : ∀ {n m : ℕ}, n ≠ 0 → n < m → pred n < pred m
 protected lemma add_left_cancel_iff {n m k : ℕ} : n + m = n + k ↔ m = k :=
 ⟨Nat.add_left_cancel, fun | rfl => rfl⟩
 
-protected lemma le_of_add_le_add_left {k n m : ℕ} (h : k + n ≤ k + m) : n ≤ m := by
-  let ⟨w, hw⟩ := le.dest h
-  rw [Nat.add_assoc, Nat.add_left_cancel_iff] at hw
-  exact Nat.le.intro hw
-
-protected lemma le_of_add_le_add_right {k n m : ℕ} : n + k ≤ m + k → n ≤ m := by
-  rw [Nat.add_comm _ k, Nat.add_comm _ k]
-  apply Nat.le_of_add_le_add_left
-
 protected lemma add_le_add_iff_le_right (k n m : ℕ) : n + k ≤ m + k ↔ n ≤ m :=
 ⟨Nat.le_of_add_le_add_right, fun h => Nat.add_le_add_right h _⟩
 
@@ -88,13 +79,6 @@ Nat.add_lt_add_left h n
 protected lemma lt_add_of_pos_left {n k : ℕ} (h : 0 < k) : n < k + n :=
 by rw [Nat.add_comm]; exact Nat.lt_add_of_pos_right h
 
-protected lemma le_of_mul_le_mul_left {a b c : ℕ} (h : c * a ≤ c * b) (hc : 0 < c) : a ≤ b :=
-not_lt.1 fun h1 => not_le.2 (Nat.mul_lt_mul_of_pos_left h1 hc) h
-
-protected theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : 0 < n) (H : n * m = n * k) : m = k :=
-Nat.le_antisymm (Nat.le_of_mul_le_mul_left (Nat.le_of_eq H) Hn)
-                (Nat.le_of_mul_le_mul_left (Nat.le_of_eq H.symm) Hn)
-
 /- sub properties -/
 
 attribute [simp] Nat.zero_sub
@@ -131,9 +115,6 @@ protected lemma le_of_le_of_sub_le_sub_right {n m k : ℕ} (h₀ : k ≤ m) (h
 protected lemma sub_le_sub_right_iff {n m k : ℕ} (h : k ≤ m) : n - k ≤ m - k ↔ n ≤ m :=
 ⟨Nat.le_of_le_of_sub_le_sub_right h, fun h => Nat.sub_le_sub_right h k⟩
 
-protected theorem sub_self_add (n m : ℕ) : n - (n + m) = 0 :=
-show (n + 0) - (n + m) = 0 by rw [Nat.add_sub_add_left, Nat.zero_sub]
-
 protected theorem add_le_to_le_sub (x : ℕ) {y k : ℕ}
   (h : k ≤ y)
 : x + k ≤ y ↔ x ≤ y - k :=
@@ -153,10 +134,6 @@ rfl
 theorem succ_pred_eq_of_pos : ∀ {n : ℕ}, 0 < n → succ (pred n) = n
 | succ k, h => rfl
 
-protected theorem sub_eq_zero_of_le {n m : ℕ} (h : n ≤ m) : n - m = 0 :=
-Exists.elim (Nat.le.dest h)
-  (λ k => λ hk : n + k = m => by rw [← hk, Nat.sub_self_add])
-
 protected theorem le_of_sub_eq_zero : ∀{n m : ℕ}, n - m = 0 → n ≤ m
 | n, 0, H => by rw [Nat.sub_zero] at H; simp [H]
 | 0, m+1, H => Nat.zero_le (m + 1)
@@ -540,7 +517,7 @@ lemma sub_mul_mod (x k n : ℕ) (h₁ : n*k ≤ x) : (x - n*k) % n = x % n := by
       apply Nat.le_trans _ h₁
       apply le_add_right _ n
     have h₄ : x - n * k ≥ n := by
-      apply Nat.le_of_add_le_add_right (k := n*k)
+      apply Nat.le_of_add_le_add_right (b := n*k)
       rw [Nat.sub_add_cancel h₂]
       simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]
     rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, IH h₂]

Mathlib/Logic/Basic.lean

@@ -568,7 +568,7 @@ section equality
 
 variable {α : Sort _} {a b : α}
 
-@[simp] theorem heq_iff_eq : HEq a b ↔ a = b :=
+theorem heq_iff_eq : HEq a b ↔ a = b :=
 ⟨eq_of_heq, heq_of_eq⟩
 
 theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq :=

Mathlib/Util/Simp.lean

@@ -38,8 +38,6 @@ toUnfold: {s.toUnfold.toList}
 erased: {s.erased.toList}
 toUnfoldThms: {s.toUnfoldThms.toList}"
 
-export private mkEqTrans from Lean.Meta.Tactic.Simp.Main
-
 def mkEqSymm (e : Expr) (r : Simp.Result) : MetaM Simp.Result :=
   ({ expr := e, proof? := · }) <$>
   match r.proof? with

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-21
+leanprover/lean4:nightly-2022-03-01