[Usa1998Q3] simpler proof of lemma2'

dwrensha · Aug 24, 2023 · 347a886 · 347a886
1 parent c85ec1f
commit 347a886
Showing 1 changed file with 1 addition and 11 deletions.
diff --git 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 =