From 4c8f6aec3d071c11ae8f77812670eeee9136d9c6 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Thu, 12 Dec 2024 16:55:36 -0500 Subject: [PATCH] some omega shortenings found by tryAtEachStep --- Compfiles/Usa1987P1.lean | 5 +---- Compfiles/Usa1992P1.lean | 5 +---- 2 files changed, 2 insertions(+), 8 deletions(-) diff --git a/Compfiles/Usa1987P1.lean b/Compfiles/Usa1987P1.lean index a8a0e2a..e4c3815 100644 --- 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 index b898bb7..f830df3 100644 --- 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]