fix test

leanprover-community · Feb 4, 2025 · 51879e1 · 51879e1
1 parent c2681ef
commit 51879e1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/test/Mathlib/test/H20231020.in b/test/Mathlib/test/H20231020.in
@@ -2,7 +2,7 @@
 
 {"cmd": "theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num", "env": 0}
 
-{"cmd": "theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})", "env": 0}
+{"cmd": "theorem mathd_numbertheory_403 : ∑ k ∈ (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})", "env": 0}
 
-{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]", "env": 0}
+{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k ∈ Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]", "env": 0}
 
diff --git a/test/Mathlib/test/H20231020.lean b/test/Mathlib/test/H20231020.lean
@@ -17,6 +17,6 @@ open Topology
 
 theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num
 
-theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})
+theorem mathd_numbertheory_403 : ∑ k ∈ (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})
 
-theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]
+theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k ∈ Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]