Merge pull request #239 from eric-wieser/no-by

Standardize on `:= sorry` not `:= by sorry`

lean4/src/putnam_1963_a3.lean

@@ -15,5 +15,5 @@ theorem putnam_1963_a3
     (f y : ℝ → ℝ)
     (hf : ContinuousOn f (Ici 1)) :
     ContDiffOn ℝ n y (Ici 1) ∧ (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔
-    ∀ x ≥ 1, y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t := by
+    ∀ x ≥ 1, y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t :=
   sorry

lean4/src/putnam_1963_a4.lean

@@ -10,5 +10,5 @@ theorem putnam_1963_a4
     (T_def : ∀ a n, T a n = n * ((1 + a (n + 1)) / a n - 1))
     (P : (ℕ → ℝ) → ℝ → Prop)
     (P_def : ∀ a C, P a C ↔ C ≤ limsup (T a) atTop ∨ ¬ BddAbove (range (T a))) :
-    (∀ a, (∀ n, 0 < a n) → P a 1) ∧ (∀ C > 1, ∃ a, (∀ n, 0 < a n) ∧ ¬ P a C) := by
+    (∀ a, (∀ n, 0 < a n) → P a 1) ∧ (∀ C > 1, ∃ a, (∀ n, 0 < a n) ∧ ¬ P a C) :=
   sorry

lean4/src/putnam_1968_a3.lean

@@ -15,5 +15,5 @@ theorem putnam_1968_a3
     ∃ (n : ℕ) (s : Fin (2 ^ n) → Set α),
       s 0 = ∅ ∧
       (∀ t, ∃! i, s i = t) ∧
-      (∀ i, i + 1 < 2 ^ n → (s i ∆ s (i + 1)).ncard = 1) := by
+      (∀ i, i + 1 < 2 ^ n → (s i ∆ s (i + 1)).ncard = 1) :=
   sorry

lean4/src/putnam_1969_a5.lean

@@ -17,5 +17,5 @@ theorem putnam_1969_a5
       x 0 = x0 ∧
       y 0 = y0 ∧
       x t = 0 ∧
-      y t = 0 := by
+      y t = 0 :=
   sorry

lean4/src/putnam_1989_b3.lean

@@ -28,5 +28,5 @@ theorem putnam_1989_b3
     (μ_def : ∀ n, μ n = ∫ x in Set.Ioi 0, x ^ n * f x) :
     (∀ n, μ n = putnam_1989_b3_solution n (μ 0)) ∧
     (∃ L, Tendsto (fun n ↦ (μ n) * 3 ^ n / n !) atTop (𝓝 L)) ∧
-    (Tendsto (fun n ↦ (μ n) * 3 ^ n / n !) atTop (𝓝 0) → μ 0 = 0) := by
+    (Tendsto (fun n ↦ (μ n) * 3 ^ n / n !) atTop (𝓝 0) → μ 0 = 0) :=
   sorry

lean4/src/putnam_1990_a6.lean

@@ -10,5 +10,5 @@ If $X$ is a finite set, let $|X|$ denote the number of elements in $X$. Call an
 theorem putnam_1990_a6 :
     ((Finset.univ : Finset <| Finset (Set.Icc 1 10) × Finset (Set.Icc 1 10)).filter
       fun ⟨S, T⟩ ↦ (∀ s ∈ S, T.card < s) ∧ (∀ t ∈ T, S.card < t)).card =
-    putnam_1990_a6_solution := by
+    putnam_1990_a6_solution :=
   sorry

lean4/src/putnam_2003_b3.lean

@@ -6,5 +6,5 @@ open MvPolynomial Set Nat
 Show that for each positive integer $n$, $n!=\prod_{i=1}^n \text{lcm}\{1,2,\dots,\lfloor n/i \rfloor\}$. (Here lcm denotes the least common multiple, and $\lfloor x \rfloor$ denotes the greatest integer $\leq x$.)
 -/
 theorem putnam_2003_b3 (n : ℕ) :
-    n ! = ∏ i in Finset.Icc 1 n, ((List.range ⌊n / i⌋₊).map succ).foldl Nat.lcm 1 := by
+    n ! = ∏ i in Finset.Icc 1 n, ((List.range ⌊n / i⌋₊).map succ).foldl Nat.lcm 1 :=
   sorry

lean4/src/putnam_2018_a3.lean

@@ -8,5 +8,5 @@ Determine the greatest possible value of $\sum_{i=1}^{10} \cos(3x_i)$ for real n
 theorem putnam_2018_a3 :
     IsGreatest
       {∑ i, Real.cos (3 * x i) | (x : Fin 10 → ℝ) (hx : ∑ i, Real.cos (x i) = 0)}
-      putnam_2018_a3_solution := by
+      putnam_2018_a3_solution :=
   sorry

lean4/src/putnam_2022_b1.lean

@@ -11,5 +11,5 @@ theorem putnam_2022_b1
     (Pconst : P.coeff 0 = 0)
     (Podd : Odd (P.coeff 1))
     (hB : ∀ x : ℝ, HasSum (fun i => b i * x ^ i) (Real.exp (aeval x P))) :
-    ∀ k : ℕ, b k ≠ 0 := by
+    ∀ k : ℕ, b k ≠ 0 :=
   sorry

lean4/src/putnam_2023_b3.lean

@@ -16,5 +16,5 @@ theorem putnam_2023_b3
     (hn : 2 ≤ n)
     (a : (Fin n → Icc (0 : ℝ) 1) → ℕ)
     (ha : ∀ x, IsGreatest {k | ∃ i : Fin k ↪o Fin n, IsZigZag ((↑) ∘ x ∘ i)} (a x)) :
-    𝔼[(↑) ∘ a] = putnam_2023_b3_solution n := by
+    𝔼[(↑) ∘ a] = putnam_2023_b3_solution n :=
   sorry