fix tests

Author: kim-em

tests/lean/run/4313.lean

@@ -21,7 +21,7 @@ theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n
   rw [bmod_def x n]
   split -- `split` now generates the more meaningful `isTrue` and `isFalse` tags.
   case isTrue p =>
-    simp only [emod_add_bmod_congr]
+    simp only [emod_add_bmod]
   case isFalse p =>
     rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg]
     simp

tests/lean/run/partial_fixpoint_induct.lean

@@ -183,7 +183,7 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
       have : r = 0 := by simp_all
       simp_all
     next =>
-      simp only [Option.map_eq_map, Option.map_eq_some'] at hsome
+      simp only [Option.map_eq_map, Option.map_eq_some_iff] at hsome
       obtain ⟨r', hr, rfl⟩ := hsome
       specialize ih _ _ hr
       simpa

tests/lean/run/simpConfigPropagationIssue1.lean

@@ -2,12 +2,12 @@ namespace Option
 
 variable {α : Type _}
 
-instance liftOrGet_isCommutative (f : α → α → α) [Std.Commutative f] :
-    Std.Commutative (liftOrGet f) :=
-  ⟨fun a b ↦ by cases a <;> cases b <;> simp [liftOrGet, Std.Commutative.comm]⟩
+instance merge_isCommutative (f : α → α → α) [Std.Commutative f] :
+    Std.Commutative (merge f) :=
+  ⟨fun a b ↦ by cases a <;> cases b <;> simp [merge, Std.Commutative.comm]⟩
 
-instance liftOrGet_isAssociative (f : α → α → α) [Std.Associative f] :
-    Std.Associative (liftOrGet f) :=
-  ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [liftOrGet, Std.Associative.assoc]⟩
+instance merge_isAssociative (f : α → α → α) [Std.Associative f] :
+    Std.Associative (merge f) :=
+  ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [merge, Std.Associative.assoc]⟩
 
 end Option