chore: bump toolchain to v4.19.0-rc2 (#1188)

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>

Author: 10 people

Batteries/Data/Nat/Gcd.lean

@@ -42,7 +42,7 @@ theorem Coprime.gcd_mul_left_cancel (m : Nat) (H : Coprime k n) : gcd (k * m) n
     rw [Coprime, Nat.gcd_assoc, H.symm.gcd_eq_one, gcd_one_right]
   Nat.dvd_antisymm
     (dvd_gcd (H1.dvd_of_dvd_mul_left (gcd_dvd_left _ _)) (gcd_dvd_right _ _))
-    (gcd_dvd_gcd_mul_left _ _ _)
+    (gcd_dvd_gcd_mul_left_left _ _ _)
 
 theorem Coprime.gcd_mul_right_cancel (m : Nat) (H : Coprime k n) : gcd (m * k) n = gcd m n := by
   rw [Nat.mul_comm m k, H.gcd_mul_left_cancel m]

Batteries/Data/Nat/Lemmas.lean

@@ -197,7 +197,7 @@ theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by
   apply testBit_lt_two_pow
   apply Nat.lt_of_lt_of_le
   · exact ofBits_lt_two_pow f
-  · exact pow_le_pow_right Nat.zero_lt_two h
+  · exact Nat.pow_le_pow_right Nat.zero_lt_two h
 
 theorem testBit_ofBits (f : Fin n → Bool) :
     (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false := by

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.19.0-rc1
+leanprover/lean4:v4.19.0-rc2