some omega shortenings found by tryAtEachStep

dwrensha · Dec 12, 2024 · 4c8f6ae · 4c8f6ae
1 parent d27fad3
commit 4c8f6ae
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 8 deletions.
diff --git a/Compfiles/Usa1987P1.lean b/Compfiles/Usa1987P1.lean
@@ -129,10 +129,7 @@ problem usa1987_p1 (m n : ℤ) :
           simp only [Set.mem_insert_iff, true_or, or_true]
         · obtain rfl : n = -21 := by linarith only [h28]
           simp only [Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true]
-      · obtain rfl : m = -1 := eq_add_of_sub_eq h25
-        norm_num at h6
-        obtain rfl : n = -1 := by linarith only [pow_eq_zero h6.symm]
-        simp only [Set.mem_insert_iff, true_or, or_true]
+      · omega
     · rw [hm'] at h13
       have h21 : 5^2 < m'^2 := by rw [←h13]; norm_num
       have h23 : 5 < m' := lt_of_pow_lt_pow_left₀ 2 hm0' h21

diff --git a/Compfiles/Usa1992P1.lean b/Compfiles/Usa1992P1.lean
@@ -316,10 +316,7 @@ lemma lemma5 {m n : ℕ} (hm : m < 10^n) :
     intro x hx
     simp only [List.map_append, List.mem_append, List.mem_map, complement_digits, m_digits_padded,
                padding, m_digits] at hx
-    obtain ⟨a, ha1, ha2⟩ | ⟨a, ha1, ha2⟩ := hx
-    · omega
-    · simp only [Nat.reduceLeDiff, List.mem_replicate, ne_eq] at ha1
-      omega
+    omega
   have h14 : complement_digits.length ≤ n := by
     simp only [List.map_append, List.length_append, List.length_map, complement_digits,
                m_digits_padded, padding, List.length_replicate, m_digits]