diff --git a/Compfiles/Imo1982P3.lean b/Compfiles/Imo1982P3.lean
index c8327cb..1ce1aa6 100644
--- a/Compfiles/Imo1982P3.lean
+++ b/Compfiles/Imo1982P3.lean
@@ -45,19 +45,9 @@ lemma sum_Fin_eq_sum_Ico {x : ℕ → ℝ} {N : ℕ} : ∑ n : Fin N, x n = ∑
 Specialization of Cauchy-Schwarz inequality with the sequences x n / √(y n) and √(y n)
 -/
 theorem Sedrakyan's_lemma {ι : Type*} {s : Finset ι} {x y : ι → ℝ}
-    (hN : 0 < Finset.card s) (_xi_pos : ∀ i ∈ s, 0 < x i) (yi_pos : ∀ i ∈ s, 0 < y i) :
+    (yi_pos : ∀ i ∈ s, 0 < y i) :
     (∑ n ∈ s, x n) ^ 2 / (∑ n ∈ s, y n) ≤ ∑ n ∈ s, (x n) ^ 2 / y n := by
-  have : 0 < ∑ n ∈ s, y n := Finset.sum_pos yi_pos <| Finset.card_pos.mp hN
-  apply le_of_le_of_eq (b := ((∑ n ∈ s, x n ^ 2 / y n) * ∑ n ∈ s, y n) / ∑ n ∈ s, y n)
-  · gcongr
-    convert Finset.sum_mul_sq_le_sq_mul_sq s (fun n ↦ x n / √ (y n)) (fun n ↦ √ (y n)) with n hn n hn n hn
-    all_goals specialize _xi_pos n hn
-    all_goals specialize yi_pos n hn
-    · field_simp
-    · field_simp
-    · rw [Real.sq_sqrt]
-      positivity
-  · field_simp
+  exact Finset.sq_sum_div_le_sum_sq_div s x yi_pos
 
 lemma ineq₁ {x : ℕ → ℝ} {N : ℕ} (hN : 1 < N) (hx : ∀ i , x (i + 1) ≤ x i) :
     x N ≤ (∑ n : Fin (N - 1), x (n + 1)) / (N - 1) := by
@@ -220,7 +210,7 @@ problem iom1982_p3a {x : ℕ → ℝ} (x_pos : ∀ i, x i > (0 : ℝ))
   have sedrakayan's_lemma :
     ∀ N > 0,
     ((∑ n : Fin N, (x n))^2 / (∑ n : Fin N, x (n + 1))) ≤ (∑ n : Fin N, (x n)^2 / x (n + 1)) :=
-    fun N hN => Sedrakyan's_lemma (by simpa) (fun i _ => x_pos i) (fun i _ => x_pos (i + 1))
+    fun N hN => Sedrakyan's_lemma (fun i _ => x_pos (i + 1))
   have :
     ∃ (N : ℕ), 0 < N ∧ 1 < N ∧ 2 < N ∧  (3.999 : ℝ) ≤ 4 * ((N - 1) / N) :=  by use 4000; norm_num
   obtain ⟨N, zero_lt_N, one_lt_N, two_lt_N, ineq₀⟩ := this
diff --git a/Compfiles/Usa1981P5.lean b/Compfiles/Usa1981P5.lean
index 3bbfa0c..1986126 100644
--- a/Compfiles/Usa1981P5.lean
+++ b/Compfiles/Usa1981P5.lean
@@ -61,8 +61,8 @@ problem usa1981_p5 (x : ℝ) (n : ℕ) :
   obtain rfl | hn := Nat.eq_zero_or_pos n
   · simp [a]
 
-  have : Nonempty (Finset.Icc 1 n) := by
-    use 1; rw [Finset.mem_Icc]; simp only [le_refl, true_and]; exact hn
+  have : Nonempty (Finset.Icc 1 n) :=
+    ⟨1, Finset.left_mem_Icc.mpr (Nat.succ_le_of_lt hn)⟩
   obtain ⟨⟨m, hm1⟩, hm2⟩ :=
     Finite.exists_min (fun (m : Finset.Icc 1 n) ↦ a m / m)
 
diff --git a/Compfiles/Usa2002P1.lean b/Compfiles/Usa2002P1.lean
index c366039..4b6433e 100644
--- a/Compfiles/Usa2002P1.lean
+++ b/Compfiles/Usa2002P1.lean
@@ -92,7 +92,7 @@ lemma usa2002_p1_generalized
   · -- Suppose that our claim holds for n = k. Let s ∈ S, |S| = k + 1,
     -- and let S' denote the set of all elements of S other than s.
     intros S hde hft hs N hN
-    have s : S := Nonempty.some (Fintype.card_pos_iff.mp (by rw [hs]; exact Nat.succ_pos k))
+    have s : S := Nonempty.some (Fintype.card_pos_iff.mp (Nat.lt_of_sub_eq_succ hs))
     let S' := { a : S // a ≠ s }
     have hs' : Fintype.card S' = k := by simp [Fintype.card_subtype_compl, hs, S']