chore: fix rebase issues

We added this option to ensure `simproc`s do not invoke `whnf`.
`simp` is already reducing the terms.

src/Init/ByCases.lean

@@ -57,7 +57,8 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 -- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
 theorem ite_some_none_eq_none [Decidable P] :
     (if P then some x else none) = none ↔ ¬ P := by
-  simp only [ite_eq_right_iff]
+  have : some x ≠ none := Option.noConfusion
+  simp only [ite_eq_right_iff, this]
   rfl
 
 @[simp] theorem ite_some_none_eq_some [Decidable P] :

src/Init/Data/AC.lean

@@ -260,7 +260,7 @@ theorem Context.evalList_sort (ctx : Context α) (h : ContextInformation.isComm
     simp [ContextInformation.isComm, Option.isSome] at h
     match h₂ : ctx.comm with
     | none =>
-      simp only [h₂] at h
+      simp [h₂] at h
     | some val =>
       simp [h₂] at h
       exact val.down

src/Init/Data/BitVec/Lemmas.lean

@@ -990,8 +990,9 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (
     x.signExtend v = x.zeroExtend v := by
   ext i
   by_cases hv : i < v
-  · simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
-      BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte]
+  · have : (false = true) = False := by simp
+    simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
+      BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, this]
     rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
     simp [BitVec.testBit_toNat]
   · simp only [getLsb_zeroExtend, hv, decide_False, Bool.false_and]

src/Init/Data/List/Count.lean

@@ -47,11 +47,11 @@ theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a
     if h : p x then
       rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
       · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
-      · simp only [h, not_true_eq_false, decide_False, not_false_eq_true]
+      · simp [h, not_true_eq_false, decide_False, not_false_eq_true]
     else
       rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
       · rfl
-      · simp only [h, not_false_eq_true, decide_True]
+      · simp [h, not_false_eq_true, decide_True]
 
 theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
   induction l with
@@ -234,7 +234,7 @@ theorem count_erase (a b : α) :
       rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
     else
       have hc_beq := beq_false_of_ne hc
-      simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
+      simp [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
       if ha : b = a then
         rw [ha, eq_comm] at hc
         rw [if_pos ((beq_iff_eq _ _).2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]

src/Init/Data/List/Erase.lean

@@ -39,13 +39,13 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er
   | cons x xs ih =>
     simp only [eraseP_cons, cond_eq_if]
     split <;> rename_i h
-    · simp only [false_or]
+    · simp
       constructor
       · rintro rfl
         simpa
       · rintro ⟨_, _, rfl, rfl⟩
         rfl
-    · simp only [cons.injEq, false_or, false_iff, not_exists, not_and]
+    · simp
       rintro x h' rfl
       simp_all
 

src/Init/Data/List/Find.lean

@@ -737,10 +737,10 @@ theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
+    simp [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
     split
     · simp_all
-    · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone]
+    · simp_all [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone]
       simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map]
 
 theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :

src/Init/Data/List/Lemmas.lean

@@ -639,7 +639,7 @@ theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α
       exact Nat.succ_le_succ_iff.mp h
 
 @[simp] theorem set_eq_nil (l : List α) (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by
-  cases l <;> cases n <;> simp only [set]
+  cases l <;> cases n <;> simp [set]
 
 theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
     (l.set n a).set m b = (l.set m b).set n a
@@ -1874,7 +1874,7 @@ theorem join_eq_append (xs : List (List α)) (ys zs : List α) :
   · induction xs generalizing ys with
     | nil =>
       simp only [join_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
-        exists_false, or_false, and_imp]
+        exists_false, or_false, and_imp, List.cons_ne_nil]
       rintro rfl rfl
       exact ⟨[], [], by simp⟩
     | cons x xs ih =>

src/Init/Data/List/Nat/Range.lean

@@ -200,7 +200,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
       cases k with
       | zero => simp [range'_succ]
       | succ k =>
-        simp only [range'_succ, false_and, cons.injEq, true_and, ih, exists_eq_left', false_or]
+        simp [range'_succ, ih, exists_eq_left']
         refine ⟨k, ?_⟩
         simp_all
         omega

src/Init/Data/List/Pairwise.lean

@@ -123,7 +123,7 @@ theorem pairwise_filterMap (f : β → Option α) {l : List β} :
   match e : f a with
   | none =>
     rw [filterMap_cons_none e, pairwise_cons]
-    simp only [e, false_implies, implies_true, true_and, IH]
+    simp [e, false_implies, implies_true, true_and, IH]
   | some b =>
     rw [filterMap_cons_some e]
     simpa [IH, e] using fun _ =>

src/Init/Data/List/Sort/Lemmas.lean

@@ -136,7 +136,7 @@ theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.1
       simp only [map_cons, cons.injEq, true_and]
       rw [merge_stable, map_cons]
       exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my
-    · simp only [↓reduceIte, map_cons, cons.injEq, true_and]
+    · simp [↓reduceIte, map_cons, cons.injEq, true_and]
       rw [merge_stable, map_cons]
       exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)
 

src/Init/Data/List/Sublist.lean

@@ -767,7 +767,7 @@ theorem prefix_cons_iff : l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ t, l₁ = a :
         refine ⟨s, by simp [h']⟩
 
 @[simp] theorem cons_prefix_cons : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := by
-  simp only [prefix_cons_iff, cons.injEq, false_or]
+  simp only [prefix_cons_iff, cons.injEq, false_or, List.cons_ne_nil]
   constructor
   · rintro ⟨t, ⟨rfl, rfl⟩, h⟩
     exact ⟨rfl, h⟩

src/Init/Data/Nat/Basic.lean

@@ -887,7 +887,7 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
 
 theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
   | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
-  | 0, succ b, _ => by simp only [Nat.sub_zero, ne_eq, not_false_eq_true]
+  | 0, succ b, _ => by simp only [Nat.sub_zero, ne_eq, not_false_eq_true, Nat.succ_ne_zero]
   | succ a, 0, h => absurd h (Nat.not_lt_zero a.succ)
   | succ a, succ b, h => by rw [Nat.succ_sub_succ]; exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -123,7 +123,7 @@ theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i
     match mod_two_eq_zero_or_one x with
     | Or.inl mod2_eq =>
       rw [←div_add_mod x 2] at xnz
-      simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
+      simp [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
       have ⟨d, dif⟩   := hyp x_pos xnz
       apply Exists.intro (d+1)
       simp_all
@@ -209,7 +209,7 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
   have x_ge_n := Nat.ge_of_not_lt not_lt
   have ⟨i, ⟨i_ge_n, test_true⟩⟩ := ge_two_pow_implies_high_bit_true x_ge_n
   have test_false := p _ i_ge_n
-  simp only [test_true] at test_false
+  simp [test_true] at test_false
 
 private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
   induction x with

src/Init/Data/Nat/Div.lean

@@ -221,7 +221,7 @@ theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by
   induction y, k using mod.inductionOn generalizing x with
     (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
   | base y k h =>
-    simp only [add_one, succ_mul, false_iff, Nat.not_le]
+    simp only [add_one, succ_mul, false_iff, Nat.not_le, Nat.succ_ne_zero]
     refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..)
     exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
   | ind y k h IH =>

src/Init/Data/Option/Lemmas.lean

@@ -162,7 +162,7 @@ theorem map_some : f <$> some a = some (f a) := rfl
 theorem map_eq_some : f <$> x = some b ↔ ∃ a, x = some a ∧ f a = b := map_eq_some'
 
 @[simp] theorem map_eq_none' : x.map f = none ↔ x = none := by
-  cases x <;> simp only [map_none', map_some', eq_self_iff_true]
+  cases x <;> simp [map_none', map_some', eq_self_iff_true]
 
 theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome := by
   cases x <;> simp

src/Lean/Meta/CtorRecognizer.lean

@@ -82,7 +82,13 @@ def constructorApp'? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr))
       else return some (val, #[mkNatAdd e (toExpr (k-1))])
   else if let some r ← constructorApp? e then
     return some r
-  else
+  else try
+    /-
+    We added the `try` block here because `whnf` fails at terms `n ^ m`
+    when `m` is a big numeral, and `n` is a numeral. This is a little bit hackish.
+    -/
     constructorApp? (← whnf e)
+  catch _ =>
+    return none
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean

@@ -75,3 +75,14 @@ builtin_dsimproc ↓ [simp, seval] dreduceDIte (dite _ _ _) := fun e => do
     | Decidable.isFalse _ h => return .visit (mkApp eb h).headBeta
     | _ => return .continue
   return .continue
+
+builtin_simproc [simp, seval] reduceCtorEq (_ = _) := fun e => withReducibleAndInstances do
+  let_expr Eq _ lhs rhs ← e | return .continue
+  match (← constructorApp'? lhs), (← constructorApp'? rhs) with
+  | some (c₁, _), some (c₂, _) =>
+    if c₁.name != c₂.name then
+      withLocalDeclD `h e fun h =>
+        return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
+    else
+      return .continue
+  | _, _ => return .continue

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -255,19 +255,6 @@ where
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
-def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
-  match e.eq? with
-  | none => return .continue
-  | some (_, lhs, rhs) =>
-    match (← constructorApp'? lhs), (← constructorApp'? rhs) with
-    | some (c₁, _), some (c₂, _) =>
-      if c₁.name != c₂.name then
-        withLocalDeclD `h e fun h =>
-          return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
-      else
-        return .continue
-    | _, _ => return .continue
-
 @[inline] def simpUsingDecide : Simproc := fun e => do
   unless (← getConfig).decide do
     return .continue
@@ -446,8 +433,7 @@ partial def preSEval (s : SimprocsArray) : Simproc :=
 def postSEval (s : SimprocsArray) : Simproc :=
   rewritePost >>
   userPostSimprocs s >>
-  sevalGround >>
-  simpCtorEq
+  sevalGround
 
 def mkSEvalMethods : CoreM Methods := do
   let s ← getSEvalSimprocs
@@ -515,7 +501,6 @@ def postDefault (s : SimprocsArray) : Simproc :=
   userPostSimprocs s >>
   simpGround >>
   simpArith >>
-  simpCtorEq >>
   simpUsingDecide
 
 /--

src/Std/Sat/AIG/RelabelNat.lean

@@ -137,7 +137,7 @@ theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap
     next idx' _ _ =>
     replace hidx : idx ≤ idx' := by omega
     cases Nat.eq_or_lt_of_le hidx with
-    | inl hidxeq => simp only [hidxeq, ih3] at heq
+    | inl hidxeq => simp [hidxeq, ih3] at heq
     | inr hlt => apply ih4 <;> assumption
   | gate ih1 ih2 ih3 ih4 =>
     next idx' _ _ _ _ _ =>

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -155,7 +155,7 @@ theorem isUnit_iff (c : DefaultClause n) (l : Literal (PosFin n)) :
   split
   · next l' heq => simp [heq]
   · next hne =>
-    simp only [false_iff]
+    simp [false_iff]
     apply hne
 
 def negate (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate
@@ -183,13 +183,13 @@ def insert (c : DefaultClause n) (l : Literal (PosFin n)) : Option (DefaultClaus
         · apply Or.inr
           constructor
           · intro heq
-            simp only [← heq] at hl
+            simp [← heq] at hl
           · simpa [hl, ← l'_eq_l] using heq1
         · simp only [Bool.not_eq_true] at hl
           apply Or.inl
           constructor
           · intro heq
-            simp only [← heq] at hl
+            simp [← heq] at hl
           · simpa [hl, ← l'_eq_l] using heq1
       · next l'_ne_l =>
         have := c.nodupkey l'
@@ -250,14 +250,14 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
     intro c' heq
     simp only [Fin.getElem_fin, fold_fn] at heq
     split at heq
-    · simp only at heq
+    · simp at heq
     · next acc =>
       specialize ih acc rfl
       rcases ih with ⟨hsize, ih⟩
       simp only at ih
       simp only [insert] at heq
       split at heq
-      · exact False.elim heq
+      · simp at heq
       · split at heq
         · next h_dup =>
           exfalso -- h_dup contradicts arrNodup

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -154,9 +154,9 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
               exact cOpt_in_arr
             · next b_eq_false =>
               simp only [Bool.not_eq_true] at b_eq_false
-              simp only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos] at h
+              simp [hasAssignment, b_eq_false, ite_false, hasNeg_addPos] at h
               specialize ih l false
-              simp only [hasAssignment, ite_false] at ih
+              simp [hasAssignment, ite_false] at ih
               rw [b_eq_false, Subtype.ext i_eq_l]
               exact ih h
           · next i_ne_l =>
@@ -302,8 +302,8 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
             · next b_eq_false =>
               simp only [Bool.not_eq_true] at b_eq_false
               exact b_eq_false
-          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos] at hb
-          simp only [hasAssignment, b_eq_false, ite_false, hb]
+          simp [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos] at hb
+          simp [hasAssignment, b_eq_false, ite_false, hb]
         · next l_ne_i =>
           simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
           exact hb
@@ -508,9 +508,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               simp only [← heq, not] at l_ne_b
-              split at l_ne_b
-              · simp only at l_ne_b
-              · simp only at l_ne_b
+              split at l_ne_b <;> simp at l_ne_b
             · next id_ne_idx => simp [id_ne_idx]
           · exact hf
         · exact Or.inr hf
@@ -551,7 +549,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
     · simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl
       split
       · next some_eq_none =>
-        simp only at some_eq_none
+        simp at some_eq_none
       · next l _ _ heq =>
         simp only [Option.some.injEq] at heq
         rw [heq] at hl
@@ -565,7 +563,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           simp only [deleteOne]
           split
           · next heq2 =>
-            simp only [heq] at heq2
+            simp [heq] at heq2
           · next l _ _ heq2 =>
             simp only [heq, Option.some.injEq] at heq2
             rw [heq2] at hl
@@ -608,9 +606,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               specialize hl i
               simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
                 Bool.not_eq_false, Bool.not_eq_true] at hl
-              by_cases b_val : b
-              · simp only [b_val, and_false] at hl
-              · simp only [b_val, false_and] at hl
+              by_cases b_val : b <;> simp [b_val] at hl
             · next id_ne_idx => simp [id_ne_idx]
           · exact hf
         · exact Or.inr hf
@@ -663,7 +659,7 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
         rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩
         rw [List.getElem_set] at h4
         split at h4
-        · exact False.elim h4
+        · simp at h4
         · rw [← h4]
           apply List.getElem_mem
       · exact h1

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -17,6 +17,9 @@ namespace Internal
 
 namespace DefaultFormula
 
+-- TODO: remove aux lemma after update-stage0
+private theorem false_ne_true : (false = true) = False := by simp
+
 open Std.Sat
 open DefaultClause DefaultFormula Assignment ReduceResult
 
@@ -34,7 +37,7 @@ theorem mem_of_necessary_assignment {n : Nat} {p : (PosFin n) → Bool} {c : Def
     · next heq => simp [Literal.negate, ← heq, h, v_in_c]
     · next hne =>
       exfalso
-      simp only [(· ⊨ ·), h] at pv
+      simp [(· ⊨ ·), h] at pv
   · specialize p'_not_entails_c v
     have h := p'_not_entails_c.2 v_in_c
     simp only [(· ⊨ ·), Bool.not_eq_false] at h
@@ -42,7 +45,7 @@ theorem mem_of_necessary_assignment {n : Nat} {p : (PosFin n) → Bool} {c : Def
     · next heq => simp [Literal.negate, ← heq, h, v_in_c]
     · next hne =>
       exfalso
-      simp only [(· ⊨ ·), h] at pv
+      simp [(· ⊨ ·), h] at pv
 
 theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c : DefaultClause n}
     {l : Literal (PosFin n)} (p_entails_cl : p ⊨ c.delete (Literal.negate l)) :
@@ -187,8 +190,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
     simp only [Fin.getElem_fin] at h1 h2
     simp only [(· ⊨ ·), h1, Clause.toList, unit_eq, List.mem_singleton, Prod.mk.injEq,
       and_false, false_and, and_true, false_or, h2, or_false, j1_unit, j2_unit] at hp1 hp2
-    simp_all only [Bool.decide_eq_false, Bool.not_eq_true', ne_eq, Fin.getElem_fin, Prod.mk.injEq,
-      and_false, false_and, and_true, false_or, or_false]
+    simp_all
     simp [hp2.1, ← hp1.1, hp1.2] at hp2
 
 theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
@@ -200,8 +202,7 @@ theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
   intro fc confirmRupHint_fold_res confirmRupHint_success
   let motive := ConfirmRupHintFoldEntailsMotive fc.1
   have h_base : motive 0 (fc.fst.assignments, [], false, false) := by
-    simp only [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRatUnits, hf.2.1,
-      false_implies, and_true, true_and, fc, motive]
+    simp [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRatUnits, hf.2.1, fc, motive]
     have fc_satisfies_AssignmentsInvariant : AssignmentsInvariant fc.1 :=
       assignmentsInvariant_insertRatUnits f hf (negate c)
     exact limplies_of_assignmentsInvariant fc.1 fc_satisfies_AssignmentsInvariant
@@ -225,7 +226,7 @@ theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
     rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
     · simp only [negate_eq, List.mem_map, Prod.exists, Bool.exists_bool] at v_in_neg_c
       rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
-      · simp only [Literal.negate, Bool.not_false, Prod.mk.injEq, and_false] at v'_eq_v
+      · simp [Literal.negate] at v'_eq_v
       · simp only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_true] at v'_eq_v
         simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists,
           Bool.exists_bool, ← unsat_c_eq, not_exists, not_or, not_and] at p_unsat_c
@@ -253,7 +254,7 @@ theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
         simp only [(· ⊨ ·), Bool.not_eq_true] at pv
         simp only [p_unsat_c] at pv
         cases pv
-      · simp only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_false] at v'_eq_v
+      · simp [Literal.negate] at v'_eq_v
     · simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf
       exact p_unsat_c <| pf unsat_c unsat_c_in_f
 
@@ -284,7 +285,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
     have p_entails_i_true := hf.2.2 i true hpos p pf
     have p_entails_i_false := hf.2.2 i false hneg p pf
     simp only [Entails.eval] at p_entails_i_true p_entails_i_false
-    simp only [p_entails_i_true] at p_entails_i_false
+    simp [p_entails_i_true] at p_entails_i_false
   · simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe]
     apply Exists.intro i
     have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
@@ -302,7 +303,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
       apply And.intro i_false_in_c
       simp only [addAssignment, ← b_eq_true, addPosAssignment, ite_true] at h2
       split at h2
-      · simp only at h2
+      · simp at h2
       · next heq =>
         have hasNegAssignment_fi : hasAssignment false (f.assignments[i.1]'i_in_bounds) := by
           simp (config := { decide := true }) only [hasAssignment, hasPosAssignment, heq]
@@ -313,11 +314,11 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
         exfalso
         rw [heq] at h3
         exact h3 (has_both b)
-      · simp only at h2
+      · simp at h2
     · apply Or.inr
       rw [i'_eq_i] at i_true_in_c
       apply And.intro i_true_in_c
-      simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false] at h2
+      simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, false_ne_true] at h2
       split at h2
       · next heq =>
         have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by
@@ -325,12 +326,12 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
         have p_entails_i := hf.2.2 i true hasPosAssignment_fi p pf
         simp only [(· ⊨ ·)] at p_entails_i
         exact p_entails_i
-      · simp only at h2
+      · simp at h2
       · next heq =>
         exfalso
         rw [heq] at h3
         exact h3 (has_both b)
-      · simp only at h2
+      · simp at h2
   · exfalso
     have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
       have i_rw : i = ⟨i.1, i.2⟩ := rfl
@@ -376,7 +377,7 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (
   simp only [performRupCheck]
   let motive := ConfirmRupHintFoldEntailsMotive f
   have h_base : motive 0 (f.assignments, [], false, false) := by
-    simp only [ConfirmRupHintFoldEntailsMotive, f_AssignmentsInvariant.1, false_implies, and_true, true_and,
+    simp [ConfirmRupHintFoldEntailsMotive, f_AssignmentsInvariant.1,
       limplies_of_assignmentsInvariant f f_AssignmentsInvariant, motive]
   have h_inductive (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (ih : motive idx.1 acc) :=
     confirmRupHint_preserves_motive f rupHints idx acc ih
@@ -407,14 +408,14 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (
     rw [hb] at h
     by_cases pi : p i
     · exact pi
-    · simp only [Bool.not_eq_true] at pi
-      simp only [pi, decide_True, h] at h1
+    · simp at pi
+      simp [pi, decide_True, h] at h1
   · simp only [Bool.not_eq_true] at hb
     rw [hb]
     rw [hb] at h
     by_cases pi : p i
-    · simp only [pi, decide_False, h] at h1
-    · simp only [Bool.not_eq_true] at pi
+    · simp [pi, h] at h1
+    · simp at pi
       exact pi
 
 theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultFormula n)
@@ -428,7 +429,7 @@ theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultForm
   · next h =>
     exact sat_of_insertRat f hf (c.delete negPivot) p pf h
   · split at performRatCheck_success
-    · exact False.elim performRatCheck_success
+    · simp at performRatCheck_success
     · next h =>
       simp only [not_or, Bool.not_eq_true, Bool.not_eq_false] at h
       have pfc : p ⊨ f.insert (c.delete negPivot) :=
@@ -516,7 +517,7 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D
         · simp only [getElem!, i_eq_idx, idx.2, Fin.getElem_fin, dite_true, decidableGetElem?]
           simp only [Fin.getElem_fin, ih.1] at h
           exact h
-      · simp only at h
+      · simp at h
   have h := (Array.foldl_induction motive h_base h_inductive).2 performRatCheck_fold_success i
   simpa [getElem!, i.2, dite_true, decidableGetElem?] using h
 

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -20,6 +20,9 @@ namespace DefaultFormula
 open Std.Sat
 open DefaultClause DefaultFormula Assignment
 
+-- TODO: remove aux lemma after update-stage0
+private theorem false_ne_true : (false = true) = False := by simp
+
 theorem size_insertUnit {n : Nat} (units : Array (Literal (PosFin n)))
     (assignments : Array Assignment) (b : Bool) (l : Literal (PosFin n)) :
     (insertUnit (units, assignments, b) l).2.1.size = assignments.size := by
@@ -111,7 +114,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           ⟨units.size, units_size_lt_updatedUnits_size⟩
         have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
         refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
-        simp only [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l]
+        simp [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l]
         constructor
         · rfl
         · constructor
@@ -127,7 +130,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                 apply Nat.lt_of_le_of_ne
                 · apply Nat.le_of_lt_succ
                   have k_property := k.2
-                  simp only [insertUnit, h3, ite_false, Array.size_push] at k_property
+                  simp [insertUnit, h3, ite_false, Array.size_push] at k_property
                   exact k_property
                 · intro h
                   simp only [← h, not_true, mostRecentUnitIdx] at hk
@@ -137,7 +140,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
               exact h2 ⟨k.1, k_in_bounds⟩
       · next i_ne_l =>
         apply Or.inl
-        simp only [insertUnit, h3, ite_false]
+        simp [insertUnit, h3, ite_false]
         rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)]
         constructor
         · exact h1
@@ -178,7 +181,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         let mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).1.size :=
           ⟨units.size, units_size_lt_updatedUnits_size⟩
         have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
-          simp only [insertUnit, h5, ite_false, Array.size_push]
+          simp [insertUnit, h5, ite_false, Array.size_push]
           exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size)
         match hb : b, hl : l.2 with
         | true, true =>
@@ -189,11 +192,11 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           exact h5 (has_add _ true)
         | true, false =>
           refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩
-          simp only [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
+          simp [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
           constructor
           · rw [Array.get_push_lt units l j.1 j.2, h1]
           · constructor
-            · simp only [i_eq_l, ← hl]
+            · simp [i_eq_l, ← hl]
               rfl
             · constructor
               · simp only [i_eq_l]
@@ -219,16 +222,16 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                     exact h4 ⟨k.1, h⟩ k_ne_j
                   · exfalso
                     have k_property := k.2
-                    simp only [insertUnit, h5, ite_false, Array.size_push] at k_property
+                    simp [insertUnit, h5, ite_false, Array.size_push] at k_property
                     rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                     · exact h k_lt_units_size
                     · simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
                       exact k_ne_l rfl
         | false, true =>
           refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
-          simp only [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
+          simp [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
           constructor
-          · simp only [i_eq_l, ← hl]
+          · simp [i_eq_l, ← hl]
             rfl
           · constructor
             · rw [Array.get_push_lt units l j.1 j.2, h1]
@@ -241,8 +244,8 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                 · match h : assignments0[i.val]'_ with
                   | unassigned => rfl
                   | pos =>
-                    simp only [addAssignment, h, ite_false, addNegAssignment] at h2
-                    simp only [i_eq_l] at h2
+                    simp [addAssignment, h, ite_false, addNegAssignment] at h2
+                    simp [i_eq_l] at h2
                     simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasPosAssignment, decidableGetElem?] at h5
                   | neg  => simp (config := {decide := true}) only [h] at h3
                   | both => simp (config := {decide := true}) only [h] at h3
@@ -256,7 +259,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                     exact h4 ⟨k.1, h⟩ k_ne_j
                   · exfalso
                     have k_property := k.2
-                    simp only [insertUnit, h5, ite_false, Array.size_push] at k_property
+                    simp [insertUnit, h5, ite_false, Array.size_push] at k_property
                     rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                     · exact h k_lt_units_size
                     · simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
@@ -270,10 +273,10 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
       · next i_ne_l =>
         apply Or.inr ∘ Or.inl
         have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
-          simp only [insertUnit, h5, ite_false, Array.size_push]
+          simp [insertUnit, h5, ite_false, Array.size_push]
           exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size)
         refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
-        simp only [insertUnit, h5, ite_false]
+        simp [insertUnit, h5, ite_false]
         constructor
         · rw [Array.get_push_lt units l j.1 j.2, h1]
         · constructor
@@ -350,7 +353,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                 simp only
                 have k_eq_units_size : k.1 = units.size := by
                   have k_property := k.2
-                  simp only [insertUnit, h, ite_false, Array.size_push] at k_property
+                  simp [insertUnit, h, ite_false, Array.size_push] at k_property
                   rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                   · exfalso; exact k_not_lt_units_size k_lt_units_size
                   · exact k_eq_units_size
@@ -431,7 +434,7 @@ theorem nodup_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd
         by_cases j = k2
         · next j_eq_k2 =>
           rw [← j_eq_k2, hj, ← bi_eq_bj, bi_eq_true] at h2
-          simp only [Prod.mk.injEq, and_false] at h2
+          simp at h2
         · next j_ne_k2 =>
           specialize h5 j j_ne_k1 j_ne_k2
           rw [hj, li_eq_lj] at h5
@@ -440,7 +443,7 @@ theorem nodup_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd
         by_cases i = k2
         · next i_eq_k2 =>
           rw [← i_eq_k2, hi, bi_eq_true] at h2
-          simp only [Prod.mk.injEq, and_false] at h2
+          simp at h2
         · next i_ne_k2 =>
           specialize h5 i i_ne_k1 i_ne_k2
           rw [hi] at h5
@@ -453,7 +456,7 @@ theorem nodup_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd
         by_cases j = k1
         · next j_eq_k1 =>
           rw [← j_eq_k1, hj, ← bi_eq_bj, bi_eq_false] at h1
-          simp only [Prod.mk.injEq, and_false] at h1
+          simp at h1
         · next j_ne_k1 =>
           specialize h5 j j_ne_k1 j_ne_k2
           rw [hj, li_eq_lj] at h5
@@ -462,7 +465,7 @@ theorem nodup_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd
         by_cases i = k1
         · next i_eq_k1 =>
           rw [← i_eq_k1, hi, bi_eq_false] at h1
-          simp only [Prod.mk.injEq, and_false] at h1
+          simp at h1
         · next i_ne_k1 =>
           specialize h5 i i_ne_k1 i_ne_k2
           rw [hi] at h5
@@ -580,7 +583,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
       have idx_ne_j2 : idx ≠ j2 := by
         rw [idx_eq_j1]
         intro j1_eq_j2
-        simp only [j1_eq_j2, ih2, Prod.mk.injEq, and_false] at ih1
+        simp [j1_eq_j2, ih2] at ih1
       refine Or.inr <| Or.inl <| ⟨j2, false, i_gt_zero, ?_⟩
       constructor
       · apply Nat.le_of_lt_succ
@@ -597,7 +600,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
             rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
             decide
           · constructor
-            · simp only [hasAssignment, hasNegAssignment, ih4, ite_false, not_false_eq_true]
+            · simp [hasAssignment, hasNegAssignment, ih4]
             · intro k k_ge_idx_add_one k_ne_j2
               intro h1
               by_cases units[k.1].2
@@ -873,7 +876,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
                 simp only [l'_eq_false, hasAssignment, ite_false] at h2
                 simp only [hasAssignment, l_eq_true, getElem!, l_eq_i, i_in_bounds,
                   Array.get_eq_getElem, ↓reduceIte, ↓reduceDIte, h1, addAssignment, l'_eq_false,
-                  hasPos_addNeg, decidableGetElem?] at h
+                  hasPos_addNeg, decidableGetElem?, false_ne_true] at h
                 exact unassigned_of_has_neither _ h h2
               · intro k k_ne_zero k_ne_j_succ
                 have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
@@ -921,7 +924,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
               · simp only [l'] at l'_eq_true
                 simp only [hasAssignment, l'_eq_true, ite_true] at h2
                 simp only [hasAssignment, l_eq_false, ↓reduceIte, getElem!, l_eq_i, i_in_bounds,
-                  Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?] at h
+                  Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, false_ne_true] at h
                 exact unassigned_of_has_neither _ h2 h
               · intro k k_ne_j_succ k_ne_zero
                 have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
@@ -1330,9 +1333,9 @@ theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (ru
   · simp only [clear_insertRup f f_readyForRupAdd (negate c), Prod.mk.injEq, and_true] at rupAddSuccess
     exact rupAddSuccess.symm
   · split at rupAddSuccess
-    · simp only [Prod.mk.injEq, and_false] at rupAddSuccess
+    · simp at rupAddSuccess
     · split at rupAddSuccess
-      · simp only [Prod.mk.injEq, and_false] at rupAddSuccess
+      · simp at rupAddSuccess
       · let fc := (insertRupUnits f (negate c)).1
         have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
           rw [size_assignments_insertRupUnits f (negate c)]

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -17,6 +17,9 @@ namespace Internal
 
 namespace DefaultFormula
 
+-- TODO: remove aux lemma after update-stage0
+private theorem false_ne_true : (false = true) = False := by simp
+
 open Std.Sat
 open DefaultClause DefaultFormula Assignment ReduceResult
 
@@ -43,13 +46,13 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
       apply Exists.intro i
       by_cases l.1.1 = i.1
       · next l_eq_i =>
-        simp only [l_eq_i, Array.getElem_modify_self i_in_bounds, h]
+        simp [l_eq_i, Array.getElem_modify_self i_in_bounds, h]
         exact add_both_eq_both l.2
       · next l_ne_i =>
-        rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+        simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
         exact h
     · apply Exists.intro l.1
-      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds]
+      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, false_ne_true]
       simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
       by_cases l.2
       · next l_eq_true =>
@@ -60,8 +63,7 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
       · next l_eq_false =>
         simp only [Bool.not_eq_true] at l_eq_false
         rw [l_eq_false]
-        simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
-          Bool.not_eq_true, decidableGetElem?] at hl
+        simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, decidableGetElem?] at hl
         split at hl <;> simp_all (config := { decide := true })
 
 theorem contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array Assignment) (assignments_size : assignments.size = n)
@@ -126,7 +128,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
   intro insertUnit_fold_success
   have false_imp : false → ∃ i : PosFin n, f.assignments[i.1]'(by rw [f_readyForRupAdd.2.1]; exact i.2.2) = both := by
     intro h
-    simp only at h
+    simp at h
   rcases contradiction_of_insertUnit_fold_success f.assignments f_readyForRupAdd.2.1 f.rupUnits false (negate c) false_imp
     insertUnit_fold_success with ⟨i, hboth⟩
   have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
@@ -148,7 +150,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
     have p_entails_i_true := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i true hpos p pf
     have p_entails_i_false := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i false hneg p pf
     simp only [Entails.eval] at p_entails_i_true p_entails_i_false
-    simp only [p_entails_i_true] at p_entails_i_false
+    simp [p_entails_i_true] at p_entails_i_false
   · simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe]
     apply Exists.intro i
     have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
@@ -166,7 +168,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
       apply And.intro i_false_in_c
       simp only [addAssignment, ← b_eq_true, addPosAssignment, ite_true] at h2
       split at h2
-      · simp only at h2
+      · simp at h2
       · next heq =>
         have hasNegAssignment_fi : hasAssignment false (f.assignments[i.1]'i_in_bounds) := by
           simp only [hasAssignment, hasPosAssignment, heq, ite_false]
@@ -178,11 +180,11 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
         exfalso
         rw [heq] at h3
         exact h3 (has_both b)
-      · simp only at h2
+      · simp at h2
     · apply Or.inr
       rw [i'_eq_i] at i_true_in_c
       apply And.intro i_true_in_c
-      simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false] at h2
+      simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, false_ne_true] at h2
       split at h2
       · next heq =>
         have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by
@@ -190,12 +192,12 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
         have p_entails_i := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i true hasPosAssignment_fi p pf
         simp only [(· ⊨ ·)] at p_entails_i
         exact p_entails_i
-      · simp only at h2
+      · simp at h2
       · next heq =>
         exfalso
         rw [heq] at h3
         exact h3 (has_both b)
-      · simp only at h2
+      · simp at h2
   · exfalso
     have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
       have i_rw : i = ⟨i.1, i.2⟩ := rfl
@@ -350,10 +352,9 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
     rcases hp2 with ⟨i2, hp2⟩
     simp only [Fin.getElem_fin] at h1
     simp only [Fin.getElem_fin] at h2
-    simp only [h1, Clause.toList, unit_eq, List.mem_singleton, Prod.mk.injEq,
-      and_false, false_and, and_true, false_or, h2, or_false] at hp1 hp2
+    simp [h1, Clause.toList, unit_eq, List.mem_singleton, h2] at hp1 hp2
     simp only [hp2.1, ← hp1.1, decide_eq_true_eq, true_and] at hp2
-    simp only [hp1.2] at hp2
+    simp [hp1.2] at hp2
 
 def ConfirmRupHintFoldEntailsMotive {n : Nat} (f : DefaultFormula n) (_idx : Nat)
     (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) :
@@ -364,7 +365,7 @@ theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n)
     (assignment : Array Assignment) :
     reduce c assignment = encounteredBoth → Unsatisfiable (PosFin n) assignment := by
   have hb : (reducedToEmpty : ReduceResult (PosFin n)) = encounteredBoth → Unsatisfiable (PosFin n) assignment := by
-    simp only [false_implies]
+    simp
   have hl (res : ReduceResult (PosFin n)) (ih : res = encounteredBoth → Unsatisfiable (PosFin n) assignment)
     (l : Literal (PosFin n)) (_ : l ∈ c.clause) :
     (reduce_fold_fn assignment res l) = encounteredBoth → Unsatisfiable (PosFin n) assignment := by
@@ -379,7 +380,7 @@ theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n)
         intro p hp
         simp only [(· ⊨ ·), Bool.not_eq_true] at hp
         specialize hp l.1
-        simp only [heq, has_both] at hp
+        simp [heq, has_both] at hp
       · simp at h
     · split at h
       · split at h <;> simp at h
@@ -388,7 +389,7 @@ theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n)
         intro p hp
         simp only [(· ⊨ ·), Bool.not_eq_true] at hp
         specialize hp l.1
-        simp only [heq, has_both] at hp
+        simp [heq, has_both] at hp
       · simp at h
     · simp at h
   exact List.foldlRecOn c.clause (reduce_fold_fn assignment) reducedToEmpty hb hl
@@ -410,11 +411,11 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
   · intro h p
     rw [reduce_fold_fn.eq_def] at h
     split at h
-    · simp only at h
+    · simp at h
     · split at h
       · next heq =>
         split at h
-        · exact False.elim h
+        · simp at h
         · next c_arr_idx_eq_false =>
           simp only [Bool.not_eq_true] at c_arr_idx_eq_false
           rcases ih.1 rfl p with ih1 | ih1
@@ -433,7 +434,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
           · exact Or.inr ih1
       · next heq =>
         split at h
-        · exact False.elim h
+        · simp at h
         · next c_arr_idx_eq_false =>
           simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_false
           rcases ih.1 rfl p with ih1 | ih1
@@ -450,19 +451,19 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
             · next h =>
               exact Or.inr h
           · exact Or.inr ih1
-      · simp only at h
-      · simp only at h
+      · simp at h
+      · simp at h
     · next l =>
       split at h
       · split at h <;> contradiction
       · split at h <;> contradiction
-      · simp only at h
-      · simp only at h
-    · simp only at h
+      · simp at h
+      · simp at h
+    · simp at h
   · intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j
     rw [reduce_fold_fn.eq_def] at h
     split at h
-    · simp only at h
+    · simp at h
     · split at h
       · next heq =>
         split at h
@@ -479,7 +480,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
           · next p_c_arr_idx_eq_false =>
             simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false
             simp (config := { decide := true }) only [h, p_c_arr_idx_eq_false] at hp
-        · exact False.elim h
+        · simp at h
       · next heq =>
         split at h
         · next c_arr_idx_eq_true =>
@@ -495,8 +496,8 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
           · next p_c_arr_idx_eq_false =>
             simp only [h] at p_c_arr_idx_eq_false
             simp only [(· ⊨ ·), c_arr_idx_eq_true, p_c_arr_idx_eq_false]
-        · exact False.elim h
-      · simp only at h
+        · simp at h
+      · simp at h
       · simp only [reducedToUnit.injEq] at h
         rw [← h]
         rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
@@ -510,7 +511,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
       split at h
       · next heq =>
         split at h
-        · exact False.elim h
+        · simp at h
         · next c_arr_idx_eq_false =>
           simp only [Bool.not_eq_true] at c_arr_idx_eq_false
           simp only [reducedToUnit.injEq] at h
@@ -525,7 +526,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
             simp (config := { decide := true }) only [p_entails_c_arr_j, decide_True, heq] at hp
       · next heq =>
         split at h
-        · exact False.elim h
+        · simp at h
         · next c_arr_idx_eq_true =>
           simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_true
           simp only [reducedToUnit.injEq] at h
@@ -538,9 +539,9 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
             simp only [(· ⊨ ·), Bool.not_eq_true] at hp
             specialize hp c_arr[idx.1].1
             simp (config := { decide := true }) only [p_entails_c_arr_j, decide_True, heq] at hp
-      · simp only at h
-      · simp only at h
-    · simp only at h
+      · simp at h
+      · simp at h
+    · simp at h
 
 theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array Assignment) :
     (reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧
@@ -550,8 +551,9 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
   rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_data]
   let motive := ReducePostconditionInductionMotive c_arr assignment
   have h_base : motive 0 reducedToEmpty := by
+    have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp
     simp only [ReducePostconditionInductionMotive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall,
-      forall_const, false_implies, implies_true, and_true, motive]
+      forall_const, false_implies, implies_true, and_true, motive, this]
     intro p
     apply Or.inl
     intro i i_lt_zero
@@ -647,7 +649,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
         · simp only [Option.some.injEq] at hc
           rw [← hc]
           apply Array.getElem_mem_data
-        · exact False.elim hc
+        · simp at hc
       split
       · next heq =>
         simp only [ConfirmRupHintFoldEntailsMotive, h1, imp_self, and_self, hsize,
@@ -666,8 +668,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
       · next l b heq =>
         simp only [ConfirmRupHintFoldEntailsMotive]
         split
-        · simp only [h1, hsize, false_implies, and_self]
-        · simp only [Array.size_modify, hsize, false_implies, and_true, true_and]
+        · simp [h1, hsize]
+        · simp [Array.size_modify, hsize]
           intro p pf
           have pacc := h1 p pf
           have pc : p ⊨ c := by
@@ -690,18 +692,18 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
               by_cases hb : b
               · simp only [hasAssignment, ↓reduceIte, addAssignment]
                 simp only [hb]
-                simp only [hasAssignment, addAssignment, hb, ite_true, ite_false, hasNeg_addPos]
+                simp [hasAssignment, addAssignment, hb, ite_true, ite_false, hasNeg_addPos]
                 exact pacc
               · exfalso -- hb, pi, l_eq_i, and plb are incompatible
                 simp only [Bool.not_eq_true] at hb
-                simp only [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
+                simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
             · simp only [Bool.not_eq_true] at pi
               simp only [pi, decide_True]
               simp only [pi, decide_True] at pacc
               by_cases hb : b
-              · simp only [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
+              · simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
               · simp only [Bool.not_eq_true] at hb
-                simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg]
+                simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, false_ne_true]
                 simp only [hasAssignment, ite_true] at pacc
                 exact pacc
           · next l_ne_i =>
@@ -711,11 +713,11 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
             simp only [getElem!, i_in_bounds, dite_true, decidableGetElem?] at pacc
             exact pacc
       · apply And.intro hsize ∘ And.intro h1
-        simp only [false_implies]
+        simp
     · apply And.intro hsize ∘ And.intro h1
-      simp only [false_implies]
+      simp
     · apply And.intro hsize ∘ And.intro h1
-      simp only [false_implies]
+      simp
 
 theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
     (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n) (rupHints : Array Nat)
@@ -726,8 +728,7 @@ theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
   intro fc confirmRupHint_fold_res confirmRupHint_success
   let motive := ConfirmRupHintFoldEntailsMotive fc.1
   have h_base : motive 0 (fc.fst.assignments, [], false, false) := by
-    simp only [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRupUnits, f_readyForRupAdd.2.1,
-      false_implies, and_true, true_and, motive, fc]
+    simp [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRupUnits, f_readyForRupAdd.2.1, motive, fc]
     have fc_satisfies_AssignmentsInvariant :=
       assignmentsInvariant_insertRupUnits_of_assignmentsInvariant f f_readyForRupAdd (negate c)
     exact limplies_of_assignmentsInvariant fc.1 fc_satisfies_AssignmentsInvariant
@@ -751,7 +752,7 @@ theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
     rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
     · simp only [negate_eq, List.mem_map, Prod.exists, Bool.exists_bool] at v_in_neg_c
       rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
-      · simp only [Literal.negate, Bool.not_false, Prod.mk.injEq, and_false] at v'_eq_v
+      · simp [Literal.negate] at v'_eq_v
       · simp only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_true] at v'_eq_v
         simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists,
           Bool.exists_bool, ← unsat_c_eq, not_exists, not_or, not_and] at p_unsat_c
@@ -779,7 +780,7 @@ theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
         simp only [(· ⊨ ·), Bool.not_eq_true] at pv
         simp only [p_unsat_c] at pv
         cases pv
-      · simp only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_false] at v'_eq_v
+      · simp [Literal.negate, Bool.not_true] at v'_eq_v
     · simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf
       exact p_unsat_c <| pf unsat_c unsat_c_in_f
 
@@ -815,9 +816,9 @@ theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rup
     · exact f_limplies_fc
     · exact limplies_insert f c p
   · split at rupAddSuccess
-    · simp only [Prod.mk.injEq, and_false] at rupAddSuccess
+    · simp at rupAddSuccess
     · split at rupAddSuccess
-      · simp only [Prod.mk.injEq, and_false] at rupAddSuccess
+      · simp at rupAddSuccess
       · next performRupCheck_success =>
         rw [Bool.not_eq_false] at performRupCheck_success
         have f_limplies_fc := safe_insert_of_performRupCheck_insertRup f f_readyForRupAdd c rupHints performRupCheck_success

src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean

@@ -33,7 +33,7 @@ theorem addEmptyCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formu
     rw [Formula.insert_iff]
     exact Or.inl rfl
   specialize pf empty empty_in_f'
-  simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool,
+  simp [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool,
     empty_eq, List.any_nil] at pf
 
 theorem addRupCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
@@ -104,7 +104,7 @@ theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formul
     lratChecker f prf = success → Unsatisfiable α f := by
   induction prf generalizing f
   · unfold lratChecker
-    simp only [false_implies]
+    simp [false_implies]
   · next action restPrf ih =>
     simp only [List.find?, List.mem_cons, forall_eq_or_imp] at prfWellFormed
     rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩
@@ -112,11 +112,10 @@ theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formul
     split
     · intro h
       exfalso
-      simp only at h
+      simp at h
     · next id rupHints restPrf' _ =>
-      simp only [ite_eq_left_iff, Bool.not_eq_true]
+      simp [ite_eq_left_iff, Bool.not_eq_true]
       intro rupAddSuccess
-      rw [← Bool.not_eq_true, imp_false, Classical.not_not] at rupAddSuccess
       exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
     · next id c rupHints restPrf' hprf =>
       split
@@ -128,7 +127,7 @@ theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formul
         rw [← hprf.2] at f'_success
         rw [hCheckSuccess] at heq
         exact addRupCaseSound f f_readyForRupAdd f_readyForRatAdd c f' rupHints heq restPrf restPrfWellFormed ih f'_success
-      · simp only [false_implies]
+      · simp [false_implies]
     · next id c pivot rupHints ratHints restPrf' hprf =>
       split
       next f' checkSuccess heq =>
@@ -141,7 +140,7 @@ theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formul
         simp only [WellFormedAction, hprf.1] at actionWellFormed
         exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
           restPrfWellFormed ih f'_success
-      · simp only [false_implies]
+      · simp [false_implies]
     · next ids restPrf' hprf =>
       intro h
       simp only [List.cons.injEq] at hprf

src/lake/Lake/Util/Compare.lean

@@ -48,11 +48,11 @@ theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α}
   unfold compareOfLessAndEq at h
   split at h
   next =>
-    exact False.elim h
+    simp at h
   next =>
     split at h
     next => assumption
-    next => exact False.elim h
+    next => simp at h
 
 theorem compareOfLessAndEq_rfl [LT α] [DecidableEq α] {a : α}
 [Decidable (a < a)] (lt_irrefl : ¬ a < a) : compareOfLessAndEq a a = .eq := by

tests/lean/mutwf1.lean

@@ -6,8 +6,8 @@ mutual
     | n, false => n + g n
   termination_by n b => (n, if b then 2 else 1)
   decreasing_by
-  · apply Prod.Lex.right; decide
-  · apply Prod.Lex.right; decide
+  · apply Prod.Lex.right; simp -- decide TODO: add `reduceCtorEq` at `clean_wf` after update-stage0
+  · apply Prod.Lex.right; simp -- decide
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then

tests/lean/run/5046.lean

@@ -0,0 +1,25 @@
+example : (1:Nat) = 0 := by
+  fail_if_success simp only
+  simp only [reduceCtorEq]
+  guard_target =ₛ False
+  sorry
+
+example : (1:Int) = 0 := by
+  fail_if_success simp only
+  sorry
+
+example : (-1:Int) = 0 := by
+  fail_if_success simp only
+  simp only [reduceCtorEq]
+  guard_target =ₛ False
+  sorry
+
+example : 2^10000 = 2^9999 := by
+  fail_if_success simp only
+  fail_if_success simp only [reduceCtorEq]
+  sorry
+
+example : 2^10000 = 2^9999 := by
+  fail_if_success simp (config := Lean.Meta.Simp.neutralConfig) only
+  fail_if_success simp (config := Lean.Meta.Simp.neutralConfig) only [reduceCtorEq]
+  sorry

tests/lean/run/eq_some_iff_get_eq_issue.lean

@@ -1,7 +1,6 @@
-
 namespace Option
 
 theorem eq_some_iff_get_eq' {o : Option α} {a : α} :
   o = some a ↔ ∃ h : o.isSome, Option.get _ h = a := by
-  cases o; simp only [isSome_none, false_iff]; intro h; cases h; contradiction
+  cases o; simp only [isSome_none, false_iff, reduceCtorEq]; intro h; cases h; contradiction
   simp [exists_prop]

tests/lean/run/reductionBug.lean

@@ -16,4 +16,4 @@ def Expr.constFold : Expr Γ τ → Option Unit
 theorem Expr.constFold_sound {e : Expr Γ τ} : constFold e = some v → True := by
   intro h
   induction e with
-  | var   => simp only [constFold] at h
+  | var   => simp only [reduceCtorEq, constFold] at h

tests/lean/simp_trace.lean.expected.out

@@ -1,4 +1,4 @@
-Try this: simp only [f]
+Try this: simp only [f, reduceCtorEq]
 [Meta.Tactic.simp.rewrite] unfold f, f (a :: b = []) ==> a :: b = []
 [Meta.Tactic.simp.rewrite] eq_self:1000, False = False ==> True
 Try this: simp only [length, gt_iff_lt]