update lean to nightly-2021-08-29

Mathlib/Data/Int/Basic.lean

@@ -31,7 +31,6 @@ lemma subNatNat_of_sub_eq_zero {m n : ℕ} (h : n - m = 0) : subNatNat m n = ofN
   | succ k => -[1+ k]
   ) = ofNat (m - n)
   rw [h]
-  rfl
 
 lemma subNatNat_of_sub_eq_succ {m n k : ℕ} (h : n - m = succ k) : subNatNat m n = -[1+ k] := by
   show (match n - m with
@@ -132,7 +131,6 @@ by
           | succ k => -[1+ k]) = ofNat n
   rw [Nat.sub_eq_zero_of_le (Nat.le_add_right _ _)]
   rw [Nat.add_sub_cancel_left]
-  rfl
 
 lemma subNatNat_add_right {m n : ℕ} : subNatNat m (m + n + 1) = negSucc n := by
   change (match m + n + 1 - m with
@@ -459,7 +457,6 @@ lemma ofNat_sub {n m : ℕ} (h : m ≤ n) : ofNat (n - m) = ofNat n - ofNat m :=
     show ofNat (n - succ m) = subNatNat n (succ m)
     simp [subNatNat, subNatNat] -- TODO: How to avoid having to simp through rename definitions to unfold them?
     rw [sub_eq_zero_of_le h]
-    rfl
 
 protected lemma add_left_comm (a b c : ℤ) : a + (b + c) = b + (a + c) :=
 by rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]

Mathlib/Data/List/Basic.lean

@@ -348,11 +348,6 @@ lemma bind_map {g : α → List β} {f : β → γ} :
 
 /-! ### length -/
 
-@[simp] lemma length_append (s t : List α) : length (s ++ t) = length s + length t := by
-  induction s with
-  | nil => simp
-  | cons a s ih => simp [ih, Nat.add_comm, Nat.add_left_comm, Nat.succ_add]
-
 -- @[simp] lemma length_repeat (a : α) (n : ℕ) : length (repeat a n) = n :=
 -- by induction n; simp [*]; refl
 

leanpkg.toml

@@ -1,4 +1,4 @@
 [package]
 name = "mathlib4"
 version = "0.1"
-lean_version = "leanprover/lean4:nightly-2021-08-25"
+lean_version = "leanprover/lean4:nightly-2021-08-29"