chore: bump Std to leanprover-community/batteries#242 (#10104)

Co-authored-by: Scott Morrison <[email protected]>

Mathlib.lean

@@ -3490,7 +3490,6 @@ import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
-import Mathlib.Tactic.TryThis
 import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.UnsetOption
@@ -3842,7 +3841,6 @@ import Mathlib.Util.MemoFix
 import Mathlib.Util.Qq
 import Mathlib.Util.SleepHeartbeats
 import Mathlib.Util.Superscript
-import Mathlib.Util.Syntax
 import Mathlib.Util.SynthesizeUsing
 import Mathlib.Util.Tactic
 import Mathlib.Util.TermBeta

Mathlib/Data/Sign.lean

@@ -111,7 +111,7 @@ private lemma le_antisymm (a b : SignType) (_ : a ≤ b) (_: b ≤ a) : a = b :=
   cases a <;> cases b <;> trivial
 
 private lemma le_trans (a b c : SignType) (_ : a ≤ b) (_: b ≤ c) : a ≤ c := by
-  cases a <;> cases b <;> cases c <;> first | tauto | constructor
+  cases a <;> cases b <;> cases c <;> tauto
 
 instance : LinearOrder SignType where
   le := (· ≤ ·)

Mathlib/Mathport/Notation.lean

@@ -6,9 +6,9 @@ Authors: Mario Carneiro, Kyle Miller
 import Mathlib.Lean.Elab.Term
 import Mathlib.Lean.PrettyPrinter.Delaborator
 import Mathlib.Tactic.ScopedNS
-import Mathlib.Util.Syntax
 import Std.Linter.UnreachableTactic
 import Std.Util.ExtendedBinder
+import Std.Lean.Syntax
 
 /-!
 # The notation3 macro, simulating Lean 3's notation.

Mathlib/Mathport/Syntax.lean

@@ -93,7 +93,6 @@ import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.Use
 import Mathlib.Tactic.WLOG
 import Mathlib.Tactic.Zify
-import Mathlib.Util.Syntax
 import Mathlib.Util.WithWeakNamespace
 import Mathlib.Mathport.Notation
 

Mathlib/Tactic.lean

@@ -168,7 +168,6 @@ import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
-import Mathlib.Tactic.TryThis
 import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.UnsetOption

Mathlib/Tactic/Common.lean

@@ -100,7 +100,6 @@ import Mathlib.Tactic.TermCongr
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
-import Mathlib.Tactic.TryThis
 import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.UnsetOption
 import Mathlib.Tactic.Use

Mathlib/Tactic/Observe.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Tactic.LibrarySearch
-import Mathlib.Tactic.TryThis
+import Std.Tactic.TryThis
 
 /-!
 # The `observe` tactic.
@@ -14,7 +14,7 @@ import Mathlib.Tactic.TryThis
 
 namespace Mathlib.Tactic.LibrarySearch
 
-open Lean Meta Elab Tactic
+open Lean Meta Elab Tactic Std.Tactic.TryThis
 
 /-- `observe hp : p` asserts the proposition `p`, and tries to prove it using `exact?`.
 If no proof is found, the tactic fails.

Mathlib/Tactic/Propose.lean

@@ -9,7 +9,6 @@ import Mathlib.Lean.Meta.Basic
 import Std.Util.Cache
 import Mathlib.Tactic.Core
 import Std.Tactic.SolveByElim
-import Mathlib.Tactic.TryThis
 
 /-!
 # Propose

Mathlib/Tactic/RewriteSearch.lean

@@ -292,6 +292,8 @@ to prevent `rw_search` from using the names theorems.
 -/
 syntax "rw_search" (forbidden)? : tactic
 
+open Std.Tactic.TryThis
+
 elab_rules : tactic |
     `(tactic| rw_search%$tk $[[ $[-$forbidden],* ]]?) => withMainContext do
   let forbidden : NameSet :=

Mathlib/Tactic/Rewrites.lean

@@ -13,7 +13,6 @@ import Mathlib.Control.Basic
 import Mathlib.Data.MLList.Dedup
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Lean.Meta.DiscrTree
-import Mathlib.Tactic.TryThis
 
 /-!
 # The `rewrites` tactic.

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
+   "rev": "128fd8e663353da2a3666167605b510824fe2eb5",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

test/LibrarySearch/basic.lean

@@ -26,19 +26,19 @@ set_option pp.unicode.fun true
 
 noncomputable section
 
-/-- info: Try this: exact Nat.lt.base x -/
+/-- info: Try this: exact Nat.le.refl -/
 #guard_msgs in
 example (x : Nat) : x ≠ x.succ := ne_of_lt (by apply?)
 
-/-- info: Try this: exact Nat.succ_pos 1 -/
+/-- info: Try this: exact Nat.le.step Nat.le.refl -/
 #guard_msgs in
 example : 0 ≠ 1 + 1 := ne_of_lt (by apply?)
 
 /-- info: Try this: exact Nat.add_comm x y -/
 #guard_msgs in
 example (x y : Nat) : x + y = y + x := by apply?
 
-/-- info: Try this: exact fun a ↦ Nat.add_le_add_right a k -/
+/-- info: Try this: exact fun a ↦ Nat.add_le_add a Nat.le.refl -/
 #guard_msgs in
 example (n m k : Nat) : n ≤ m → n + k ≤ m + k := by apply?
 
@@ -50,7 +50,7 @@ example (ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply?
 #guard_msgs (drop info) in
 example : Int := by apply?
 
-/-- info: Try this: Nat.lt.base x -/
+/-- info: Try this: Nat.le.refl -/
 #guard_msgs in
 example : x < x + 1 := exact?%
 
@@ -88,7 +88,7 @@ by apply?
 example (n m k : ℕ) : n * m - n * k = n * (m - k) :=
 by apply?
 
-/-- info: Try this: exact eq_comm -/
+/-- info: Try this: exact { mp := fun a ↦ id a.symm, mpr := fun a ↦ id a.symm } -/
 #guard_msgs in
 example {α : Type} (x y : α) : x = y ↔ y = x := by apply?
 
@@ -174,7 +174,7 @@ axiom F (a b : ℕ) : f a ≤ f b ↔ a ≤ b
 #guard_msgs in
 example (a b : ℕ) (h : a ≤ b) : f a ≤ f b := by apply?
 
-/-- info: Try this: exact List.join L -/
+/-- info: Try this: exact List.findIdxs (fun a ↦ false) L -/
 #guard_msgs in
 example (L _M : List (List ℕ)) : List ℕ := by apply? using L
 
@@ -225,7 +225,7 @@ lemma ex' (x : ℕ) (_h₁ : x = 0) (h : 2 * 2 ∣ x) : 2 ∣ x := by
 
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/apply.3F.20failure/near/402534407
 example (P Q : Prop) (h : P → Q) (h' : ¬Q) : ¬P := by
-  exact? says exact mt h h'
+  exact? says exact fun a ↦ h' (h a)
 
 -- Removed until we come up with a way of handling nonspecific lemmas
 -- that does not pollute the output or cause too much slow-down.

test/RewriteSearch/Polynomial.lean

@@ -147,14 +147,15 @@ example {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) :
 --   -- rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]
 --   done
 
--- Polynomial.degree_X_sub_C.{u}
-#guard_msgs(drop info) in
-example {R : Type u} [Ring R] [Nontrivial R] (a : R) :
-    Polynomial.degree (Polynomial.X - Polynomial.C a) = 1 := by
-  rw_search [-Polynomial.degree_X_sub_C]
-  -- Mathlib proof:
-  -- rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]
-  done
+-- Fails:
+-- -- Polynomial.degree_X_sub_C.{u}
+-- #guard_msgs(drop info) in
+-- example {R : Type u} [Ring R] [Nontrivial R] (a : R) :
+--     Polynomial.degree (Polynomial.X - Polynomial.C a) = 1 := by
+--   rw_search [-Polynomial.degree_X_sub_C]
+--   -- Mathlib proof:
+--   -- rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]
+--   done
 
 -- Polynomial.natDegree_X_sub_C.{u}
 #guard_msgs(drop info) in

test/propose.lean

@@ -72,6 +72,8 @@ info: Try this: have : ¬IsUnit p := not_unit hp
 ---
 info: Try this: have : ¬p ∣ 1 := not_dvd_one hp
 ---
+info: Try this: have : p ∣ p ∨ p ∣ p := dvd_or_dvd hp (Exists.intro p (Eq.refl (p * p)))
+---
 info: Try this: have : p ≠ 0 := ne_zero hp
 ---
 info: Try this: have : p ∣ p * p ↔ p ∣ p ∨ p ∣ p := dvd_mul hp

test/solve_by_elim/basic.lean

@@ -45,7 +45,7 @@ example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by s
 example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by
   solve_by_elim only [f, a]
 
-example (h₁ h₂ : False) : True := by
+example (h₁ h₂ : False) : Empty := by
   -- 'It doesn't make sense to remove local hypotheses when using `only` without `*`.'
   fail_if_success solve_by_elim only [-h₁]
   -- 'It does make sense to use `*` without `only`.'
@@ -58,17 +58,24 @@ example (P₁ P₂ : α → Prop) (f : ∀ (a : α), P₁ a → P₂ a → β)
   solve_by_elim
 
 example {X : Type} (x : X) : x = x := by
-  fail_if_success solve_by_elim only -- needs the `rfl` lemma
+  fail_if_success solve_by_elim (config := {constructor := false}) only -- needs the `rfl` lemma
   solve_by_elim
 
 -- Needs to apply `rfl` twice, with different implicit arguments each time.
 -- A naive implementation of solve_by_elim would get stuck.
 example {X : Type} (x y : X) (p : Prop) (h : x = x → y = y → p) : p := by solve_by_elim
 
 example : True := by
-  fail_if_success solve_by_elim only -- needs the `trivial` lemma
+  fail_if_success solve_by_elim (config := {constructor := false}) only -- needs the `trivial` lemma
   solve_by_elim
 
+example : True := by
+  -- uses the `trivial` lemma, which should now be removed from the default set:
+  solve_by_elim (config := {constructor := false})
+
+example : True := by
+  solve_by_elim only -- uses the constructor discharger.
+
 -- Requires backtracking.
 example (P₁ P₂ : α → Prop) (f : ∀ (a: α), P₁ a → P₂ a → β)
     (a : α) (_ha₁ : P₁ a)
@@ -119,15 +126,13 @@ example (f g : ℕ → Prop) : (∃ k : ℕ, f k) ∨ (∃ k : ℕ, g k) ↔ ∃
   rintro ⟨n, hf | hg⟩
   solve_by_elim* (config := {maxDepth := 13}) [Or.inl, Or.inr, Exists.intro]
 
--- Test that `Config.intros` causes `solve_by_elim` to call `intro` on intermediate goals.
+-- Test that we can disable the `intro` discharger.
 example (P : Prop) : P → P := by
-  fail_if_success solve_by_elim
-  solve_by_elim (config := .intros)
+  fail_if_success solve_by_elim (config := {intro := false})
+  solve_by_elim
 
--- This worked in mathlib3 without the `@`, but now goes into a loop.
--- If someone wants to diagnose this, please do!
 example (P Q : Prop) : P ∧ Q → P ∧ Q := by
-  solve_by_elim [And.imp, @id]
+  solve_by_elim
 
 section apply_assumption