From 97f34d8c7dcb950698072a6d2cb42059eac98f74 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Sun, 19 Nov 2023 10:31:55 +0000 Subject: [PATCH] chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now (#8496) According to `git bisect`, #7905 is what made the single `linarith` call work here. --- Archive/Imo/Imo1994Q1.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Archive/Imo/Imo1994Q1.lean b/Archive/Imo/Imo1994Q1.lean index b6a0a2b52d61cb..05c0bdfec40bce 100644 --- a/Archive/Imo/Imo1994Q1.lean +++ b/Archive/Imo/Imo1994Q1.lean @@ -89,11 +89,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1) simp only [mem_map, mem_Icc, mem_Ioc, Fin.zero_le, true_and_iff, Equiv.subLeft_apply, Function.Embedding.coeFn_mk, exists_prop, RelEmbedding.coe_toEmbedding] at hx ⊢ rcases hx with ⟨i, ⟨hi, rfl⟩⟩ - have h1 : a i + a (Fin.last m - k) ≤ n := by - -- Porting note: Original proof was `by linarith only [h, a.monotone hi]` - have := a.monotone hi - simp only at this ⊢ - linarith only [h, this] + have h1 : a i + a (Fin.last m - k) ≤ n := by linarith only [h, a.monotone hi] have h2 : a i + a (Fin.last m - k) ∈ A := hadd _ (ha _) _ (ha _) h1 rw [← mem_coe, ← range_orderEmbOfFin A hm, Set.mem_range] at h2 cases' h2 with j hj