Update Basic.lean

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -845,7 +845,7 @@ end deprecated
 is a strong limit by this definition. -/
 structure IsStrongLimit (c : Cardinal) : Prop where
   ne_zero : c ≠ 0
-  two_power_lt : ∀ x < c, 2 ^ x < c
+  two_power_lt {x} : x < c → 2 ^ x < c
 
 protected theorem IsStrongLimit.isSuccLimit {c} (H : IsStrongLimit c) : IsSuccLimit c := by
   rw [Cardinal.isSuccLimit_iff]
@@ -1540,10 +1540,10 @@ theorem aleph0_le_of_isSuccLimit {c : Cardinal} (h : IsSuccLimit c) : ℵ₀ ≤
   contrapose! h
   exact not_isSuccLimit_of_lt_aleph0 h
 
-theorem isStrongLimit_aleph0 : IsStrongLimit ℵ₀ :=
-  ⟨aleph0_ne_zero, fun x hx => by
-    rcases lt_aleph0.1 hx with ⟨n, rfl⟩
-    exact mod_cast nat_lt_aleph0 (2 ^ n)⟩
+theorem isStrongLimit_aleph0 : IsStrongLimit ℵ₀ := by
+  refine ⟨aleph0_ne_zero, fun hx ↦ ?_⟩
+  obtain ⟨n, rfl⟩ := lt_aleph0.1 hx
+  exact_mod_cast nat_lt_aleph0 _
 
 theorem IsStrongLimit.aleph0_le {c} (H : IsStrongLimit c) : ℵ₀ ≤ c :=
   aleph0_le_of_isSuccLimit H.isSuccLimit