chore: bump dependencies (#7767)

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

Author: kim-em

Mathlib/Init/Align.lean

@@ -5,7 +5,6 @@ Authors: Daniel Selsam, Mario Carneiro
 -/
 import Mathlib.Mathport.Rename
 import Mathlib.Init.Logic
-import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm
 import Mathlib.Tactic.Relation.Trans
 

Mathlib/Init/Core.lean

@@ -8,8 +8,8 @@ notation, basic datatypes and type classes
 import Mathlib.Mathport.Rename
 import Std.Classes.SetNotation
 import Std.Classes.Dvd
-import Mathlib.Tactic.Relation.Rfl
-import Mathlib.Tactic.Relation.Symm
+import Std.Tactic.Relation.Rfl
+import Std.Tactic.Relation.Symm
 import Mathlib.Tactic.Relation.Trans
 
 /-! ### alignments from lean 3 `init.core` -/

Mathlib/Init/Logic.lean

@@ -5,10 +5,10 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 import Std.Tactic.Ext
 import Std.Tactic.Lint.Basic
+import Std.Tactic.Relation.Rfl
 import Std.Logic
 import Std.WF
 import Mathlib.Tactic.Basic
-import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm
 import Mathlib.Mathport.Attributes
 import Mathlib.Mathport.Rename

Mathlib/Lean/Meta.lean

@@ -22,34 +22,6 @@ namespace Lean.MVarId
 def synthInstance (g : MVarId) : MetaM Unit := do
   g.assign (← Lean.Meta.synthInstance (← g.getType))
 
-/--
-Replace hypothesis `hyp` in goal `g` with `proof : typeNew`.
-The new hypothesis is given the same user name as the original,
-it attempts to avoid reordering hypotheses, and the original is cleared if possible.
--/
--- adapted from Lean.Meta.replaceLocalDeclCore
-def replace (g : MVarId) (hyp : FVarId) (proof : Expr) (typeNew : Option Expr := none) :
-    MetaM AssertAfterResult :=
-  g.withContext do
-    let typeNew ← typeNew.getDM (inferType proof)
-    let ldecl ← hyp.getDecl
-    -- `typeNew` may contain variables that occur after `hyp`.
-    -- Thus, we use the auxiliary function `findMaxFVar` to ensure `typeNew` is well-formed
-    -- at the position we are inserting it.
-    let (_, ldecl') ← findMaxFVar typeNew |>.run ldecl
-    let result ← g.assertAfter ldecl'.fvarId ldecl.userName typeNew proof
-    (return { result with mvarId := ← result.mvarId.clear hyp }) <|> pure result
-where
-  /-- Finds the `LocalDecl` for the FVar in `e` with the highest index. -/
-  findMaxFVar (e : Expr) : StateRefT LocalDecl MetaM Unit :=
-    e.forEach' fun e ↦ do
-      if e.isFVar then
-        let ldecl' ← e.fvarId!.getDecl
-        modify fun ldecl ↦ if ldecl'.index > ldecl.index then ldecl' else ldecl
-        return false
-      else
-        return e.hasFVar
-
 /-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`. -/
 def note (g : MVarId) (h : Name) (v : Expr) (t : Option Expr := .none) :
     MetaM (FVarId × MVarId) := do
@@ -236,10 +208,6 @@ namespace Lean.Elab.Tactic
 def liftMetaTactic' (tac : MVarId → MetaM MVarId) : TacticM Unit :=
   liftMetaTactic fun g => do pure [← tac g]
 
-/-- Analogue of `liftMetaTactic` for tactics that do not return any goals. -/
-def liftMetaFinishingTactic (tac : MVarId → MetaM Unit) : TacticM Unit :=
-  liftMetaTactic fun g => do tac g; pure []
-
 @[inline] private def TacticM.runCore (x : TacticM α) (ctx : Context) (s : State) :
     TermElabM (α × State) :=
   x ctx |>.run s

Mathlib/Logic/Function/Conjugate.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.Relation.Rfl
 
 #align_import logic.function.conjugate from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 

Mathlib/Mathport/Syntax.lean

@@ -71,7 +71,6 @@ import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.PushNeg
 import Mathlib.Tactic.Qify
 import Mathlib.Tactic.Recover
-import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm
 import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename

Mathlib/Tactic/Common.lean

@@ -74,7 +74,6 @@ import Mathlib.Tactic.Propose
 import Mathlib.Tactic.PushNeg
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recover
-import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm
 import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename

Mathlib/Tactic/GCongr/Core.lean

@@ -356,15 +356,15 @@ open Elab Tactic
   eval h goal := do
     let m ← mkFreshExprMVar none
     goal.assignIfDefeq (← mkAppOptM ``Eq.subst #[h, m])
-    goal.rfl
+    goal.applyRfl
 
 /-- See if the term is `a < b` and the goal is `a ≤ b`. -/
 @[gcongr_forward] def exactLeOfLt : ForwardExt where
   eval h goal := do goal.assignIfDefeq (← mkAppM ``le_of_lt #[h])
 
 /-- See if the term is `a ∼ b` with `∼` symmetric and the goal is `b ∼ a`. -/
 @[gcongr_forward] def symmExact : ForwardExt where
-  eval h goal := do (← goal.symm).assignIfDefeq h
+  eval h goal := do (← goal.applySymm).assignIfDefeq h
 
 @[gcongr_forward] def exact : ForwardExt where
   eval e m := m.assignIfDefeq e

Mathlib/Tactic/LibrarySearch.lean

@@ -158,7 +158,7 @@ def librarySearchSymm (goal : MVarId)
     Nondet MetaM (List MVarId) :=
   (librarySearchCore goal required solveByElimDepth) <|>
   .squash fun _ => do
-    if let some symm ← observing? goal.symm then
+    if let some symm ← observing? goal.applySymm then
       return librarySearchCore symm required solveByElimDepth
     else
       return .nil

Mathlib/Tactic/Relation/Rfl.lean

@@ -3,83 +3,27 @@ Copyright (c) 2022 Newell Jensen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Newell Jensen
 -/
-import Lean
 import Mathlib.Lean.Meta
+import Std.Tactic.Relation.Rfl
 
 /-!
-# `rfl` tactic extension for reflexive relations
+# `Lean.MVarId.liftReflToEq`
 
-This extends the `rfl` tactic so that it works on any reflexive relation,
-provided the reflexivity lemma has been marked as `@[refl]`.
+Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
+relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
+If this can't be done, returns the original `MVarId`.
 -/
 
 namespace Mathlib.Tactic
 
-open Lean Meta
-
-/-- Environment extensions for `refl` lemmas -/
-initialize reflExt :
-    SimpleScopedEnvExtension (Name × Array (DiscrTree.Key true)) (DiscrTree Name true) ←
-  registerSimpleScopedEnvExtension {
-    addEntry := fun dt (n, ks) ↦ dt.insertCore ks n
-    initial := {}
-  }
-
-initialize registerBuiltinAttribute {
-  name := `refl
-  descr := "reflexivity relation"
-  add := fun decl _ kind ↦ MetaM.run' do
-    let declTy := (← getConstInfo decl).type
-    let (_, _, targetTy) ← withReducible <| forallMetaTelescopeReducing declTy
-    let fail := throwError
-      "@[refl] attribute only applies to lemmas proving x ∼ x, got {declTy}"
-    let .app (.app rel lhs) rhs := targetTy | fail
-    unless ← withNewMCtxDepth <| isDefEq lhs rhs do fail
-    let key ← DiscrTree.mkPath rel
-    reflExt.add (decl, key) kind
-}
-
-open Elab Tactic
-
-/-- Closes the goal if the target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
-Otherwise throws an error.
-
-See also `Lean.MVarId.refl`, which is for `x = x` specifically.
-
-This is the `MetaM` implementation of the `rfl` tactic.
--/
-def _root_.Lean.MVarId.rfl (goal : MVarId) : MetaM Unit := do
-  let .app (.app rel _) _ ← withReducible goal.getType'
-    | throwError "reflexivity lemmas only apply to binary relations, not
-      {indentExpr (← goal.getType)}"
-  let s ← saveState
-  let mut ex? := none
-  for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
-    try
-      let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
-      if gs.isEmpty then return () else
-        logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n
-          {goalsToMessageData gs}"
-    catch e =>
-      ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
-    s.restore
-  if let some (sErr, e) := ex? then
-    sErr.restore
-    throw e
-  else
-    throwError "rfl failed, no lemma with @[refl] applies"
+open Lean Meta Elab Tactic
 
 /--
 This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
 relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
 -/
 def rflTac : TacticM Unit :=
-  withMainContext do liftMetaFinishingTactic (·.rfl)
-
-@[inherit_doc rflTac]
-elab_rules : tactic
-| `(tactic| rfl) => rflTac
+  withMainContext do liftMetaFinishingTactic (·.applyRfl)
 
 /-- Helper theorem for `Lean.MVar.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
@@ -97,7 +41,7 @@ def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
   if rel.isAppOf `Eq then
     -- No need to lift Eq to Eq
     return mvarId
-  for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
+  for lem in ← (Std.Tactic.reflExt.getState (← getEnv)).getMatch rel do
     let res ← observing? do
       -- First create an equality relating the LHS and RHS
       -- and reduce the goal to proving that LHS is related to LHS.