From 347a8864e39b336514127cd2744287fb94677521 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Thu, 24 Aug 2023 18:19:32 -0400
Subject: [PATCH] [Usa1998Q3] simpler proof of lemma2'

---
 MathPuzzles/Usa1998Q3.lean | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

diff --git a/MathPuzzles/Usa1998Q3.lean b/MathPuzzles/Usa1998Q3.lean
index 3abf5698..f7b365fe 100644
--- a/MathPuzzles/Usa1998Q3.lean
+++ b/MathPuzzles/Usa1998Q3.lean
@@ -63,17 +63,7 @@ lemma lemma1 (x : ℝ) (hx : x ∈ Set.Ioo 0 (Real.pi / 2)) :
   · exact hx.2
 
 lemma lemma2' (n : ℕ) : Finset.erase (Finset.range (n + 1)) n = Finset.range n :=
-by ext a
-   rw[Finset.mem_erase, Finset.mem_range, Finset.mem_range]
-   constructor
-   · intro ⟨ha1, ha2⟩
-     obtain h1 | h2 := Iff.mp Order.lt_succ_iff_eq_or_lt ha2
-     · exact (ha1 h1).elim
-     · exact h2
-   · intro ha
-     constructor
-     · exact Nat.ne_of_lt ha
-     · exact Nat.lt_add_right a n 1 ha
+by rw[←Nat.succ_eq_add_one, Finset.range_succ]; simp
 
 lemma lemma2 (f : ℕ → ℝ) :
     ∏ i in Finset.range (n + 1), ∏ j in Finset.erase (Finset.range (n + 1)) i, f j =