From a14d999daef394324c4fc99087a78e7c165c884a Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Wed, 11 Dec 2024 17:53:22 -0500
Subject: [PATCH] some simplifications suggested by tryAtEachStep

---
 Compfiles/Imo1962P1.lean  |  3 +--
 Compfiles/Imo2023P4.lean  |  3 +--
 Compfiles/Iran1998P9.lean | 16 +++-------------
 Compfiles/Usa2015P1.lean  |  4 +---
 4 files changed, 6 insertions(+), 20 deletions(-)

diff --git a/Compfiles/Imo1962P1.lean b/Compfiles/Imo1962P1.lean
index 1676ad76..3f8550df 100644
--- a/Compfiles/Imo1962P1.lean
+++ b/Compfiles/Imo1962P1.lean
@@ -137,8 +137,7 @@ theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846
     · exfalso; exact case_4_digit h h2
     · have h4 : c = 15384 := case_5_digit h h2
       have h5 : n = 10 * 15384 + 6 := h4 ▸ h2.left
-      norm_num at h5
-      exact h5.ge
+      exact Nat.le_of_eq h5.symm
 
 snip end
 
diff --git a/Compfiles/Imo2023P4.lean b/Compfiles/Imo2023P4.lean
index 7fe2851c..18812168 100644
--- a/Compfiles/Imo2023P4.lean
+++ b/Compfiles/Imo2023P4.lean
@@ -287,8 +287,7 @@ theorem imo2023_p4_generalized
           obtain ⟨aa, haa, haa2, haa3⟩ := ha
           simp only [e] at haa3
           rw [← haa3]
-          simp only [Subtype.mk_le_mk]
-          omega
+          exact Subtype.mk_le_mk.mpr haa
         · intro ha
           simp only [Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach,
                      true_and] at ha
diff --git a/Compfiles/Iran1998P9.lean b/Compfiles/Iran1998P9.lean
index 33173a88..c3abc514 100644
--- a/Compfiles/Iran1998P9.lean
+++ b/Compfiles/Iran1998P9.lean
@@ -68,12 +68,7 @@ problem iran1998_p9
 
   have hv₁ : ‖v₁‖ = Real.sqrt (x + y + z) := by
     have hn := compute_norm v₁
-    have h1: ((∑ i : Fin 3, ((v₁ i) ^ 2)) : ℝ) = (v₁ 0)^2 + (v₁ 1)^2 + (v₁ 2)^2 := by
-      rw[Fin.sum_univ_succ, Fin.sum_univ_succ, Fin.sum_univ_one]
-      ring_nf
-      norm_cast
-
-    rw [h1] at hn
+    rw [Fin.sum_univ_three] at hn
     have hv1 : v₁ 0 = Real.sqrt x := rfl
     have hv2 : v₁ 1 = Real.sqrt y := rfl
     have hv3 : v₁ 2 = Real.sqrt z := rfl
@@ -86,11 +81,7 @@ problem iran1998_p9
 
   have hv₂ : ‖v₂‖ = 1 := by
     have hn := compute_norm v₂
-    have h2: ((∑ i : Fin 3, ((v₂ i) ^ 2)) : ℝ) = (v₂ 0)^2 + (v₂ 1)^2 + (v₂ 2)^2 := by
-      rw[Fin.sum_univ_succ, Fin.sum_univ_succ, Fin.sum_univ_one]
-      ring_nf
-      norm_cast
-    rw [h2] at hn
+    rw [Fin.sum_univ_three] at hn
     have hv1 : v₂ 0 = Real.sqrt ((x-1)/x) := rfl
     have hv2 : v₂ 1 = Real.sqrt ((y-1)/y) := rfl
     have hv3 : v₂ 2 = Real.sqrt ((z-1)/z) := rfl
@@ -117,8 +108,7 @@ problem iran1998_p9
   have hinner :=
     calc ((inner v₁ v₂): ℝ)
           = ∑ i : Fin 3, v₁ i * v₂ i := rfl
-        _ = v₁ 0 * v₂ 0 + v₁ 1 * v₂ 1 + v₁ 2 * v₂ 2 :=
-               by rw[Fin.sum_univ_succ, Fin.sum_univ_succ, Fin.sum_univ_one]; ring_nf; simp
+        _ = v₁ 0 * v₂ 0 + v₁ 1 * v₂ 1 + v₁ 2 * v₂ 2 := Fin.sum_univ_three _
         _ = Real.sqrt x * Real.sqrt ((x - 1) / x) +
             Real.sqrt y * Real.sqrt ((y - 1) / y) +
             Real.sqrt z * Real.sqrt ((z - 1) / z) := rfl
diff --git a/Compfiles/Usa2015P1.lean b/Compfiles/Usa2015P1.lean
index b7c34ec8..116d6e8a 100644
--- a/Compfiles/Usa2015P1.lean
+++ b/Compfiles/Usa2015P1.lean
@@ -84,9 +84,7 @@ problem usa2015_p1 (x y : ℤ) :
       rw [this, ht4] at ht
       have : y = 3 := by linarith only [ht]
       simp [*]; use 1; simp
-    · have : t - 2 ≠ 0 := by intro; apply ht4; linarith
-      have hn := abc (by positivity) ht3
-      obtain ⟨d, hd⟩ := hn
+    · obtain ⟨d, hd⟩ := abc (sub_ne_zero_of_ne ht4) ht3
       have Odd_dd : Odd (d ^ 2) := by
         rw [←hd]; apply Even.add_one; apply Even.mul_right; exact Int.even_iff.mpr rfl
       have Odd_d  : Odd d := (Int.odd_pow' (by positivity)).mp Odd_dd