switch proposition names pge and primep in S01_Sets.lean

avigad · Jul 16, 2024 · 7d6f2e2 · 7d6f2e2
1 parent 6b81b19
commit 7d6f2e2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/MIL/C04_Sets_and_Functions/S01_Sets.lean b/MIL/C04_Sets_and_Functions/S01_Sets.lean
@@ -647,8 +647,8 @@ example : (⋃ p ∈ primes, { x | x ≤ p }) = univ := by
   apply eq_univ_of_forall
   intro x
   simp
-  rcases Nat.exists_infinite_primes x with ⟨p, primep, pge⟩
-  use p, pge
+  rcases Nat.exists_infinite_primes x with ⟨p, pge, primep⟩
+  use p, primep
 
 -- BOTH:
 end