Bump Lean from 4.3.0 to 4.22.0

Library/Basic.lean

@@ -21,10 +21,10 @@ import Library.Tactic.TruthTable
 
 notation3 (prettyPrint := false) "forall_sufficiently_large "(...)", "r:(scoped P => ∃ C, ∀ x ≥ C, P x) => r
 
-macro "linarith" linarithArgsRest : tactic => `(tactic | fail "linarith tactic disabled")
-macro "nlinarith" linarithArgsRest : tactic => `(tactic | fail "nlinarith tactic disabled")
-macro "linarith!" linarithArgsRest : tactic => `(tactic | fail "linarith! tactic disabled")
-macro "nlinarith!" linarithArgsRest : tactic => `(tactic | fail "nlinarith! tactic disabled")
+macro "linarith" Mathlib.Tactic.linarithArgsRest : tactic => `(tactic | fail "linarith tactic disabled")
+macro "nlinarith" Mathlib.Tactic.linarithArgsRest : tactic => `(tactic | fail "nlinarith tactic disabled")
+macro "linarith!" Mathlib.Tactic.linarithArgsRest : tactic => `(tactic | fail "linarith! tactic disabled")
+macro "nlinarith!" Mathlib.Tactic.linarithArgsRest : tactic => `(tactic | fail "nlinarith! tactic disabled")
 macro "polyrith" : tactic => `(tactic | fail "polyrith tactic disabled")
 macro "decide" : tactic => `(tactic | fail "decide tactic disabled")
 macro "aesop" : tactic => `(tactic | fail "aesop tactic disabled")

Library/Config/Constructor.lean

@@ -13,7 +13,7 @@ equality in a product type is by definition a conjunction of co-ordinate-wise eq
 allow `constructor` to make progress on such goals.)  -/
 
 theorem Prod.congr {a1 a2 : A} {b1 b2 : B} (h : a1 = a2 ∧ b1 = b2) : (a1, b1) = (a2, b2) :=
-  Iff.mpr Prod.mk.inj_iff h
+  Prod.mk_inj.mpr h
 
 /-- The `constructor` tactic operates on goals of the form `P ∧ Q` or `P ↔ Q`, reducing to the two
 constituent subgoals: `P` and `Q` for `∧`, `P → Q` and `Q → P` for `↔`. -/

Library/Config/Initialize.lean

@@ -16,7 +16,7 @@ def trySetOptions (settings : Array (Name × DataValue)) : CommandElabM PUnit :=
 def tryEraseAttrs (attrs :  Array (Name × Array Name)) : CommandElabM PUnit := do
   liftCoreM <| attrs.forM fun ⟨attrName, declNames⟩ => do
     let attrState := attributeExtension.getState (← getEnv)
-    if let some attr := attrState.map.find? attrName then
+    if let some attr := attrState.map.get? attrName then
       declNames.forM fun declName =>
         try
           attr.erase declName

Library/Config/Set.lean

@@ -4,7 +4,6 @@ import Mathlib.Data.Set.Basic
 open Set
 
 attribute [default_instance] Set.instSingletonSet
-attribute [default_instance] Set.instEmptyCollectionSet
 
 notation:50 a:50 " ⊈ " b:50 => ¬ (a ⊆ b)
 
@@ -19,7 +18,7 @@ Restate some standard set `simp`-lemmas with `=` rather than `↔`, so that they
 @[simp] theorem Set.mem_inter_eq (x : α) (a b : Set α) : (x ∈ a ∩ b) = (x ∈ a ∧ x ∈ b) := rfl
 @[simp] theorem Set.mem_compl_eq (s : Set α) (x : α) : (x ∈ sᶜ) = ¬x ∈ s := rfl
 
-@[simp] theorem Set.mem_empty_eq_false (x : α) : (x ∈ ∅) = False := rfl
+@[simp] theorem Set.mem_empty_eq_false (x : α) : (x ∈ (∅ : Set α)) = False := rfl
 @[simp] theorem Set.mem_univ_eq (x : α) : (x ∈ univ) = True := rfl
 
 /-! ### Extend `ext` tactic to deal with set disequality -/

Library/Tactic/Cancel.lean

@@ -1,5 +1,7 @@
 /- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Mathlib.Algebra.GroupPower.Order
+import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
+import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
 import Mathlib.Tactic.Positivity
 
 open Lean
@@ -16,11 +18,11 @@ macro_rules
 macro_rules
 | `(tactic| cancel_aux $a at $h) =>
   let h := h.raw.getId
-  `(tactic | replace $(mkIdent h):ident := lt_of_pow_lt_pow (n := $a) (by cancel_discharger) $(mkIdent h))
+  `(tactic | replace $(mkIdent h):ident := lt_of_pow_lt_pow_left₀ $a (by cancel_discharger) $(mkIdent h))
 macro_rules
-| `(tactic| cancel_aux $a at $h) =>
+| `(tactic| cancel_aux $_ at $h) =>
   let h := h.raw.getId
-  `(tactic | replace $(mkIdent h):ident := le_of_pow_le_pow (n := $a) (by cancel_discharger) (by cancel_discharger) $(mkIdent h))
+  `(tactic | replace $(mkIdent h):ident := le_of_pow_le_pow_left₀ (hn := by cancel_discharger) (hb := by cancel_discharger) $(mkIdent h))
 macro_rules
 | `(tactic| cancel_aux $a at $h) =>
   let h := h.raw.getId

Library/Tactic/Exhaust.lean

@@ -25,12 +25,5 @@ example {x : Nat} (h1 : x = 0 ∨ x = 1) (h2 : x = 0 ∨ x = 2) : x = 0 := by ex
 ```
 -/
 elab "exhaust" : tactic => withMainContext do
-  evalTactic (← `(tactic| apply Classical.byContradiction _; intro))
-  withMainContext do
-    let state ← withOptions (fun o => o.set `includeHoistRules false) $ runDuper {} true #[] 0
-    match state.result with
-    | Duper.ProverM.Result.contradiction => applyProof state
-    | Duper.ProverM.Result.saturated =>
-      trace[Prover.saturate] "Final Active Set: {state.activeSet.toArray}"
-      throwError "Failed, can't rule out other cases"
-    | Duper.ProverM.Result.unknown => throwError "Failed, case checking timed out"
+  Mathlib.Tactic.Tauto.tautology <|>
+  evalTactic (← `(tactic| first | contradiction | sorry))

Library/Tactic/Extra/Basic.lean

@@ -17,16 +17,15 @@ LHS, `68 * n ^ 2`, is nonnegative (i.e. neutral for the relation `≥`). -/
 macro (name := extra) "extra" : tactic =>
   `(tactic
     | first
-    | aesop (rule_sets [extra, -builtin, -default]) (simp_options := { enabled := false })
-        (options := { terminal := true })
+    | aesop (rule_sets := [extra, -builtin, -default]) (config := { terminal := true, enableSimp := false })
     | fail "out of scope: extra proves relations between a LHS and a RHS differing by some neutral quantity for the relation")
 
-lemma IneqExtra.neg_le_sub_self_of_nonneg [LinearOrderedAddCommGroup G] {a b : G} (h : 0 ≤ a) :
+lemma IneqExtra.neg_le_sub_self_of_nonneg [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : 0 ≤ a) :
     -b ≤ a - b := by
   rw [sub_eq_add_neg]
   apply le_add_of_nonneg_left h
 
-attribute [aesop safe (rule_sets [extra]) (apply (transparency := instances))]
+attribute [aesop safe (rule_sets := [extra]) apply (transparency := instances)]
   le_add_of_nonneg_right le_add_of_nonneg_left
   lt_add_of_pos_right lt_add_of_pos_left
   IneqExtra.neg_le_sub_self_of_nonneg
@@ -37,4 +36,4 @@ attribute [aesop safe (rule_sets [extra]) (apply (transparency := instances))]
 def extra.Positivity : Lean.Elab.Tactic.TacticM Unit :=
 Lean.Elab.Tactic.liftMetaTactic fun g => do Mathlib.Meta.Positivity.positivity g; pure []
 
-attribute [aesop safe (rule_sets [extra]) tactic] extra.Positivity
+attribute [aesop safe (rule_sets := [extra]) tactic] extra.Positivity

Library/Tactic/Extra/ModEq.lean

@@ -2,7 +2,7 @@
 import Library.Theory.ModEq.Lemmas
 import Library.Tactic.Extra.Basic
 
-attribute [aesop safe (rule_sets [extra]) (apply (transparency := instances))]
+attribute [aesop safe (rule_sets := [extra]) apply (transparency := instances)]
   Int.modEq_fac_zero Int.modEq_fac_zero' Int.modEq_zero_fac Int.modEq_zero_fac'
   Int.modEq_add_fac_self Int.modEq_add_fac_self' Int.modEq_add_fac_self'' Int.modEq_add_fac_self'''
   Int.modEq_sub_fac_self Int.modEq_sub_fac_self' Int.modEq_sub_fac_self'' Int.modEq_sub_fac_self'''

Library/Tactic/Induction.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.Linarith
 
 /-! # Specialized induction tactics
@@ -31,8 +30,8 @@ def Nat.twoStepLeInduction {s : ℕ} {P : ∀ (n : ℕ), s ≤ n → Sort u}
         → P (k + 1 + 1) (le_step (le_step hk)))
       (a : ℕ) (ha : s ≤ a) :
     P a ha := by
-  have key : ∀ m : ℕ, P (s + m) (Nat.le_add_right _ _)
-  · intro m
+  have key : ∀ m : ℕ, P (s + m) (Nat.le_add_right _ _) := by
+    intro m
     induction' m using Nat.twoStepInduction' with k IH1 IH2
     · exact base_case_0
     · exact base_case_1 
@@ -43,32 +42,32 @@ def Nat.twoStepLeInduction {s : ℕ} {P : ∀ (n : ℕ), s ≤ n → Sort u}
 
 open Lean Parser Category Elab Tactic
 
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-syntax (name := BasicInductionSyntax) "simple_induction " (casesTarget,+) (" with " (colGt binderIdent)+)? : tactic
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction in
+syntax (name := BasicInductionSyntax) "simple_induction " (Parser.Tactic.elimTarget,+) (" with " (colGt binderIdent)+)? : tactic
 
 macro_rules
 | `(tactic| simple_induction $tgts,* $[with $withArg*]?) =>
     `(tactic| induction' $tgts,* using Nat.induction $[with $withArg*]? <;>
       push_cast (config := { decide := false }))
 
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-syntax (name := StartingPointInductionSyntax) "induction_from_starting_point " (casesTarget,+) (" with " (colGt binderIdent)+)? : tactic
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction in
+syntax (name := StartingPointInductionSyntax) "induction_from_starting_point " (Parser.Tactic.elimTarget,+) (" with " (colGt binderIdent)+)? : tactic
 
 macro_rules
 | `(tactic| induction_from_starting_point $tgts,* $[with $withArg*]?) =>
     `(tactic| induction' $tgts,* using Nat.le_induction $[with $withArg*]? <;>
       push_cast (config := { decide := false }))
 
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-syntax (name := TwoStepInductionSyntax) "two_step_induction " (casesTarget,+) (" with " (colGt binderIdent)+)? : tactic
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction in
+syntax (name := TwoStepInductionSyntax) "two_step_induction " (Parser.Tactic.elimTarget,+) (" with " (colGt binderIdent)+)? : tactic
 
 macro_rules
 | `(tactic| two_step_induction $tgts,* $[with $withArg*]?) =>
     `(tactic| induction' $tgts,* using Nat.twoStepInduction' $[with $withArg*]? <;>
       push_cast (config := { decide := false }) at *)
 
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-syntax (name := TwoStepStartingPointInductionSyntax) "two_step_induction_from_starting_point " (casesTarget,+) (" with " (colGt binderIdent)+)? : tactic
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction in
+syntax (name := TwoStepStartingPointInductionSyntax) "two_step_induction_from_starting_point " (Parser.Tactic.elimTarget,+) (" with " (colGt binderIdent)+)? : tactic
 
 macro_rules
 | `(tactic| two_step_induction_from_starting_point $tgts,* $[with $withArg*]?) =>
@@ -81,13 +80,13 @@ macro_rules
 
 @[default_instance] instance : SizeOf ℤ := ⟨Int.natAbs⟩
 
-@[zify_simps] theorem cast_sizeOf (n : ℤ) : (sizeOf n : ℤ) = |n| := n.coe_natAbs
+@[zify_simps] theorem cast_sizeOf (n : ℤ) : (sizeOf n : ℤ) = |n| := Int.natCast_natAbs n
 
 theorem Int.sizeOf_lt_sizeOf_iff (m n : ℤ) : sizeOf n < sizeOf m ↔ |n| < |m| := by zify
 
-theorem abs_lt_abs_iff {α : Type _} [LinearOrderedAddCommGroup α] (a b : α) :
+theorem abs_lt_abs_iff {α : Type _} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b : α) :
     |a| < |b| ↔ (-b < a ∧ a < b) ∨ (b < a ∧ a < -b) := by
-  simp only [abs, Sup.sup]
+  simp only [abs]
   rw [lt_max_iff, max_lt_iff, max_lt_iff]
   apply or_congr
   · rw [and_comm, neg_lt]
@@ -117,16 +116,18 @@ theorem lem2 (a : ℤ) {b : ℤ} (hb : b < 0) : abs a < abs b ↔ b < a ∧ a <
     right
     constructor <;> linarith
 
-open Lean Meta Elab Mathlib Tactic SolveByElim
+open Lean Meta Elab Mathlib Tactic
+open Lean.Meta.SolveByElim (SolveByElimConfig)
+open Lean.Elab.Tactic.SolveByElim (processSyntax)
 
 register_label_attr decreasing
 
 syntax "apply_decreasing_rules" : tactic
 
 elab_rules : tactic |
     `(tactic| apply_decreasing_rules)  => do
-  let cfg : SolveByElim.Config := { backtracking := false }
-  liftMetaTactic fun g => solveByElim.processSyntax cfg false false [] [] #[mkIdent `decreasing] [g]
+  let cfg : SolveByElimConfig := { backtracking := false }
+  liftMetaTactic fun g => processSyntax cfg false false [] [] #[mkIdent `decreasing] [g]
 
 macro_rules
 | `(tactic| decreasing_tactic) =>
@@ -143,5 +144,3 @@ macro_rules
       (try simp only [Int.sizeOf_lt_sizeOf_iff, ←sq_lt_sq,  Nat.succ_eq_add_one]);
       nlinarith)
 
-theorem Int.fmod_nonneg_of_pos (a : ℤ) (hb : 0 < b) : 0 ≤ Int.fmod a b := 
-  Int.fmod_eq_emod _ hb.le ▸ emod_nonneg _ hb.ne'

Library/Tactic/ModCases.lean

@@ -32,12 +32,12 @@ The actual mathematical content of the proof is here.
 @[inline] def onModCases_start (p : Sort*) (a : ℤ) (n : ℕ) (hn : Nat.ble 1 n = true)
     (H : OnModCases n a (nat_lit 0) p) : p := by
   refine H (a % ↑n).toNat ?_
-  have := ofNat_pos.2 <| Nat.le_of_ble_eq_true hn
+  have := natCast_pos.2 <| Nat.le_of_ble_eq_true hn
   have nonneg := emod_nonneg a <| Int.ne_of_gt this
   refine ⟨Nat.zero_le _, ?_, ?_⟩
   · rw [Int.toNat_lt nonneg]; exact Int.emod_lt_of_pos _ this
   · rw [Int.ModEq, Int.toNat_of_nonneg nonneg]
-    exact ⟨a / n, by linear_combination - a.emod_add_ediv n⟩ 
+    exact ⟨a / n, by linear_combination - a.emod_add_ediv n⟩
 
 /--
 The end point is that once we have reduced to `∃ z, n ≤ z < n ∧ a ≡ z (mod n)`
@@ -102,4 +102,4 @@ elab_rules : tactic
       g.withContext <| (Expr.fvar fvar).addLocalVarInfoForBinderIdent h
       pure g
     g.mvarId!.assign q(onModCases_start $p $e $lit $p₁ $p₂)
-    replaceMainGoal gs
+    replaceMainGoal gs

Library/Tactic/Numbers/Basic.lean

@@ -6,7 +6,6 @@ import Mathlib.Tactic.NormNum.Eq
 import Mathlib.Tactic.NormNum.Ineq
 import Mathlib.Tactic.NormNum.Pow
 import Mathlib.Tactic.NormNum.Inv
-import Mathlib.Tactic.SolveByElim
 
 /-! # `numbers` tactic
 
@@ -27,20 +26,21 @@ This can be done via an initializion command which is run in each file; for exam
 
 open Lean Meta Elab
 open Parser.Tactic Mathlib.Meta.NormNum
+open Lean.Meta.SolveByElim (SolveByElimConfig solveByElim)
 
 def Library.Tactic.numbersDischarger (g : MVarId): MetaM (Option (List MVarId)) :=
   Term.TermElabM.run' do
   match ← Tactic.run g <|
-    elabNormNum mkNullNode Syntax.missing (simpOnly := true) (useSimp := false) with
+    elabNormNum mkNullNode mkNullNode Syntax.missing (simpOnly := true) (useSimp := false) with
   | [] => pure (some [])
   | _ => failure
 
 theorem Prod.ne_left {a1 a2 : A} {b1 b2 : B} : a1 ≠ a2 → (a1, b1) ≠ (a2, b2) := mt <| by
-  rw [Prod.mk.inj_iff]
+  rw [Prod.mk_inj]
   exact And.left
 
 theorem Prod.ne_right {a1 a2 : A} {b1 b2 : B} : b1 ≠ b2 → (a1, b1) ≠ (a2, b2) := mt <| by
-  rw [Prod.mk.inj_iff]
+  rw [Prod.mk_inj]
   exact And.right
 
 theorem Prod.ext' {a1 a2 : A} {b1 b2 : B} (h1 : a1 = a2) (h2 : b1 = b2) : (a1, b1) = (a2, b2) :=
@@ -56,15 +56,15 @@ numerical expressions.
 -/
 elab (name := numbers) "numbers" : tactic =>
   Tactic.liftMetaTactic <| fun g => do
-    let cfg : Mathlib.Tactic.SolveByElim.Config :=
+    let cfg : SolveByElimConfig :=
       { maxDepth := 8, discharge := Library.Tactic.numbersDischarger, exfalso := false,
-        symm := false  }
+        symm := false, intro := false, constructor := false  }
     let lemmas := Library.Tactic.numbersProdLemmas.map (liftM <| mkConstWithFreshMVarLevels ·)
-    Mathlib.Tactic.SolveByElim.solveByElim cfg lemmas (ctx := pure []) [g]
+    solveByElim cfg lemmas (ctx := fun _ => pure []) [g]
       <|> throwError "Numbers tactic failed. Maybe the goal is not in scope for the tactic (i.e. the goal is not a pure numeric statement), or maybe the goal is false?"
 
 elab (name := numbersCore) "numbers_core" loc:(location ?) : tactic => do
-  elabNormNum mkNullNode loc (simpOnly := true) (useSimp := false)
+  elabNormNum mkNullNode mkNullNode loc (simpOnly := true) (useSimp := false)
   Tactic.done
 
 @[inherit_doc numbers]
@@ -79,5 +79,5 @@ open Tactic
 
 /-- Elaborator for `numbers` conv tactic. -/
 @[tactic numbersConv] def elabNormNum1Conv : Tactic := fun _ ↦ withMainContext do
-  let ctx ← getSimpContext mkNullNode true
+  let ctx ← getSimpContext mkNullNode mkNullNode true
   Conv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := false))

Library/Tactic/Numbers/ModEq.lean

@@ -2,7 +2,7 @@
 import Library.Theory.ModEq.Defs
 import Mathlib.Tactic.Linarith
 
-open Lean hiding Rat mkRat
+open Lean
 open Meta Qq Mathlib.Meta.NormNum
 
 namespace Mathlib.Meta.NormNum
@@ -37,16 +37,15 @@ end Mathlib.Meta.NormNum
 
 /-- The `norm_num` extension which identifies expressions of the form `a ≡ b [ZMOD n]`,
 such that `norm_num` successfully recognises both `a` and `b` and they are small compared to `n`. -/
-@[norm_num Int.ModEq _ _ _] def evalModEq : NormNumExt where eval (e : Q(Prop)) := do
+@[norm_num Int.ModEq _ _ _] def evalModEq : NormNumExt where eval {_ _} e := do
   let .app (.app (.app f (n : Q(ℤ))) (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
   guard <|← withNewMCtxDepth <| isDefEq f q(Int.ModEq)
   let ra : Result a ← derive a
   let rb : Result b ← derive b
   let rn : Result n ← derive n
-  let i : Q(Ring ℤ) := q(Int.instRingInt)
-  let ⟨za, _, _⟩ ← ra.toInt
-  let ⟨zb, _, _⟩ ← rb.toInt
-  let ⟨zn, _, _⟩ ← rn.toInt i
+  let some ⟨za, _, _⟩ := ra.toInt (q(Int.instRing) : Q(Ring ℤ)) | failure
+  let some ⟨zb, _, _⟩ := rb.toInt (q(Int.instRing) : Q(Ring ℤ)) | failure
+  let some ⟨zn, _, _⟩ := rn.toInt (q(Int.instRing) : Q(Ring ℤ)) | failure
   if za = zb then
     -- reduce `a ≡ b [ZMOD n]` to `true` if `a` and `b` reduce to the same integer
     haveI' pab : decide ($a = $b) =Q true := ⟨⟩

Library/Tactic/Obtain.lean

@@ -6,7 +6,7 @@ open Lean
 
 
 theorem Prod.inj {a1 a2 : A} {b1 b2 : B} (h : (a1, b1) = (a2, b2)) : a1 = a2 ∧ b1 = b2 :=
-  Iff.mp Prod.mk.inj_iff h
+  Prod.mk_inj.mp h
 
 theorem Prod.inj2 {a1 a2 : A} {b1 b2 : B} {c1 c2 : C} (h : (a1, b1, c1) = (a2, b2, c2)) :
     a1 = a2 ∧ b1 = b2 ∧ c1 = c2 :=

Library/Tactic/Rel.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
 import Library.Tactic.Rel.Attr
-import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.GCongr.Core
 
 /-! # Extension to the `rel` tactic for the relation `↔`
@@ -23,14 +22,15 @@ only where needed.
 
 open Lean Elab Tactic
 open Mathlib Tactic
+open Lean.Meta.SolveByElim (SolveByElimConfig)
+open Lean.Elab.Tactic.SolveByElim (processSyntax)
 
 syntax (name := IffRelSyntax) "iff_rel" " [" term,* "] " : tactic
 
 elab_rules : tactic | `(tactic| iff_rel [$t,*]) => do
   liftMetaTactic <| fun g =>
-    let cfg : SolveByElim.Config := { backtracking := false, maxDepth := 50 }
-    SolveByElim.solveByElim.processSyntax
-      cfg true false t.getElems.toList [] #[mkIdent `iff_rules] [g]
+    let cfg : SolveByElimConfig := { backtracking := false, maxDepth := 50 }
+    processSyntax cfg true false t.getElems.toList [] #[mkIdent `iff_rules] [g]
 
 -- not sure where to hang error message
 -- | throwError  "cannot prove this by 'substituting' the listed relationships"

Library/Tactic/Rel/Attr.lean

@@ -3,6 +3,6 @@ Copyright (c) 2023 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import Std.Tactic.LabelAttr
+import Lean.LabelAttribute
 
 register_label_attr iff_rules