chore: bump toolchain to v4.20.0-rc1 (#1219)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>

Author: 11 people

Batteries/Control/AlternativeMonad.lean

@@ -120,7 +120,7 @@ instance : LawfulAlternative Option.{u} where
   map_failure _ := rfl
   failure_seq _ := rfl
   orElse_failure := Option.orElse_none
-  failure_orElse := Option.none_orElse
+  failure_orElse := by simp [failure]
   orElse_assoc | some _, _, _ => rfl | none, _, _ => rfl
   map_orElse | some _ => by simp | none => by simp
 

Batteries/Data/BitVec/Lemmas.lean

@@ -58,7 +58,7 @@ theorem getLsbD_ofFnLE (f : Fin n → Bool) (i) :
     (ofFnLE f).getLsbD i = if h : i < n then f ⟨i, h⟩ else false := by
   split
   · next h => rw [getLsbD_eq_getElem h, getElem_ofFnLE]
-  · next h => rw [getLsbD_ge _ _ (Nat.ge_of_not_lt h)]
+  · next h => rw [getLsbD_of_ge _ _ (Nat.ge_of_not_lt h)]
 
 @[simp] theorem getMsb'_ofFnLE (f : Fin n → Bool) (i) : (ofFnLE f).getMsb' i = f i.rev := by
   simp [getMsb'_eq_getLsb', Fin.rev]; congr 2; omega
@@ -70,7 +70,7 @@ theorem getMsbD_ofFnLE (f : Fin n → Bool) (i) :
     have heq : n - 1 - i = n - (i + 1) := by omega
     have hlt : n - (i + 1) < n := by omega
     simp [getMsbD_eq_getLsbD, getLsbD_ofFnLE, Fin.rev, h, heq, hlt]
-  · next h => rw [getMsbD_ge _ _ (Nat.ge_of_not_lt h)]
+  · next h => rw [getMsbD_of_ge _ _ (Nat.ge_of_not_lt h)]
 
 theorem msb_ofFnLE (f : Fin n → Bool) :
     (ofFnLE f).msb = if h : n ≠ 0 then f ⟨n-1, Nat.sub_one_lt h⟩ else false := by

Batteries/Data/Fin/Lemmas.lean

@@ -25,8 +25,8 @@ theorem findSome?_succ {f : Fin (n+1) → Option α} :
     findSome? f = (f 0 <|> findSome? fun i => f i.succ) := by
   simp only [findSome?, foldl_succ, Option.none_orElse, Function.comp_apply]
   cases f 0
-  · rw [Option.none_orElse]
-  · rw [Option.some_orElse]
+  · rw [Option.orElse_eq_orElse, Option.none_orElse, Option.none_orElse]
+  · simp only [Option.some_orElse, Option.orElse_eq_orElse, Option.none_orElse]
     induction n with
     | zero => rfl
     | succ n ih => rw [foldl_succ, Option.some_orElse, ih (f := fun i => f i.succ)]
@@ -51,11 +51,11 @@ theorem exists_of_findSome?_eq_some {f : Fin n → Option α} (h : findSome? f =
     rw [findSome?_succ] at h
     match heq : f 0 with
     | some x =>
-      rw [heq, Option.some_orElse] at h
+      rw [heq, Option.orElse_eq_orElse, Option.some_orElse] at h
       exists 0
       rw [heq, h]
     | none =>
-      rw [heq, Option.none_orElse] at h
+      rw [heq, Option.orElse_eq_orElse, Option.none_orElse] at h
       match ih h with | ⟨i, _⟩ => exists i.succ
 
 theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f = none) (i) :
@@ -66,10 +66,10 @@ theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f
     rw [findSome?_succ] at h
     match heq : f 0 with
     | some x =>
-      rw [heq, Option.some_orElse] at h
+      rw [heq, Option.orElse_eq_orElse, Option.some_orElse] at h
       contradiction
     | none =>
-      rw [heq, Option.none_orElse] at h
+      rw [heq, Option.orElse_eq_orElse, Option.none_orElse] at h
       cases i using Fin.cases with
       | zero => exact heq
       | succ i => exact ih h i
@@ -106,7 +106,7 @@ theorem map_findSome? (f : Fin n → Option α) (g : α → β) :
   | zero => rfl
   | succ n ih => simp [findSome?_succ, Function.comp_def, Option.map_orElse, ih]
 
-theorem findSome?_guard {p : Fin n → Bool} : findSome? (Option.guard fun i => p i) = find? p := rfl
+theorem findSome?_guard {p : Fin n → Bool} : findSome? (Option.guard p) = find? p := rfl
 
 theorem findSome?_eq_findSome?_finRange (f : Fin n → Option α) :
     findSome? f = (List.finRange n).findSome? f := by

Batteries/Data/List/Lemmas.lean

@@ -575,7 +575,7 @@ theorem dropInfix?_go_eq_some_iff [BEq α] {i l acc p s : List α} :
         rw [cons_eq_append_iff] at h₁
         simp at h₁
         obtain (⟨⟨rfl, rfl⟩, rfl⟩ | ⟨a', h₁, rfl⟩) := h₁
-        · simp only [nil_beq_iff, isEmpty_iff] at h₂
+        · simp only [nil_beq_eq, isEmpty_iff] at h₂
           simp only [h₂] at h
           simp at h
         · rw [append_eq_cons_iff] at h₁
@@ -647,7 +647,7 @@ theorem append_eq_of_isPrefixOf?_eq_some [BEq α] [LawfulBEq α] {xs ys zs : Lis
 
 @[simp] theorem isSuffixOf?_eq_some_iff_append_eq [BEq α] [LawfulBEq α] {xs ys zs : List α} :
     xs.isSuffixOf? ys = some zs ↔ zs ++ xs = ys := by
-  simp only [isSuffixOf?, map_eq_some', isPrefixOf?_eq_some_iff_append_eq]
+  simp only [isSuffixOf?, map_eq_some_iff, isPrefixOf?_eq_some_iff_append_eq]
   constructor
   · intro
     | ⟨_, h, heq⟩ =>

Batteries/Data/Nat/Gcd.lean

@@ -171,7 +171,7 @@ theorem Coprime.eq_one_of_dvd {k m : Nat} (H : Coprime k m) (d : k ∣ m) : k =
 
 theorem Coprime.gcd_mul (k : Nat) (h : Coprime m n) : gcd k (m * n) = gcd k m * gcd k n :=
   Nat.dvd_antisymm
-    (gcd_mul_dvd_mul_gcd k m n)
+    (gcd_mul_right_dvd_mul_gcd k m n)
     ((h.gcd_both k k).mul_dvd_of_dvd_of_dvd
       (gcd_dvd_gcd_mul_right_right ..)
       (gcd_dvd_gcd_mul_left_right ..))
@@ -183,5 +183,5 @@ theorem gcd_mul_gcd_of_coprime_of_mul_eq_mul
     rw [← h]
     apply Nat.mul_dvd_mul (gcd_dvd ..).1 (gcd_dvd ..).1
   · rw [gcd_comm a, gcd_comm b]
-    refine Nat.dvd_trans ?_ (gcd_mul_dvd_mul_gcd ..)
+    refine Nat.dvd_trans ?_ (gcd_mul_right_dvd_mul_gcd ..)
     rw [h, gcd_mul_right_right d c]; apply Nat.dvd_refl

Batteries/Data/RBMap/Lemmas.lean

@@ -711,7 +711,7 @@ theorem zoom_del {t : RBNode α} :
     t.zoom cut path = (t', path') →
     path.del (t.del cut) (match t with | node c .. => c | _ => red) =
     path'.del t'.delRoot (match t' with | node c .. => c | _ => red) := by
-  unfold RBNode.del; split <;> simp [zoom]
+  rw [RBNode.del.eq_def]; split <;> simp [zoom]
   · intro | rfl, rfl => rfl
   · next c a y b =>
     split
@@ -1152,7 +1152,7 @@ theorem findEntry?_some_mem_toList {t : RBMap α β cmp} (h : t.findEntry? x = s
 
 theorem find?_some_mem_toList {t : RBMap α β cmp} (h : t.find? x = some v) :
     ∃ y, (y, v) ∈ toList t ∧ cmp x y = .eq := by
-  obtain ⟨⟨y, v⟩, h', rfl⟩ := Option.map_eq_some'.1 h
+  obtain ⟨⟨y, v⟩, h', rfl⟩ := Option.map_eq_some_iff.1 h
   exact ⟨_, findEntry?_some_mem_toList h', findEntry?_some_eq_eq h'⟩
 
 theorem mem_toList_unique [@TransCmp α cmp] {t : RBMap α β cmp}
@@ -1176,7 +1176,7 @@ theorem findEntry?_some [@TransCmp α cmp] {t : RBMap α β cmp} :
 
 theorem find?_some [@TransCmp α cmp] {t : RBMap α β cmp} :
     t.find? x = some v ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = .eq := by
-  simp only [find?, findEntry?_some, Option.map_eq_some']; constructor
+  simp only [find?, findEntry?_some, Option.map_eq_some_iff]; constructor
   · rintro ⟨_, h, rfl⟩; exact ⟨_, h⟩
   · rintro ⟨b, h⟩; exact ⟨_, h, rfl⟩
 
@@ -1185,7 +1185,7 @@ theorem contains_iff_findEntry? {t : RBMap α β cmp} :
 
 theorem contains_iff_find? {t : RBMap α β cmp} :
     t.contains x ↔ ∃ v, t.find? x = some v := by
-  simp only [contains_iff_findEntry?, Prod.exists, find?, Option.map_eq_some', and_comm,
+  simp only [contains_iff_findEntry?, Prod.exists, find?, Option.map_eq_some_iff, and_comm,
     exists_eq_left]
   rw [exists_comm]
 

Batteries/Data/Rat/Basic.lean

@@ -48,7 +48,7 @@ dividing both `num` and `den` by `g` (which is the gcd of the two) if it is not
   if hg : g = 1 then
     { num, den
       den_nz := by simp [hg] at den_nz; exact den_nz
-      reduced := by simp [hg, Int.natAbs_ofNat] at reduced; exact reduced }
+      reduced := by simp [hg, Int.natAbs_natCast] at reduced; exact reduced }
   else { num := num.tdiv g, den := den / g, den_nz, reduced }
 
 theorem Rat.normalize.den_nz {num : Int} {den g : Nat} (den_nz : den ≠ 0)

Batteries/Data/Rat/Lemmas.lean

@@ -52,7 +52,7 @@ theorem normalize_self (r : Rat) : normalize r.num r.den r.den_nz = r := (mk_eq_
 theorem normalize_mul_left {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) :
     normalize (↑a * n) (a * d) (Nat.mul_ne_zero a0 d0) = normalize n d d0 := by
   simp [normalize_eq, mk'.injEq, Int.natAbs_mul, Nat.gcd_mul_left,
-    Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero a0), Int.ofNat_mul,
+    Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero a0), Int.natCast_mul,
     Int.mul_ediv_mul_of_pos _ _ (Int.ofNat_pos.2 <| Nat.pos_of_ne_zero a0)]
 
 theorem normalize_mul_right {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) :
@@ -68,7 +68,7 @@ theorem normalize_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
     have hd₁ := Int.ofNat_dvd.2 <| Nat.gcd_dvd_right n₁.natAbs d₁
     have hd₂ := Int.ofNat_dvd.2 <| Nat.gcd_dvd_right n₂.natAbs d₂
     rw [← Int.ediv_mul_cancel (Int.dvd_trans hd₂ (Int.dvd_mul_left ..)),
-      Int.mul_ediv_assoc _ hd₂, ← Int.ofNat_ediv, ← h.2, Int.ofNat_ediv,
+      Int.mul_ediv_assoc _ hd₂, ← Int.natCast_ediv, ← h.2, Int.natCast_ediv,
       ← Int.mul_ediv_assoc _ hd₁, Int.mul_ediv_assoc' _ hn₁,
       Int.mul_right_comm, h.1, Int.ediv_mul_cancel hn₂]
   · rw [← normalize_mul_right _ z₂, ← normalize_mul_left z₂ z₁, Int.mul_comm d₁, h]
@@ -172,10 +172,10 @@ theorem divInt_num_den (z : d ≠ 0) (h : n /. d = ⟨n', d', z', c⟩) :
   rcases Int.eq_nat_or_neg d with ⟨_, rfl | rfl⟩ <;>
     simp_all [divInt_neg', Int.ofNat_eq_zero, Int.neg_eq_zero]
   · have ⟨m, h₁, h₂⟩ := mkRat_num_den z h; exists m
-    simp [Int.ofNat_eq_zero, Int.ofNat_mul, h₁, h₂]
+    simp [Int.ofNat_eq_zero, Int.natCast_mul, h₁, h₂]
   · have ⟨m, h₁, h₂⟩ := mkRat_num_den z h; exists -m
     rw [← Int.neg_inj, Int.neg_neg] at h₂
-    simp [Int.ofNat_eq_zero, Int.ofNat_mul, h₁, h₂, Int.mul_neg, Int.neg_eq_zero]
+    simp [Int.ofNat_eq_zero, Int.natCast_mul, h₁, h₂, Int.mul_neg, Int.neg_eq_zero]
 
 @[simp] theorem ofInt_ofNat : ofInt (OfNat.ofNat n) = OfNat.ofNat n := rfl
 
@@ -209,7 +209,7 @@ theorem normalize_add_normalize (n₁ n₂) {d₁ d₂} (z₁ z₂) :
   cases e₁ : normalize n₁ d₁ z₁; rcases normalize_num_den e₁ with ⟨g₁, zg₁, rfl, rfl⟩
   cases e₂ : normalize n₂ d₂ z₂; rcases normalize_num_den e₂ with ⟨g₂, zg₂, rfl, rfl⟩
   simp only [add_def]; rw [← normalize_mul_right _ (Nat.mul_ne_zero zg₁ zg₂)]; congr 1
-  · rw [Int.add_mul]; simp [Int.ofNat_mul, Int.mul_assoc, Int.mul_left_comm, Int.mul_comm]
+  · rw [Int.add_mul]; simp [Int.natCast_mul, Int.mul_assoc, Int.mul_left_comm, Int.mul_comm]
   · simp [Nat.mul_left_comm, Nat.mul_comm]
 
 theorem mkRat_add_mkRat (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
@@ -220,8 +220,8 @@ theorem divInt_add_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z
     n₁ /. d₁ + n₂ /. d₂ = (n₁ * d₂ + n₂ * d₁) /. (d₁ * d₂) := by
   rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
   rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
-  simp_all [-Int.natCast_mul, Int.ofNat_eq_zero, Int.neg_eq_zero, divInt_neg', Int.mul_neg,
-    Int.ofNat_mul_ofNat, Int.neg_add, Int.neg_mul, mkRat_add_mkRat]
+  simp_all [← Int.natCast_mul, Int.ofNat_eq_zero, Int.neg_eq_zero, divInt_neg', Int.mul_neg,
+    Int.neg_add, Int.neg_mul, mkRat_add_mkRat]
 
 @[simp] theorem neg_num (a : Rat) : (-a).num = -a.num := rfl
 @[simp] theorem neg_den (a : Rat) : (-a).den = a.den := rfl
@@ -246,7 +246,7 @@ theorem sub_def (a b : Rat) :
         (Nat.dvd_trans (Nat.gcd_dvd_right ..) <|
          Nat.dvd_trans (Nat.gcd_dvd_right ..) (Nat.dvd_mul_left ..)),
       ← normalize_mul_right _ this]; congr 1
-    · simp only [Int.sub_mul, Int.mul_assoc, Int.ofNat_mul_ofNat,
+    · simp only [Int.sub_mul, Int.mul_assoc, ← Int.natCast_mul,
         Nat.div_mul_cancel (Nat.gcd_dvd_left ..), Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]
     · rw [Nat.mul_right_comm, Nat.div_mul_cancel (Nat.gcd_dvd_left ..)]
 
@@ -267,7 +267,7 @@ theorem mul_def (a b : Rat) :
   have H1 : a.num.natAbs.gcd b.den ≠ 0 := Nat.gcd_ne_zero_right b.den_nz
   have H2 : b.num.natAbs.gcd a.den ≠ 0 := Nat.gcd_ne_zero_right a.den_nz
   rw [mk_eq_normalize, ← normalize_mul_right _ (Nat.mul_ne_zero H1 H2)]; congr 1
-  · rw [Int.ofNat_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.tdiv ..),
+  · rw [Int.natCast_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.tdiv ..),
       Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..), Int.mul_assoc,
       Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)]
   · rw [← Nat.mul_assoc, Nat.mul_right_comm, Nat.mul_right_comm (_/_),
@@ -288,7 +288,7 @@ theorem normalize_mul_normalize (n₁ n₂) {d₁ d₂} (z₁ z₂) :
   cases e₁ : normalize n₁ d₁ z₁; rcases normalize_num_den e₁ with ⟨g₁, zg₁, rfl, rfl⟩
   cases e₂ : normalize n₂ d₂ z₂; rcases normalize_num_den e₂ with ⟨g₂, zg₂, rfl, rfl⟩
   simp only [mul_def]; rw [← normalize_mul_right _ (Nat.mul_ne_zero zg₁ zg₂)]; congr 1
-  · simp [Int.ofNat_mul, Int.mul_assoc, Int.mul_left_comm]
+  · simp [Int.natCast_mul, Int.mul_assoc, Int.mul_left_comm]
   · simp [Nat.mul_left_comm, Nat.mul_comm]
 
 theorem mkRat_mul_mkRat (n₁ n₂ : Int) (d₁ d₂) :
@@ -300,8 +300,7 @@ theorem divInt_mul_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z
     (n₁ /. d₁) * (n₂ /. d₂) = (n₁ * n₂) /. (d₁ * d₂) := by
   rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
   rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
-  simp_all [-Int.natCast_mul, divInt_neg', Int.mul_neg, Int.ofNat_mul_ofNat,  Int.neg_mul,
-    mkRat_mul_mkRat]
+  simp_all [← Int.natCast_mul, divInt_neg', Int.mul_neg, Int.neg_mul, mkRat_mul_mkRat]
 
 theorem inv_def (a : Rat) : a.inv = a.den /. a.num := by
   unfold Rat.inv; split

Batteries/Data/String/Lemmas.lean

@@ -300,7 +300,7 @@ theorem revFindAux_of_valid (p) : ∀ l r,
     simp only [utf8Len_reverse, Char.reduceDefault, List.headD_cons] at h1 h2
     simp only [List.reverse_cons, List.append_assoc, List.singleton_append, utf8Len_cons, h2, h1]
     cases p c <;> simp only [Bool.false_eq_true, ↓reduceIte, Bool.not_false, Bool.not_true,
-      List.tail?_cons, Option.map_some']
+      List.tail?_cons, Option.map_some]
     exact revFindAux_of_valid p l (c::r)
 
 theorem revFind_of_valid (p s) :

Batteries/Tactic/Lint/Frontend.lean

@@ -149,7 +149,7 @@ The first `drop_fn_chars` characters are stripped from the filename.
 -/
 def groupedByFilename (results : Std.HashMap Name MessageData) (useErrorFormat : Bool := false) :
     CoreM MessageData := do
-  let sp ← if useErrorFormat then initSrcSearchPath ["."] else pure {}
+  let sp ← if useErrorFormat then getSrcSearchPath else pure {}
   let grouped : Std.HashMap Name (System.FilePath × Std.HashMap Name MessageData) ←
     results.foldM (init := {}) fun grouped declName msg => do
       let mod ← findModuleOf? declName