chore: bump Std (#8403)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Archive/Imo/Imo1969Q1.lean

@@ -6,7 +6,6 @@ Authors: Kevin Lacker
 import Mathlib.Algebra.GroupPower.Identities
 import Mathlib.Data.Int.NatPrime
 import Mathlib.Tactic.Linarith
-import Mathlib.Tactic.NormCast
 import Mathlib.Data.Set.Finite
 
 #align_import imo.imo1969_q1 from "leanprover-community/mathlib"@"2d6f88c296da8df484d7f5b9ee1d10910ab473a2"

Mathlib.lean

@@ -3228,8 +3228,6 @@ import Mathlib.Tactic.MoveAdd
 import Mathlib.Tactic.NoncommRing
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Tactic.Nontriviality.Core
-import Mathlib.Tactic.NormCast
-import Mathlib.Tactic.NormCast.Tactic
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NormNum.BigOperators

Mathlib/Algebra/CharZero/Defs.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Data.Int.Cast.Defs
-import Mathlib.Tactic.NormCast.Tactic
 import Mathlib.Tactic.Cases
 import Mathlib.Algebra.NeZero
 

Mathlib/Data/FunLike/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.NormCast
 import Mathlib.Util.CompileInductive
 
 #align_import data.fun_like.basic from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"

Mathlib/Data/Set/Lattice.lean

@@ -56,7 +56,7 @@ In lemma names,
 set_option autoImplicit true
 
 
-open Function Tactic Set
+open Function Set
 
 universe u
 

Mathlib/Init/Data/Ordering/Lemmas.lean

@@ -45,7 +45,8 @@ variable {α : Type u} {lt : α → α → Prop} [DecidableRel lt]
 attribute [local simp] cmpUsing
 
 @[simp]
-theorem cmpUsing_eq_lt (a b : α) : (cmpUsing lt a b = Ordering.lt) = lt a b := by simp
+theorem cmpUsing_eq_lt (a b : α) : (cmpUsing lt a b = Ordering.lt) = lt a b := by
+  simp only [cmpUsing, Ordering.ite_eq_lt_distrib, ite_self, if_false_right_eq_and, and_true]
 #align cmp_using_eq_lt cmpUsing_eq_lt
 
 @[simp]

Mathlib/Lean/Meta/Simp.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison, Gabriel Ebner, Floris van Doorn
 import Lean
 import Std.Tactic.OpenPrivate
 import Std.Lean.Meta.DiscrTree
+import Std.Lean.Meta.Simp
 
 /-!
 # Helper functions for using the simplifier.
@@ -37,15 +38,6 @@ toUnfold: {s.toUnfold.toList}
 erased: {s.erased.toList.map (·.key)}
 toUnfoldThms: {s.toUnfoldThms.toList}"
 
-def mkEqSymm (e : Expr) (r : Simp.Result) : MetaM Simp.Result :=
-  ({ expr := e, proof? := · }) <$>
-  match r.proof? with
-  | none => pure none
-  | some p => some <$> Meta.mkEqSymm p
-
-def mkCast (r : Simp.Result) (e : Expr) : MetaM Expr := do
-  mkAppM ``cast #[← r.getProof, e]
-
 /--
 Constructs a proof that the original expression is true
 given a simp result which simplifies the target to `True`.
@@ -67,43 +59,6 @@ def getPropHyps : MetaM (Array FVarId) := do
         result := result.push localDecl.fvarId
   return result
 
-export private mkDischargeWrapper from Lean.Elab.Tactic.Simp
-
--- copied from core
-/--
-If `ctx == false`, the config argument is assumed to have type `Meta.Simp.Config`,
-and `Meta.Simp.ConfigCtx` otherwise.
-If `ctx == false`, the `discharge` option must be none
--/
-def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bool)
-    (kind := SimpKind.simp) (ctx := false) (ignoreStarArg : Bool := false) :
-    TacticM MkSimpContextResult := do
-  if ctx && !stx[2].isNone then
-    if kind == SimpKind.simpAll then
-      throwError "'simp_all' tactic does not support 'discharger' option"
-    if kind == SimpKind.dsimp then
-      throwError "'dsimp' tactic does not support 'discharger' option"
-  let dischargeWrapper ← mkDischargeWrapper stx[2]
-  let simpOnly := !stx[3].isNone
-  let simpTheorems ← if simpOnly then
-    simpOnlyBuiltins.foldlM (·.addConst ·) {}
-  else
-    pure simpTheorems
-  let congrTheorems ← Meta.getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
-    config       := (← elabSimpConfig stx[1] (kind := kind))
-    simpTheorems := #[simpTheorems], congrTheorems
-  }
-  if !r.starArg || ignoreStarArg then
-    return { r with dischargeWrapper }
-  else
-    let mut simpTheorems := r.ctx.simpTheorems
-    let hs ← getPropHyps
-    for h in hs do
-      unless simpTheorems.isErased (.fvar h) do
-        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    return { ctx := { r.ctx with simpTheorems }, dischargeWrapper }
-
 export private checkTypeIsProp shouldPreprocess preprocess mkSimpTheoremCore
   from Lean.Meta.Tactic.Simp.SimpTheorems
 

Mathlib/Logic/Basic.lean

@@ -885,8 +885,6 @@ theorem exists_unique_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃! h
   @exists_unique_const (q h) p ⟨h⟩ _
 #align exists_unique_prop_of_true exists_unique_prop_of_true
 
-theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True :=
-  iff_true_intro fun h ↦ hn.elim h
 #align forall_prop_of_false forall_prop_of_false
 
 theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬p → ¬∃ h' : p, q h' :=
@@ -1145,18 +1143,9 @@ theorem dite_eq_iff' : dite P A B = c ↔ (∀ h, A h = c) ∧ ∀ h, B h = c :=
 theorem ite_eq_iff' : ite P a b = c ↔ (P → a = c) ∧ (¬P → b = c) := dite_eq_iff'
 #align ite_eq_iff' ite_eq_iff'
 
-@[simp] theorem dite_eq_left_iff : dite P (fun _ ↦ a) B = a ↔ ∀ h, B h = a := by
-  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
 #align dite_eq_left_iff dite_eq_left_iff
-
-@[simp] theorem dite_eq_right_iff : (dite P A fun _ ↦ b) = b ↔ ∀ h, A h = b := by
-  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
 #align dite_eq_right_iff dite_eq_right_iff
-
-@[simp] theorem ite_eq_left_iff : ite P a b = a ↔ ¬P → b = a := dite_eq_left_iff
 #align ite_eq_left_iff ite_eq_left_iff
-
-@[simp] theorem ite_eq_right_iff : ite P a b = b ↔ P → a = b := dite_eq_right_iff
 #align ite_eq_right_iff ite_eq_right_iff
 
 theorem dite_ne_left_iff : dite P (fun _ ↦ a) B ≠ a ↔ ∃ h, a ≠ B h := by

Mathlib/Mathport/Syntax.lean

@@ -61,7 +61,6 @@ import Mathlib.Tactic.MkIffOfInductiveProp
 import Mathlib.Tactic.ModCases
 import Mathlib.Tactic.Monotonicity
 import Mathlib.Tactic.Nontriviality
-import Mathlib.Tactic.NormCast
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.PermuteGoals

Mathlib/Tactic.lean

@@ -92,8 +92,6 @@ import Mathlib.Tactic.MoveAdd
 import Mathlib.Tactic.NoncommRing
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Tactic.Nontriviality.Core
-import Mathlib.Tactic.NormCast
-import Mathlib.Tactic.NormCast.Tactic
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NormNum.BigOperators

Mathlib/Tactic/Common.lean

@@ -61,8 +61,6 @@ import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Lift
 import Mathlib.Tactic.Lint
 import Mathlib.Tactic.MkIffOfInductiveProp
--- NormCast imports `Mathlib.Algebra.Group.Defs`
--- import Mathlib.Tactic.NormCast
 -- NormNum imports `Mathlib.Algebra.GroupPower.Lemmas` and `Mathlib.Algebra.Order.Invertible`
 -- import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NthRewrite

Mathlib/Tactic/Find.lean

@@ -25,6 +25,7 @@ open Lean
 open Lean.Meta
 open Lean.Elab
 open Lean.Elab
+open Std.Tactic
 
 namespace Mathlib.Tactic.Find
 

Mathlib/Tactic/LibrarySearch.lean

@@ -27,7 +27,7 @@ example : Nat := by exact?
 
 namespace Mathlib.Tactic.LibrarySearch
 
-open Lean Meta Std.Tactic.TryThis
+open Lean Meta Std.Tactic TryThis
 
 initialize registerTraceClass `Tactic.librarySearch
 initialize registerTraceClass `Tactic.librarySearch.lemmas