chore: Let gcongr know about Nat.cast_lt (#15879)

From LeanAPAP

Author: YaelDillies

Mathlib/Computability/AkraBazzi/AkraBazzi.lean

@@ -1053,7 +1053,7 @@ lemma rpow_p_mul_one_sub_smoothingFn_le :
                   case bn_gt_one =>
                     calc 1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
                         _ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
-                        _ < b i * n := by gcongr; rw [Nat.cast_lt]; exact hn
+                        _ < b i * n := by gcongr
                   case le => calc b i * n ≤ 1 * n := by have := R.b_lt_one i; gcongr
                                           _ = n := by rw [one_mul]
                 positivity
@@ -1149,7 +1149,7 @@ lemma rpow_p_mul_one_add_smoothingFn_ge :
                 case bn_gt_one =>
                   calc 1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
                       _ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
-                      _ < b i * n := by gcongr; rw [Nat.cast_lt]; exact hn
+                      _ < b i * n := by gcongr
                 case le => calc b i * n ≤ 1 * n := by have := R.b_lt_one i; gcongr
                                         _ = n := by rw [one_mul]
               positivity

Mathlib/Data/Nat/Cast/Order/Basic.lean

@@ -69,6 +69,9 @@ variable [CharZero α] {m n : ℕ}
 theorem strictMono_cast : StrictMono (Nat.cast : ℕ → α) :=
   mono_cast.strictMono_of_injective cast_injective
 
+@[gcongr]
+lemma _root_.GCongr.natCast_lt_natCast {a b : ℕ} (h : a < b) : (a : α) < b := strictMono_cast h
+
 /-- `Nat.cast : ℕ → α` as an `OrderEmbedding` -/
 @[simps! (config := .asFn)]
 def castOrderEmbedding : ℕ ↪o α :=